Package org.checkerframework.framework.qual

Annotation Type MonotonicQualifier

  • @Documented
@Retention(RUNTIME)
@Target(ANNOTATION_TYPE)
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.

    • Required Element Summary

      Required Elements 
      Modifier and Type Required Element Description
      java.lang.Class<? extends java.lang.annotation.Annotation> value  

    • Element Detail

      • value

        java.lang.Class<? extends java.lang.annotation.Annotation> value