@Target(value=ANNOTATION_TYPE) @Retention(value=RUNTIME) public @interface ConditionalPostconditionAnnotation
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.
EnsuresQualifier| Modifier and Type | Required Element and Description |
|---|---|
Class<? extends Annotation> |
qualifier
The hard-coded qualifier for the postcondition.
|
public abstract Class<? extends Annotation> qualifier