Package org.checkerframework.checker.nonempty.qual

Annotation Interface EnsuresNonEmptyIf

@Documented @Retention(RUNTIME) @Target({METHOD,CONSTRUCTOR}) @ConditionalPostconditionAnnotation(qualifier=NonEmpty.class) @InheritedAnnotation public @interface EnsuresNonEmptyIf
Indicates that the specific expressions are non-empty, 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 a parameter that is a list, and returns true if the length of the list is non-zero. You could annotate the method as follows: 

 @EnsuresNonEmptyIf(result = true, expression = "#1")
  public <T> boolean isLengthGreaterThanZero(List<T> items) { ... }
because, if isLengthGreaterThanZero returns true, then items was non-empty. Note that you can write more than one @EnsuresNonEmptyIf annotations on a single method.

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

 @EnsuresNonEmptyIf(result = true, expression = "this.orders")
  public <T> boolean areOrdersActive() {
    return this.orders != null && this.orders.size() > 0;
 }
An @EnsuresNonEmptyIf 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 areOrdersActive() returns true, then getOrders() will return a non-empty Map. You can express this relationship as: 

 @EnsuresNonEmptyIf(result = true, expression = "this.getOrders()")
  public <T> boolean areOrdersActive() {
    return this.orders != null && this.orders.size() > 0;
 }
See Also:
See the Checker Framework Manual:
Non-Empty Checker

  • Nested Class Summary

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

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String[]
    expression
    Returns the Java expressions that are non-empty after the method returns the given result.
    boolean
    result
    A return value of the method; when the method returns that value, the postcondition holds.

  • Element Details

    • result

      boolean result
      A return value of the method; when the method returns that value, the postcondition holds.
      Returns:
      the return value of the method for which the postcondition holds

    • expression

      String[] expression
      Returns the Java expressions that are non-empty after the method returns the given result.
      Returns:
      the Java expressions that are non-empty after the method returns the given result