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

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 org.checkerframework.checker.nullness.qual.EnsuresNonNull and org.checkerframework.checker.lock.qual.EnsuresLockHeld.

Nested and Inner Type Summary

Modifier and Type	Class and Description
public static @interface	EnsuresQualifier.List A wrapper annotation that makes the `EnsuresQualifier` annotation repeatable.

Method Summary

Modifier and Type	Method and Description
public String[]	Returns: the Java expressions for which the qualifier holds after successful method termination expression() Returns the Java expressions for which the qualifier holds after successful method termination.
public Class<? extends Annotation>	Returns: the qualifier that is guaranteed to hold on successful termination of the method qualifier() Returns the qualifier that is guaranteed to hold on successful termination of the method.

Inherited from java.lang.annotation.Annotation:: annotationType equals hashCode toString

Method Detail

expression	back to summary
public String[] expression() Returns the Java expressions for which the qualifier holds after successful method termination. Returns:String[] the Java expressions for which the qualifier holds after successful method termination

expression

back to summary

public String[] expression()

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

Returns:String[]: the Java expressions for which the qualifier holds after successful method termination

qualifier	back to summary
public Class<? extends Annotation> qualifier() Returns the qualifier that is guaranteed to hold on successful termination of the method. Returns:Class<? extends Annotation> the qualifier that is guaranteed to hold on successful termination of the method

qualifier

back to summary

public Class<? extends Annotation> qualifier()

Returns the qualifier that is guaranteed to hold on successful termination of the method.

Returns:Class<? extends Annotation>: the qualifier that is guaranteed to hold on successful termination of the method

org.checkerframework.framework.qual back to summary

public @Interface EnsuresQualifier.List

Annotations

extends Annotation

@Documented
@Retention:RUNTIME
@Target:METHOD, CONSTRUCTOR
@InheritedAnnotation

A wrapper annotation that makes the EnsuresQualifier annotation repeatable.

Programmers generally do not need to write this. It is created by Java when a programmer writes more than one EnsuresQualifier annotation at the same location.

Method Summary

Modifier and Type	Method and Description
public EnsuresQualifier[]	Returns: the repeatable annotations value() Return the repeatable annotations.

Inherited from java.lang.annotation.Annotation:: annotationType equals hashCode toString

Method Detail

value	back to summary
public EnsuresQualifier[] value() Return the repeatable annotations. Returns:EnsuresQualifier[] the repeatable annotations

value

back to summary

public EnsuresQualifier[] value()

Return the repeatable annotations.

Returns:EnsuresQualifier[]: the repeatable annotations