org.checkerframework.framework.qual

Annotation Type PostconditionAnnotation

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

The annotation E that is meta-annotated as PostconditionAnnotation must have an element called value that is an array of Strings of the same format and with the same meaning as the value expression in EnsuresQualifier.

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 and Description
Class<? extends Annotation>	qualifier The qualifier that will be established as a postcondition.

Element Detail

qualifier

public abstract Class<? extends Annotation> qualifier

The qualifier that will be established as a postcondition.

This element is analogous to EnsuresQualifier.qualifier().