Package org.checkerframework.common.value.qual

Annotation Interface EnsuresMinLenIf

@Documented @Retention(RUNTIME) @Target({METHOD,CONSTRUCTOR}) @ConditionalPostconditionAnnotation(qualifier=MinLen.class) @InheritedAnnotation @Repeatable(List.class) public @interface EnsuresMinLenIf
Indicates that the value of the given expression is a sequence containing at least the given number of elements, if the method returns the given result (either true or false).

When the annotated method returns result, then all the expressions in expression are considered to be MinLen(targetValue).

See Also:
See the Checker Framework Manual:
Constant Value Checker

  • Nested Class Summary

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

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String[]
    expression
    Returns Java expression(s) that are a sequence with the given minimum length after the method returns result().
    boolean
    result
    Returns the return value of the method under which the postcondition to hold.

  • Optional Element Summary

    Optional Elements
    Modifier and Type
    Optional Element
    Description
    int
    targetValue
    Returns the minimum number of elements in the sequence.

  • Element Details

    • expression

      String[] expression
      Returns Java expression(s) that are a sequence with the given minimum length after the method returns result().
      Returns:
      an array of Java expression(s), each of which is a sequence with the given minimum length after the method returns result()
      See the Checker Framework Manual:
      Syntax of Java expressions

    • result

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

    • targetValue

      @QualifierArgument("value") int targetValue
      Returns the minimum number of elements in the sequence.
      Returns:
      the minimum number of elements in the sequence
      Default:
      0