@Target(value=ANNOTATION_TYPE)
@Retention(value=RUNTIME)
public @interface PostconditionAnnotation
EnsuresQualifier
.
The annotation that is annotated as PostconditionAnnotation
must have
a value called value
that is an array of String
s of the same
format and with the same meaning as the value expression
in
EnsuresQualifier
.
The value qualifier
that is necessary for a 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.
|