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.
-
-
Element Detail
-
value
java.lang.String[] value
The Java expressions to which the qualifier applies.- Returns:
- the Java expressions to which the qualifier applies
- See Also:
EnsuresQualifier
-
-
-
methods
@QualifierArgument("value") java.lang.String[] methods
The methods guaranteed to be invoked on the expressions.- Returns:
- the methods guaranteed to be invoked on the expressions
-
-