@Documented @Retention(value=RUNTIME) @Target(value={METHOD,CONSTRUCTOR}) @PostconditionAnnotation(qualifier=LockHeld.class) @InheritedAnnotation public static @interface EnsuresLockHeld.List
EnsuresLockHeld annotation repeatable.
 Programmers generally do not need to write this. It is created by Java when a programmer
 writes more than one EnsuresLockHeld annotation at the same location.
| Modifier and Type | Required Element and Description | 
|---|---|
| EnsuresLockHeld[] | value | 
public abstract EnsuresLockHeld[] value