com.surelogic
Annotation Type Vouch

@Documented
@Target(value={TYPE,METHOD,CONSTRUCTOR,FIELD})
public @interface Vouch

Vouches for any inconsistent analysis result within the scope of code that the annotation appears on. This means that any inconsistent result will be changed to a consistent result. Its use is for documentation and to quiet overly conservative analysis results.

This annotation is trusted, i.e., it is not verified.

The Vouch annotation, when made on a type, constructor, or method, requires a brief programmer explanation for the vouch being made (via the value attribute).

The default value attribute of the Vouch annotation applied to a field declaration is further constrained to be one of the following:

• @Vouch("Containable") – Vouches that the object referenced by the annotated field is containable. The object is treated as if it is annotated with Containable. It is a modeling error if the type of the field is primitive. It is also a modeling error if the reference type is explicitly annotated NotContainable.
• @Vouch("final") – Vouches that the annotated field reference acts as if it is constant, or final, even though this cannot be proven by the Java compiler. It is recommended that, wherever possible, the program's code be refactored to avoid the use of this annotation—and allow the field to be declared final. It is a modeling error if the field is declared to be final
• @Vouch("Immutable") – Vouches that the object referenced by the annotated field is immutable. The object is treated as if it is annotated with Immutable. It is a modeling error if the type of the field is primitive. It is also a modeling error if the reference type is explicitly annotated Mutable.
• @Vouch("ThreadSafe") – Vouches that the object referenced by the annotated field is thread-safe. The object is treated as if it is annotated with ThreadSafe. It is a modeling error if the type of the field is primitive. It is also a modeling error if the reference type is explicitly annotated NotThreadSafe.

It is a modeling error if the Vouch annotation applied to a field does not take one of the above forms.

When used on a field declaration the reason attribute is used to capture the programmer explanation for the vouch.

Semantics:

This annotation acts upon the results reported from tools, such as SureLogic JSure, that statically verify the assertions imposed by promise annotations. It allows programmers to quiet overly conservative analysis results being reported by the tool.

Note that Vouch serves a different role than Assume. Vouches made by the programmer are typically applied in situations where a static verification tool, such as JSure, is unable to verify the programmer's implementation to be consistent with the expressed model. For example, due the fundamental limitations of static program analysis imposed by Rice's theorem or because the programmer is unwilling, perhaps due to an organizational constraint of some sort, to refactor the implementation to facilitate a static verification. In contrast, assumptions are used to express an expectation by the programmer about the evolving model—irrespective of whether or not the expectation can be verified.

Examples:

In the example code below an init method is used to set state, perhaps due to an API restriction about using constructors, and then CentralControl instances are safely published. A Vouch is used to explain that the init method needs to be an exception to the lock policy.

 @Region("private ControlRegion")
 @RegionLock("ControlLock is lock protects ControlRegion")
 public class CentralControl {
 
   private final Object lock = new Object();
 
   @InRegion("ControlRegion")
   private String f_id;
 
   @Vouch("Instances are thread confined until after init(String) is called.")
   public void init(String id) {
     f_id = id;
   }
 
   public String getId() {
     synchronized (lock) {
       return f_id;
     }
   }
 
   public void setId(String value) {
     synchronized (lock) {
       f_id = value;
     }
   }
 }
 

A Vouch is used to explain that the SmokeTest class is test code.

 @Vouch("Test code that is intentionally inconsistent with models")
 public class SmokeTest extends ... {
   ...
 }
 

A Vouch is used to explain that a class is using the cheap read-write lock trick described by Goetz. Without the Vouch the read of the value field in the getValue method would be reported to be inconsistent with the declared locking policy.

 @ThreadSafe
 public class Counter {
 
   // Employs the cheap read-write lock trick
   // All mutative operations MUST be done with the "this" lock
   @GuardedBy("this")
   private volatile int value;
 
   @Vouch("cheap read-write lock trick")
   public int getValue() {
     return value;
   }
 
   public synchronized int increment() {
     return value++;
   }
 }
 

A @Vouch("Immutable") annotation is used to express that a list made unmodifiable by invoking Collections.unmodifiableList(java.util.List) is immutable after object construction. The use of Vouch is necessary in this example because, in general, List instances are mutable.

 @Immutable
 public class KeyTimes implements Iterable {
 
   @Vouch("Immutable")
   private final List<Double> f_keyTimes;
 
   private KeyTimes(double... times) {
     final List<Double> timesList = new ArrayList();
     // fills in the collection from the passed varargs
     ...
     f_keyTimes = Collections.unmodifiableList(timesList);
   }
   ...
 }
 

The same example, but with an explanation for the vouch explicitly captured in the annotation

 @Immutable
 public class KeyTimes implements Iterable {
 
   @Vouch(value="Immutable",
          reason="Initialized with an immutable list via Collections.unmodifiableList()")
   private final List<Double> f_keyTimes;
 
   private KeyTimes(double... times) {
     final List<Double> timesList = new ArrayList();
     // fills in the collection from the passed varargs
     ...
     f_keyTimes = Collections.unmodifiableList(timesList);
   }
   ...
 }
 

