Annotation Type EnsuresCalledMethods
@PostconditionAnnotation(qualifier=CalledMethods.class)
@Target({METHOD,CONSTRUCTOR})
public @interface EnsuresCalledMethods
Indicates that the method, if it terminates successfully, always invokes the given methods on the
given expressions.
Consider the following method:
@EnsuresCalledMethods(value = "#1", methods = "m") public void callM(T t) { ... }
This method guarantees that t.m()
is always called before the method returns.
-
Required Element Summary
Required Elements
-
Element Details
-
value
String[] valueThe Java expressions to which the qualifier applies.- Returns:
- the Java expressions to which the qualifier applies
- See Also:
-
methods
The methods guaranteed to be invoked on the expressions.- Returns:
- the methods guaranteed to be invoked on the expressions
-