com.surelogic
Annotation Type Assume

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

Declares an assumption about a portion of the system. This assumption is limited to the scope of code that the annotation appears on. The general form is

@Assume("promise for target")

Where the promise is assumed on all declarations matched by target. For example, the below assumes a @Starts("nothing") annotation on the no-argument constructor for IllegalArgumentException. The assumption supports the @Starts("nothing") promised on the method.

 @Starts("nothing")
 @Assume("Starts(nothing) for new() in IllegalArgumentException in java.lang")
 public Rendezvous(int parties, RendezvousFunction function) {
   if (parties <= 0)
     throw new IllegalArgumentException();
   ...
 }
 

It is a modeling error to omit the for clause. Further, it is a modeling error for target to match code within the scope of the assumption. For example, the below annotation making an assumption within the scope that the assumption applies is not well-formed.

 package com.surelogic.example;
 
 // BAD - Modeling Error
 @Assume("Starts(nothing) for init() in Foo in com.surelogic.example")
 class Foo {
 
   public void init() { ... }
 }
 

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) ).

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

Examples:

Consider the following example Assume annotations on a class C:

@Assume("@Borrowed(this) for new(**) in Foo")

Applies the assumption to any constructor in Foo. The '**' pattern indicates any number of parameters including zero. If there is more than one Foo type then the assumption is made for all of them.

@Assume("@Borrowed(this) for !static **(**) in * in com.surelogic")

Applies the assumption to any instance method or constructor declared in any type in the package com.surelogic. The '**(**)' pattern matches both methods and constructors. The '*(**)' pattern only matches methods.

@Assume("@Borrowed(this) for !static *(**) | new(**) in * in com.surelogic")

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

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 Assume("Starts(nothing) for new() in IllegalArgumentException in java.lang")
  */
 public Rendezvous(int parties, RendezvousFunction function) { ... }
 

See Also:

Assumes

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