com.surelogic
Annotation Type Borrowed

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

Declares that the reference passed to the parameter or receiver to which this annotation is applied does not receive any new aliases due to reads from the annotated parameter or receiver during execution of the method or constructor. 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.

Annotating @Borrowed("this") on a constructor is defined to be equivalent to annotating @Unique("return"). 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, @Borrowed("this") or @Unique("return"), is a matter of programmer preference.

Annotating a field as @Borrowed means that the entity pointed to by the field is unique as long as the object with the borrowed field is being used. Put another way, the borrowed field is treated as unique as long as the unique object assigned to it isn't being used. Once the original reference is used, the borrowed field cannot be used any more. Such a field can be initialized with a value of a borrowed parameter to a constructor as long as the parameter's borrowed annotation sets the allowsReturn attribute to true and we have write access to its complete state. A @Borrowed field must be final and cannot be static.

Annotating @Borrowed on a field additionally means that the Instance region of the object referenced by the annotated field is mapped into the Instance region of the object that contains the annotated field.

Borrowed fields are not currently assured by analysis.

It is a modeling error to use this annotation on a parameter whose type is primitive. For example, the method declaration public void setValue(@Borrowed int value) would generate a modeling error. It is a modeling error to annotate @Borrowed("this") on a static method. For example, the declaration @Borrowed("this") public static void process() would generate a modeling error.

Methods that override a method with @Borrowed applied to a parameter (or the receiver), p, must also have p explicitly annotated with @Borrowed. It is a modeling error if they are not.

Semantics:

The reference in the annotated parameter or receiver at the start of the method's execution is not read from the parameter and subsequently assigned to a field of any object or returned by the method.

Examples:

In the below example, the first parameter to the static method run promises that it will not hold onto an alias to the passed Cart object. The two methods go and log promise that they will not hold onto an alias to the receiver. The combination of these three promises allows the model to be verified.

 public class Cart {
 
   static void run(@Borrowed Cart cart) {
     cart.go(10);
     cart.log("started moving");
     cart.go(20);
     cart.log("moved again");
   }
 
   int x, y;
   final List<String> log = new ArrayList<String>();
 
   @Borrowed("this")
   void go(int value) {
     x += value;
     y += value;
   }
 
   @Borrowed("this")
   void log(String msg) {
     log.add(msg);
   }
   ...
 }
 

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;
 
   @Borrowed("this")
   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("@Borrowed(this) for new(**)")
 public class Example {
   int x = 1;
   int y = 1;
   ...
 }
 

Annotating a parameter as @Borrowed only specifies that the method will not alias the reference in the annotated parameter via that parameter. If the method has access to that reference via another non-borrowed parameter, aliases may be created through the other parameter. Consider

 public class Example {
   private Example x;
   private Example y;
   
   @Unique
   private Example u;
  
   @Unique("return")
   public Example() {
     super();
   }
  
   public Example method(@Borrowed Example a, Example b) {
     a.doStuff();
     return b;
   }
   
   @Borrowed("this")
   public void doStuff() {
     // ...
   }
  
   public void run() {
     Example a = method(x, y);
     Example b = method(y, y);
     Example c = method(u, u); // Illegal: Uniqueness assurance fails here
     // ...
   }
 }
 

Here the method method() promises to borrow the reference passed to a, but says nothing about the reference passed to b. No aliases are made from a because the the method doStuff() borrows its receiver. The method returns an alias to the reference in b however.

Let's consider the calls to method() from run():

• The first call passes the values of the this.x and this.y. This call is unremarkable.
• The second call passes the value of the this.y to both parameters. This call does result in an alias to the reference in this.y, the method return value, but the alias is created through the non-borrowed parameter b.
• The third call passes the value of the @Unique field u to both parameters. This case is troubling because method() returns an alias to the field via the non-borrowed parameter b. This call, however, is rejected by uniqueness assurance because simply passing the value of u to two arguments of the same method creates aliases

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 Borrowed("a, b, c")
  */
 public void m1(Object a, Object b, Object c) { ... }
 

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

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

See Also:

Unique

Optional Element Summary

boolean	allowReturn When this attribute is true the annotated parameter (or receiver) is allowed to be assigned to a borrowed field in the object returned by the method/constructor.
String	value When annotating a constructor or a method, this attribute must be "this" to clarify the intent that it is the receiver that is borrowed.

value

public abstract String value

When annotating a constructor or a method, this attribute must be "this" to clarify the intent that it is the receiver that is borrowed. It is a modeling error if the attribute is not "this" in this case.

 class C {
   @Borrowed("this")
   public C() { ... }
 
   @Borrowed("this")
   void method() { ... }
   ...
 }
 

This attribute is not used when annotating a parameter; it is a modeling error for the value to be anything other than the default when annotating a parameter.

 int proc(@Borrowed int value       /* Illegal: Parameter has primitive type */, 
          @Borrowed Object settings /* Legal: Parameter has reference type */) { ... }
 

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

 value = ["this"] ; See above comments
 

Default:

""

allowReturn

public abstract boolean allowReturn

When this attribute is true the annotated parameter (or receiver) is allowed to be assigned to a borrowed field in the object returned by the method/constructor. This attribute is not used for borrowed fields. Assurance currently ignores this attribute.

Default:

false