com.surelogic
Annotation Type Unique

@Documented
@Target(value={FIELD,CONSTRUCTOR,METHOD,PARAMETER})
public @interface Unique

Declares that the parameter, receiver, return value, or field to which this annotation is applied is a unique reference to an object. Normally this indicates that the referenced object is not aliased. It is allowed, however, to pass a unique reference to a method as an actual argument or the receiver if formal argument or receiver, respectively, is Borrowed. That is, Unique values can be safely passed to the parameter or used as the receiver with the guarantee that they will still be unique when the method returns. Said another way we create a temporary alias on the stack then ensure that it goes away.

Annotating @Unique("return") on a constructor is defined to be equivalent to annotating @Borrowed("this"). Either of these annotations indicates that the object being constructed is not aliased during construction, which implies that the reference "returned" by the new expression that invokes the constructor is unique. Which annotation is preferred, @Unique("return") or @Borrowed("this"), is a matter of programmer preference.

It is a modeling error to annotate a method return value if the return type is primitive (e.g., @Unique("return") public int getValue() would generate a modeling error). It is a modeling error to annotate a parameter if the parameter's type is primitive (e.g., public void setValue(@Unique int value) would generate a modeling error).

Examples:

A class with a unique field. Note that the getUniqueObject ensures that the returned reference is unique by creating a new object.

 public class UniqueField {
   @Unique
   private Object o;
 
   public void setField(@Unique Object value) {
     o = value;
     process(o);
   }
 
   @Unique("return")
   public Object getUniqueObject() {
     return new Object();
   }
 
   @RegionEffects("reads value:Instance")
   public static void process(@Borrowed Object value) {
     // for future processing
   }
 }
 

The call to process is allowed because that method promises that the alias to o created by the value parameter will be returned once the method call completes. However, process must also promise not to read state outside of its passed parameters. This is done with the RegionEffects annotation on the process method declaration.

This annotation is often used to support a RegionLock assertion on a constructor because if the receiver is not leaked during object construction then the state under construction will remain within the thread that invoked new.

 @RegionLock("Lock is this protects Instance")
 public class Example {
 
   int x = 1;
   int y;
 
   @Unique("return")
   public Example(int y) {
     this.y = y;
   }
   ...
 }
 

The scoped promise Promise can be used if the constructor is implicit (i.e., generated by the compiler). It has the ability to place promises on implicit and explicit constructors.

 @RegionLock("Lock is this protects Instance")
 @Promise("@Unique(return) for new(**)")
 public class Example {
   int x = 1;
   int y = 1;
   ...
 }
 

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. One complication is that the parameter being annotated must be explicitly specified because the annotation can no longer appear in the context of the parameter declaration.

 /**
  * @annotate Unique("a, b, c")
  */
 public void m1(Object a, Object b, Object c) { ... }
 

This annotation states that the three parameters are unique. Alternatively, you can use several annotations as shown below.

 /**
  * @annotate Unique("a")
  * @annotate Unique("b")
  * @annotate Unique("c")
  */
 public void m1(Object a, Object b, Object c) { ... }
 

See Also:

Borrowed

Optional Element Summary

String

value When annotating a method, this attribute is used to disambiguate whether the annotation refers to the method's receiver, the method's return value, or both.

value

public abstract String value

When annotating a method, this attribute is used to disambiguate whether the annotation refers to the method's receiver, the method's return value, or both. The value is comma separated list of tokens, and has the following set of legal values (ignoring white space issues):

• ""
• "this"
• "return"
• "this, return"
• "return, this"

The values are interpreted thusly

• If the list contains the value "this", it indicates the receiver is unique. This value is only allowed on methods.
• If the list contains the value "return", it indicates the return value is unique. This value is allowed on methods and constructors.
• If the list contains both "this" and "return", it indicates that both the receiver and the return value are unique. This value is only allowed on methods.

This attribute is not used when annotating a parameter or a field: the attribute value must be the empty string in these cases.

The value of this attribute must conform to the following grammar (in Augmented Backus–Naur Form):

 value = [("this" ["," "return"]) / ("return" ["," "this"])] ; See above comments
 

Default:

""