org.checkerframework.framework.qual

Annotation Type ConditionalPostconditionAnnotation

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

A meta-annotation that indicates that an annotation is a conditional postcondition annotation, i.e., a type-specialized version of EnsuresQualifierIf. The annotation that is annotated as ConditionalPostconditionAnnotation must have a value called expression that is an array of Strings of the same format and with the same meaning as the value expression in EnsuresQualifierIf, as well as a value result with the same meaning as the value result in EnsuresQualifierIf.

The value qualifier that is necessary for a conditional postcondition specified with EnsuresQualifier is hard-coded here with the value qualifier.

Author:

Stefan Heule

See Also:

EnsuresQualifier

Required Element Summary

Required Elements

Modifier and Type	Required Element and Description
java.lang.Class<? extends java.lang.annotation.Annotation>	qualifier The hard-coded qualifier for the postcondition.

Element Detail

qualifier

public abstract java.lang.Class<? extends java.lang.annotation.Annotation> qualifier

The hard-coded qualifier for the postcondition.