Package org.checkerframework.framework.qual

Annotation Type PostconditionAnnotation

  • @Documented
@Retention(RUNTIME)
@Target(ANNOTATION_TYPE)
public @interface PostconditionAnnotation
    A meta-annotation that indicates that an annotation E is a postcondition annotation, i.e., E is a type-specialized version of EnsuresQualifier or of EnsuresQualifier.List.

    The established postcondition P has type specified by the qualifier field of this annotation.

    If the annotation E has elements annotated by QualifierArgument, their values are copied to the arguments (elements) of annotation P with the same names. Different element names may be used in E and P, if a QualifierArgument in E gives the name of the corresponding element in P.

    For example, the following code declares a postcondition annotation for the MinLen qualifier: 

    
 @PostconditionAnnotation(qualifier = MinLen.class)
 @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
  public @interface EnsuresMinLen {
    String[] value();
    @QualifierArgument("value")
    int targetValue() default 0;
    The value element holds the expressions to which the qualifier applies and targetValue holds the value for the value argument of MinLen.

    The following code then uses the annotation on a method that ensures field to be @MinLen(2) upon return. 

    
 @EnsuresMinLen(value = "field", targetValue = 2")
  public void setField(String argument) {
    field = "(" + argument + ")";
  }
    See Also:
    EnsuresQualifier, QualifierArgument

    • Required Element Summary

      Required Elements 
      Modifier and Type Required Element Description
      java.lang.Class<? extends java.lang.annotation.Annotation> qualifier
      The qualifier that will be established as a postcondition.

    • Element Detail

      • qualifier

        java.lang.Class<? extends java.lang.annotation.Annotation> qualifier
        The qualifier that will be established as a postcondition.

        This element is analogous to EnsuresQualifier.qualifier().