org.checkerframework.framework.qual

Annotation Type ConditionalPostconditionAnnotation

@Documented
 @Retention(value=RUNTIME)
 @Target(value=ANNOTATION_TYPE)
public @interface ConditionalPostconditionAnnotation

A meta-annotation that indicates that an annotation E is a conditional postcondition annotation, i.e., E is a type-specialized version of EnsuresQualifierIf.

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

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:

  @ConditionalPostconditionAnnotation(qualifier = MinLen.class)
  @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
 public  @interface EnsuresMinLen {
   String[] expression();
   boolean result();
    @QualifierArgument("value")
   int targetValue() default 0;
 

The expression 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(4) upon returning true.

  @EnsuresMinLenIf(expression = "field", result = true, targetValue = 4")
 public boolean isFieldBool() {
   return field == "true" || field == "false";
 }
 

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 EnsuresQualifierIf.qualifier().