com.surelogic
Annotation Type Promise

@Documented
@Target(value={PACKAGE,TYPE})
public @interface Promise

Declares a promise that applies to multiple declarations within the scope of code that the annotation appears on. The general form is

@Promise("promise for target")

Where the promise is placed on all declarations matched by target. It is possible to omit the for clause which indicates that promise should be placed on all meaningful declarations within the type or package. For example, @Promise("@Borrowed(this)") on a type places a @Borrowed("this") promise on all the method and constructors declared within the type.

The syntax for promise is the same as if the promise was written in the code except that all "'s are removed (e.g., @Borrowed("this") becomes @Borrowed(this) ).

One handy feature of this annotation is that it can be used to place promises on the implicit no-argument constructor that is generated by the compiler if a class contains no explicit constructor. The snippet below places a @Borrowed("this") on the implicit (or explicit) no-argument constructor for Implicit.

 @Promise("@Borrowed(this) for new()")
 class Implicit { ... }
 

To declare more than one scoped promise for an entity use the Promises annotation. It is a modeling error for an entity to have both a Promises and a Promise annotation.

Semantics:

This annotation creates one or more "virtual" promises within the scope of the declaration to which the annotation is applied. From the point of view of the verifying analyses, it is as if these virtual promises were annotated by the programmer—and they are to be verified. The results reported from tools, such as SureLogic JSure, should "link" each virtual promise to its associated Promise annotation to make it clear to the programmer the source of each virtual promise.

Examples:

Consider the following example Promise annotations on a class C:

@Promise("@Borrowed(this)")

Places the promise on all constructors and methods in C because @Borrowed("this") only applies to constructors and methods.

@Promise("@Borrowed(this) for new(**)")

Applies to any constructor in C. The '**' pattern indicates any number of parameters including zero.

@Promise("@Borrowed(this) for !static **(**)")

Applies to any instance method or constructor declared in C. The '**(**)' pattern matches both methods and constructors. The '*(**)' pattern only matches methods.

@Promise("@Borrowed(this) for !static *(**) | new(**)")

Equivalent to the promise above but without using the '**(**)' shorthand.

@Promise("@RequiresLock(MyLock) for some*(**) & !(someoneElse())")

Applies to any method in C with a name starting with some, except for a no-argument method named someoneElse.

@Promise("@InRegion(MyRegion) for * mutable* | int *")

Applies to fields in C declared of any type with names starting with mutable, or of type int with any name.

The scoped promise Promise can be used if the constructor is implicit. It has the ability to place promises on implicit and explicit constructors. The below example places the

 @RegionLock("Lock is this protects Instance")
 @Promise("@Borrowed(this) 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.

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

See Also:

Promises

Required Element Summary

String

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

Element Detail

value

public abstract String value

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

 value = Payload [ "for" Target ]
 
 Payload = A promise with "'s removed, e.g., @Borrowed("this") becomes @Borrowed(this)
 
 Target =
   TypeDecPat / FieldDecPat / MethodDecPat/ ConstructorDecPat /
   Target "|" Target /
   Target "&" Target /
   [ "!" ] "(" Target ")"
   
 TypeDecPat = [ Visibility ] ( QualifiedName / IdentifierPat [ InPackagePat ] )
 FieldDecPat = [ Visibility ] [ Static ] TypeSigPat IdentifierPat [ InTypePat ]
 MethodDecPat = [ Visibility ] [ Static ] IdentifierPat "(" [ ParameterSigPat ] ")" [ InTypePat ]
 ConstructorDecPat = [ Visibility ] "new" "(" [ ParameterSigPat ] ")" [ InTypePat ]
 
 TypeSigPat =
   "*" /
   ( "boolean" / "char" / "byte" / "short" /
     "int" / "long" / "float" / "double" / "void" /
     IdentifierPat / QualifiedName ) *( "[]" )
 ParameterSigPat = ( TypeSigPat / "**" ) *("," ( TypeSigPat / "**" ) )
 
 InNameExp =
   QualifiedNamePat /
   InNameExp "|" InNameExp /
   InNameExp "&" InNameExp /
   [ "!" ] "(" InNameExp ")"
 InNamePat =
   QualifiedNamePat /
   "(" InNameExp ")"
 InPackagePat = "in" InNamePat
 InTypePat    = "in" InNamePat [ InPackagePat ]
 
 Visibility = "public" / "protected" / "private"
 Static = [ "!" ] "static"
 IdentifierPat = [ "*" ] ( Identifier *("*" Identifier) ) [ "*" ]
 QualifiedNamePat = ( IdentifierPat / "*" / "**" ) *("." ( IdentifierPat / "*" / "**" ) )
 QualifiedName = Identifier *("." Identifier)
 
 IDENTIFIER = Legal Java Identifier