A conditional postcondition annotation to indicate that a method ensures that certain expressions have a certain qualifier once the method has terminated, and if the result is as indicated by result. 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:


  @EnsuresQualifierIf(result = true, expression = "#1", qualifier = Odd.class)
   boolean isOdd(int p1, int p2) {
       return p1 % 2 == 1;
   }

This annotation is only applicable to methods with a boolean return type.

Some type systems have specialized versions of this annotation, such as org.checkerframework.checker.nullness.qual.EnsuresNonNullIf and org.checkerframework.checker.lock.qual.EnsuresLockHeldIf.

Nested and Inner Type Summary

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

Method Summary

Modifier and Type	Method and Description
public String[]	Returns: the Java expressions for which the qualifier holds if the method terminates with return value `result()` expression() Returns the Java expressions for which the qualifier holds if the method terminates with return value `result()`.
public Class<? extends Annotation>	Returns: the qualifier that is guaranteed to hold if the method terminates with return value `result()` qualifier() Returns the qualifier that is guaranteed to hold if the method terminates with return value `result()`.
public boolean	Returns: the return value of the method that needs to hold for the postcondition to hold result() Returns the return value of the method that needs to hold for the postcondition to hold.

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

Method Detail

expression back to summary

expression	back to summary
public String[] expression() Returns the Java expressions for which the qualifier holds if the method terminates with return value `result()`. Returns:String[] the Java expressions for which the qualifier holds if the method terminates with return value `result()`

public String[] expression()

Returns the Java expressions for which the qualifier holds if the method terminates with return value result().

Returns:String[]: the Java expressions for which the qualifier holds if the method terminates with return value result()

qualifier back to summary

qualifier	back to summary
public Class<? extends Annotation> qualifier() Returns the qualifier that is guaranteed to hold if the method terminates with return value `result()`. Returns:Class<? extends Annotation> the qualifier that is guaranteed to hold if the method terminates with return value `result()`

public Class<? extends Annotation> qualifier()

Returns the qualifier that is guaranteed to hold if the method terminates with return value result().

Returns:Class<? extends Annotation>: the qualifier that is guaranteed to hold if the method terminates with return value result()

result	back to summary
public boolean result() Returns the return value of the method that needs to hold for the postcondition to hold. Returns:boolean the return value of the method that needs to hold for the postcondition to hold

result

back to summary

public boolean result()

Returns the return value of the method that needs to hold for the postcondition to hold.

Returns:boolean: the return value of the method that needs to hold for the postcondition to hold

org.checkerframework.framework.qual back to summary

public @Interface EnsuresQualifierIf.List

Annotations

extends Annotation

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

A wrapper annotation that makes the EnsuresQualifierIf annotation repeatable.

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

Method Summary

Modifier and Type	Method and Description
public EnsuresQualifierIf[]	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 EnsuresQualifierIf[] value() Return the repeatable annotations. Returns:EnsuresQualifierIf[] the repeatable annotations

value

back to summary

public EnsuresQualifierIf[] value()

Return the repeatable annotations.

Returns:EnsuresQualifierIf[]: the repeatable annotations