org.checkerframework.common.value.qual

Annotation Type EnsuresMinLenIf

@Documented
 @Retention(value=RUNTIME)
 @Target(value={METHOD,CONSTRUCTOR})
 @ConditionalPostconditionAnnotation(qualifier=MinLen.class)
 @InheritedAnnotation
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 and Description
String[]	expression Java expression(s) that are a sequence with the given minimum length after the method returns the given result.
boolean	result The return value of the method that needs to hold for the postcondition to hold.

Optional Element Summary

Optional Elements

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

Element Detail

expression

public abstract String[] expression

Java expression(s) that are a sequence with the given minimum length after the method returns the given result.

See the Checker Framework Manual:

Syntax of Java expressions

result

public abstract boolean result

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

targetValue

@QualifierArgument(value="value")
public abstract int targetValue

The minimum number of elements in the sequence.

Default:

0