Package org.checkerframework.checker.optional.qual

Annotation Interface EnsuresPresentIf

@Documented @Retention(RUNTIME) @Target({METHOD,CONSTRUCTOR}) @ConditionalPostconditionAnnotation(qualifier=Present.class) @InheritedAnnotation public @interface EnsuresPresentIf
Indicates that the given expressions of type Optional<T> are present, if the method returns the given result (either true or false).

Here are ways this conditional postcondition annotation can be used:

Method parameters: Suppose that a method has two arguments of type Optional<T> and returns true if they are both equal and present. You could annotate the method as follows: 

  @EnsuresPresentIf(expression="#1", result=true)
  @EnsuresPresentIf(expression="#2", result=true)
  public <T> boolean isPresentAndEqual(Optional<T> optA, Optional<T> optB) { ... }
because, if isPresentAndEqual returns true, then the first (#1) argument to isPresentAndEqual was present, and so was the second (#2) argument. Note that you can write two @EnsuresPresentIf annotations on a single method.

Fields: The value expressions can refer to fields, even private ones. For example: 

  @EnsuresPresentIf(expression="this.optShape", result=true)
  public boolean isShape() {
    return (this.optShape != null && this.optShape.isPresent());
  }
An @EnsuresPresentIf annotation that refers to a private field is useful for verifying that a method establishes a property, even though client code cannot directly affect the field.

Method postconditions: Suppose that if a method isRectangle() returns true, then getRectangle() will return a present Optional. You an express this relationship as: 

 @EnsuresPresentIf(result=true, expression="getRectangle()")
 public @Pure isRectangle() { ... }
See Also:
See the Checker Framework Manual:
Optional Checker

  • Nested Class Summary

    Nested Classes
    Modifier and Type
    Class
    Description
    static @interface 
    EnsuresPresentIf.List
    A wrapper annotation that makes the EnsuresPresentIf annotation repeatable.

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String[]
    expression
    Returns the Java expressions of type Optional<T> that are present after the method returns the given result.
    boolean
    result
    Returns the return value of the method under which the postcondition holds.

  • Element Details

    • result

      boolean result
      Returns the return value of the method under which the postcondition holds.
      Returns:
      the return value of the method under which the postcondition holds

    • expression

      String[] expression
      Returns the Java expressions of type Optional<T> that are present after the method returns the given result.
      Returns:
      the Java expressions of type Optional<T> that are present after the method returns the given result.
      See the Checker Framework Manual:
      Syntax of Java expressions