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.

• If E is a type-specialized version of EnsuresQualifier, its value element must be an array of Strings, analogous to EnsuresQualifier.expression().
• If E is a type-specialized version of EnsuresQualifier.List, its value element must be an array of postcondition annotations, analogous to EnsuresQualifier.List.value().

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

Element Details

qualifier

Class<? extends Annotation> qualifier

The qualifier that will be established as a postcondition.

This element is analogous to EnsuresQualifier.qualifier().