com.surelogic
Annotation Type Containable

@Documented
@Target(value=TYPE)
public @interface Containable

The class to which this annotation is applied is declared to be containable. That is, instances of the class can be safely encapsulated via region aggregation into other objects because methods of this class do not leak references to themselves or any of the other objects that they reference, transitively. This implies that

• each non-static method must be annotated @Borrowed("this");
• each constructor must be annotated @Unique("return"); and
• each non-primitively typed field must be
  • of a type annotated @Containable, and
  • annotated @Unique or @UniqueInRegion.

Typically, subtypes of the annotated type must be explicitly annotated @Containable as well. It is a modeling error if they are not. This annotation has two attributes, implementationOnly and verify, that control how subtypes of an Containable type must be annotated. The implementationOnly attribute indicates that the implementation of the annotated class should be assured without making a general statement about the visible behavior of the type or its subtypes. There are several rules with regards to the implementationOnly attribute on Containable types:

1. The implementationOnly attribute must be false when Containable appears on an interface, because interfaces do not have an implementation.
2. The subinterfaces of an interface annotated with Containable must be annotated with Containable; classes that implement an interface annotated with Containable must be annotated with @Containable(implementationOnly=false).
3. The superclass of a class annotated with @Containable(implementationOnly=true) must be annotated with @Containable(implementationOnly=true); there are no constraints on the subclasses.
4. The superclass of a class annotated with @Containable(implementationOnly=false) must be annotated with either @Containable(implementationOnly=false) or @Containable(implementationOnly=true); the subclasses must be annotated with @Containable(implementationOnly=false).

Finally, it may be possible to implement a class that satisfies the semantics of Containable, but that is not verifiable using the syntactic and annotation constraints described above. For this case, we provide the "escape hatch" of turning off tool verification for the annotation with the verify attribute. For example, @Containable(verify=false) would skip tool verification entirely.

A type may not be annotated with both @Containable and @NotContainable.

Semantics:

For each object transitively referenced by instances of the annotated type (including the instance itself), no reference to that object is returned by any method/constructor of the class nor is that object referenced by a field of any other object that is not also transitively referenced by the instance (including the instance itself).

Examples:

The class Point is a containable class that uses only primitively typed fields. Instances of it are in turn contained by the Rectangle class.

 @Containable
 public class Point {
   private int x;
   private int y;
 
   @Unique("return")
   @RegionEffects("none")
   public Point(int x, int y) {
     this.x = x;
     this.y = y;
   }
 
   @Borrowed("this")
   @RegionEffects("writes Instance")
   public void translate(int dx, int dy) {
     x += dx;
     y += dy;
   }
 }
 
 @Containable
 public class Rectangle {
   @Unique
   private final Point topLeft;
 
   @Unique
   private final Point bottomRight;
 
   @Unique("return")
   public Rectangle(int x1, int y1, int x2, int y2) {
     topLeft = new Point(x1, y1);
     bottomRight = new Point(x2, y2);
   }
 
   @Borrowed("this")
   @RegionEffects("writes Instance")
   public void translate(int dx, int dy) {
     topLeft.translate(dx, dy);
     bottomRight.translate(dx, dy);
   }
 }
 

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 Containable
  */
 public class Point {
   ...
 }
 

See Also:

ThreadSafe, NotContainable, Vouch

Optional Element Summary

boolean	implementationOnly Indicates that the implementation of the annotated class should be assured without making a general statement about the visible behavior of the type or its subtypes.
boolean	verify Indicates whether or not tool verification should be attempted.

implementationOnly

public abstract boolean implementationOnly

Indicates that the implementation of the annotated class should be assured without making a general statement about the visible behavior of the type or its subtypes.

Returns:

true if only the annotated class should be assured without making a general statement about the visible behavior of the type or its subtypes, false otherwise. The default value for this attribute is false.

Default:

false

verify

public abstract boolean verify

Indicates whether or not tool verification should be attempted.

Returns:

true if the claim should be verified by a tool, such as SureLogic JSure, false otherwise. The default value for this attribute is true.

Default:

true