| Annotation Type | Description | 
|---|---|
| EnsuresLockHeld | Indicates that the given expressions are held if the method terminates successfully. | 
| EnsuresLockHeld.List | A wrapper annotation that makes the  EnsuresLockHeldannotation repeatable. | 
| EnsuresLockHeldIf | Indicates that the given expressions are held if the method terminates successfully and returns
 the given result (either true or false). | 
| EnsuresLockHeldIf.List | A wrapper annotation that makes the  EnsuresLockHeldIfannotation repeatable. | 
| GuardedBy | Indicates that a thread may dereference the value referred to by the annotated variable only if
 the thread holds all the given lock expressions. | 
| GuardedByBottom | The bottom type in the GuardedBy type system. | 
| GuardedByUnknown | It is unknown what locks guard the value referred to by the annotated variable. | 
| GuardSatisfied | If a variable  xhas type@GuardSatisfied, then all lock expressions forx's value are held. | 
| Holding | Indicates a method precondition: the specified expressions must be held when the annotated method
 is invoked. | 
| LockHeld | Indicates that an expression is used as a lock and the lock is known to be held on the current
 thread. | 
| LockingFree | The method neither acquires nor releases locks, nor do any of the methods that it calls. | 
| LockPossiblyHeld | Indicates that an expression is not known to be  LockHeld. | 
| MayReleaseLocks | The method, or one of the methods it calls, might release locks that were held prior to the
 method being called. | 
| NewObject | A type that represents a newly-constructed object. | 
| ReleasesNoLocks | The method maintains a strictly nondecreasing lock held count on the current thread for any locks
 that were held prior to the method call. |