org.checkerframework.framework.qual

Annotation Type MonotonicQualifier

@Target(value=ANNOTATION_TYPE)
 @Retention(value=RUNTIME)
public @interface MonotonicQualifier

A meta-annotation that indicates that a qualifier indicates that an expression goes monotonically from a type qualifier T to another qualifier S. The annotation S is called the target of the monotonic qualifier, and has to be indicated by value().

This meta-annotation can be used on the declaration of the monotonic qualifier used for the type-system at hand, and is often called MonoT if the target is T. The subtyping hierarchy has to be defined as follows:

   T <: MonoT <: S
 

where <: indicates the subtyping relation.

An expression of a monotonic type can only be assigned expressions of the target type T. This means that an expression of the monotonic type MonoT cannot be assigned to a variable of the same type.

Reading an expression of a monotonic type MonoT might always yield an expression of type S. However, once it has been observed that a variable has the target type T, the monotonic property ensures that it will stay of type T for the rest of the program execution. This is even true if arbitrary other code is executed.

Note that variables of a monotonic type can be re-assigned arbitrarily often, but only with expressions of the target type.

Author:

Stefan Heule

Required Element Summary

Required Elements

Modifier and Type	Required Element and Description
Class<? extends Annotation>	value

Element Detail

value

public abstract Class<? extends Annotation> value