EnsuresMinLenIf (checker-framework 3.39.0-eisop1 API)

```
@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:

MinLen

See the Checker Framework Manual:
Constant Value Checker

Required Element Summary

Required Elements
Modifier and Type	Required Element	Description
`java.lang.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 Detail
  - expression
```
java.lang.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