A @Vouch("Immutable") annotation is used to express that a private array is immutable after object construction. Because the Java language does not allow the programmer to express that the contents of the array are unchanging, use of a Vouch is necessary in this example.

 @Immutable
 public class Aircraft {
 
   @Vouch(value="Immutable",
          reason="Initialized in the constructor; immutable thereafter")
   private final Wing[] f_wings;
 
   public Aircraft() {
     f_wings = new Wing[2];
     f_wings[0] = new Wing();
     f_wings[1] = new Wing();
   }
   ...
 }
 

A @Vouch("ThreadSafe") annotation is used to express that a list made unmodifiable by invoking Collections.synchronizedList(List) is thread-safe . The vouch is necessary because, in general, List instances are not thread-safe.

 @ThreadSafe
 public class KeyValues<T> {
 
   @Vouch("ThreadSafe")
   private final List<T> f_values;
   
   private KeyValues(List<T> values) {
     f_values = Collections.synchronizedList(values);
   }
   ...
 }
 

The below example, which is a highly questionable protocol, sets the lock once after object construction and uses @Vouch("final") to state this policy.

 @Region("private BadFinalRegion")
 @RegionLock("BadFinalLock is lock protects BadFinalRegion")
 public class BadFinal {
 
   @Vouch("final")
   private Object lock;
 
   // Called only once at startup
   public void setLock(Object value) {
     lock = value;
   }
   ...
   @InRegion("BadFinalRegion")
   private int x, y;
 
   public void tick() {
     synchronized (lock) {
       x++;
       y++;
     }
   }
   ...
 }
 

An improved implementation would set the lock via the constructor and avoid the assumption about the lock reference. In the example below, the BadFinal code is changed so that the lock field can be declared to be final (and checked by the compiler).

 @Region("private GoodFinalRegion")
 @RegionLock("GoodFinalLock is lock protects GoodFinalRegion")
 public class GoodFinal {
 
   private final Object lock;
 
   public GoodFinal(Object value) {
     lock = value;
   }
   ...
   @InRegion("GoodFinalRegion")
   private int x, y;
 
   public void tick() {
     synchronized (lock) {
       x++;
       y++;
     }
   }
   ...
 }
 

In general, use of @Vouch("final") should be avoided where it is possible to refactor the code in a manner similar to the example above.

Javadoc usage notes:

This annotation may placed in Javadoc, which can be useful for Java 1.4 code which does not include language support for annotations, via the @annotate tag.

 /**
  * @annotate Region("private ControlRegion")
  * @annotate RegionLock("ControlLock is lock protects ControlRegion")
  */
 public class CentralControl {
 
   private final Object lock = new Object();
 
   /**
    * @annotate InRegion("ControlRegion")
    */
   private String f_id;
 
   /**
    * @annotate Vouch("Instances are thread confined until after init(String) is called.")
    */
   public void init(String id) {
     f_id = id;
   }
   ...
 }
 

 /**
  * @annotate Immutable
  */
 public class KeyTimes implements Iterable {
   /**
    * @annotate Vouch("Immutable")
    */
   private final List<Double> f_keyTimes;
 
   ...
 }
 

 /**
  * @annotate Immutable
  */
 public class Aircraft {
 
   /**
    * @annotate Vouch("Immutable")
    */
   private final Wing[] f_wings;
   
   ...
 }
 

 /**
  * @annotate ThreadSafe
  */
 public class KeyValues<T> {
 
   /**
    * @annotate Vouch("ThreadSafe")
    */
   private final List<T> f_values;
   
   ...
 }
 

 public class BadFinal {
   /**
    * @annotate Vouch("final")
    */
   private Object lock;
   ...
 }
 

See Also:

Assume

Required Element Summary

String

value When the annotation applies to a type, method, or constructor then the value of this attribution must contain a brief programmer explanation of why the annotated code should have its inconsistent assurance results suppressed.

Optional Element Summary

String

reason When the annotation applies to a field declaration, this attribute contains a brief programmer explanation of why the annotated code should have its inconsistent assurance results suppressed.

Element Detail

value

public abstract String value

When the annotation applies to a type, method, or constructor then the value of this attribution must contain a brief programmer explanation of why the annotated code should have its inconsistent assurance results suppressed.

When the annotation applies to a field then the value of this attribute must conform to the following grammar (in Augmented Backus–Naur Form):

 value = "Containable" / "final" / "Immutable" / "ThreadSafe"
 

reason

public abstract String reason

When the annotation applies to a field declaration, this attribute contains a brief programmer explanation of why the annotated code should have its inconsistent assurance results suppressed.

Default:

""