org.checkerframework.framework.qual

Annotation Type EnsuresQualifier

@Documented
 @Retention(value=RUNTIME)
 @Target(value={METHOD,CONSTRUCTOR})
 @InheritedAnnotation
public @interface EnsuresQualifier

A postcondition annotation to indicate that a method ensures certain expressions to have a certain type qualifier once the method has successfully terminated. The expressions for which the qualifier must hold after the method's execution are indicated by expression and are specified using a string. The qualifier is specified by qualifier.

Here is an example use:

   @EnsuresQualifier(expression = "p.f1", qualifier = Odd.class)
   void oddF1_1() {
       p.f1 = null;
   }
 

Some type systems have specialized versions of this annotation, such as @EnsuresNonNull and @EnsuresLockHeld.

Author:

Stefan Heule

See Also:

EnsuresQualifiers, EnsuresQualifierIf

See the Checker Framework Manual:

Syntax of Java expressions

Required Element Summary

Required Elements

Modifier and Type	Required Element and Description
java.lang.String[]	expression The Java expressions for which the qualifier holds after successful method termination.
java.lang.Class<? extends java.lang.annotation.Annotation>	qualifier The qualifier that is guaranteed to hold on successfull termination of the method.

Element Detail

expression

public abstract java.lang.String[] expression

The Java expressions for which the qualifier holds after successful method termination.

See the Checker Framework Manual:

Syntax of Java expressions

qualifier

public abstract java.lang.Class<? extends java.lang.annotation.Annotation> qualifier

The qualifier that is guaranteed to hold on successfull termination of the method.