Package org.checkerframework.checker.calledmethods.qual

Annotation Type EnsuresCalledMethodsIf

@Documented
@Retention(RUNTIME)
@Target({METHOD,CONSTRUCTOR})
@ConditionalPostconditionAnnotation(qualifier=CalledMethods.class)
@InheritedAnnotation
@Repeatable(List.class)
public @interface EnsuresCalledMethodsIf

Indicates that the method, if it terminates with the given result, invokes the given methods on the given expressions.

See Also:

EnsuresCalledMethods, CalledMethods

See the Checker Framework Manual:

Called Methods Checker

Required Element Summary

Required Elements

Modifier and Type	Required Element	Description
java.lang.String[]	expression	Returns Java expressions that have had the given methods called on them after the method returns result().
java.lang.String[]	methods	The methods guaranteed to be invoked on the expressions if the result of the method is result().
boolean	result	Returns the return value of the method under which the postcondition holds.

Element Detail

expression

java.lang.String[] expression

Returns Java expressions that have had the given methods called on them after the method returns result().

Returns:

an array of Java expressions

See the Checker Framework Manual:

Syntax of Java expressions

result

boolean result

Returns the return value of the method under which the postcondition holds.

Returns:

the return value of the method under which the postcondition holds

methods

@QualifierArgument("value")
java.lang.String[] methods

The methods guaranteed to be invoked on the expressions if the result of the method is result().

Returns:

the methods guaranteed to be invoked on the expressions if the result of the method is result()