| Annotation Type | Description |
|---|---|
| CalledMethods |
If an expression has type
@CalledMethods({"m1", "m2"}), then methods m1 and
m2 have definitely been called on its value. |
| CalledMethodsBottom |
The bottom type for the Called Methods type system.
|
| CalledMethodsPredicate |
This annotation represents a predicate on
@CalledMethods annotations. |
| EnsuresCalledMethods |
Indicates that the method, if it terminates successfully, always invokes the given methods on the
given expressions.
|
| EnsuresCalledMethods.List |
A wrapper annotation that makes the
EnsuresCalledMethods annotation repeatable. |
| EnsuresCalledMethodsIf |
Indicates that the method, if it terminates with the given result, invokes the given methods on
the given expressions.
|
| EnsuresCalledMethodsIf.List |
A wrapper annotation that makes the
EnsuresCalledMethodsIf annotation repeatable. |
| EnsuresCalledMethodsVarArgs |
Indicates that the method, if it terminates successfully, always invokes the given methods on all
of the arguments passed in the varargs position.
|
| RequiresCalledMethods |
Indicates a method precondition: when the method is invoked, the specified expressions must have
had the specified methods called on them.
|
| RequiresCalledMethods.List |
A wrapper annotation that makes the
RequiresCalledMethods annotation repeatable. |