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

• If E is a type-specialized version of EnsuresQualifierIf, it must have
  • an element expression that is an array of Strings, analogous to EnsuresQualifierIf#expression(), and
  • an element result with the same meaning as EnsuresQualifierIf#result().
• If E is a type-specialized version of EnsuresQualifierIf.List, it must have an element value that is an array of conditional postcondition annotations, analogous to EnsuresQualifierIf.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 org.checkerframework.common.value.qual.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 org.checkerframework.common.value.qual.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";
}