Annotation Type EnsuresQualifierIf
-
@Documented @Retention(RUNTIME) @Target(METHOD) @InheritedAnnotation @Repeatable(List.class) public @interface EnsuresQualifierIf
A conditional postcondition annotation to indicate that a method ensures that certain expressions have a certain qualifier once the method has terminated, and if the result is as indicated byresult
. The expressions for which the qualifier holds after the method's execution are indicated byexpression
and are specified using a string. The qualifier is specified by thequalifier
annotation element.Here is an example use:
@EnsuresQualifierIf(result = true, expression = "#1", qualifier = Odd.class) boolean isOdd(int p1, int p2) { return p1 % 2 == 1; }
This annotation is only applicable to methods with a boolean return type.
Some type systems have specialized versions of this annotation, such as
org.checkerframework.checker.nullness.qual.EnsuresNonNullIf
andorg.checkerframework.checker.lock.qual.EnsuresLockHeldIf
.- See Also:
EnsuresQualifier
- See the Checker Framework Manual:
- Syntax of Java expressions
-
-
Required Element Summary
Required Elements Modifier and Type Required Element Description java.lang.String[]
expression
Returns the Java expressions for which the qualifier holds if the method terminates with return valueresult()
.java.lang.Class<? extends java.lang.annotation.Annotation>
qualifier
Returns the qualifier that is guaranteed to hold if the method terminates with return valueresult()
.boolean
result
Returns the return value of the method that needs to hold for the postcondition to hold.
-
-
-
Element Detail
-
expression
java.lang.String[] expression
Returns the Java expressions for which the qualifier holds if the method terminates with return valueresult()
.- Returns:
- the Java expressions for which the qualifier holds if the method terminates with
return value
result()
- See the Checker Framework Manual:
- Syntax of Java expressions
-
-