org.checkerframework.common.value.qual

Annotation Type EnsuresMinLenIf

@Documented
 @Retention(value=RUNTIME)
 @Target(value={METHOD,CONSTRUCTOR})
 @ConditionalPostconditionAnnotation(qualifier=MinLen.class)
 @InheritedAnnotation
 @Repeatable(value=EnsuresMinLenIf.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 and 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 and Description
int	targetValue Returns the minimum number of elements in the sequence.

Element Detail

expression

public abstract 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

public abstract 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="value")
public abstract int targetValue

Returns the minimum number of elements in the sequence.

Returns:

the minimum number of elements in the sequence

Default:

0