Package org.checkerframework.framework.qual

Annotation Interface PreconditionAnnotation

@Documented @Retention(RUNTIME) @Target(ANNOTATION_TYPE) public @interface PreconditionAnnotation
A meta-annotation that indicates that an annotation R is a precondition annotation, i.e., R is a type-specialized version of RequiresQualifier. The value qualifier that is necessary for a precondition specified with RequiresQualifier is specified here with the value qualifier.

The annotation R that is meta-annotated as PreconditionAnnotation 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 RequiresQualifier.

The established precondition P has type specified by the qualifier field of this annotation. If the annotation R 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 R and P, if a QualifierArgument in R gives the name of the corresponding element in P.

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


 @PreconditionAnnotation(qualifier = MinLen.class)
 @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
 public @interface RequiresMinLen {
   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 requires field to be @MinLen(2) upon entry. 


 @RequiresMinLen(value = "field", targetValue = 2")
 public char getThirdCharacter() {
   return field.charAt(2);
 }
See Also:

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    Class<? extends Annotation>
    qualifier
    The qualifier that must be established as a precondition.

  • Element Details

    • qualifier

      Class<? extends Annotation> qualifier
      The qualifier that must be established as a precondition.