| Annotation Type | Description |
|---|---|
| EnsuresLockHeld |
Indicates that the value expressions are
LockHeld if the method
terminates successfully. |
| EnsuresLockHeldIf |
Indicates that the given expressions are @LockHeld
if the method returns the given result (either true or false).
|
| GuardedBy |
The field (or other variable) to which this annotation is applied can
only be accessed when holding a particular lock, which may be a built-in
(synchronization) lock, or may be an explicit
Lock. |
| Holding |
Indicates a method pre and postcondition: the method expects the
specified expressions to be @LockHeld when the annotated method
is invoked.
|
| HoldingOnEntry |
Indicates a method precondition: the method expects the specified
expressions to be @LockHeld when the annotated method is invoked.
|
| LockHeld |
LockHeld is a type annotation that indicates that an expression is
used as a lock and the lock is known to be held on the current thread. |
| LockPossiblyHeld |
LockPossiblyHeld is a type annotation that indicates that the value is not
known to be @LockHeld (see LockHeld). |