@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 String
s 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 |
---|---|
java.lang.Class<? extends java.lang.annotation.Annotation> |
qualifier
The hard-coded qualifier for the postcondition.
|