org.checkerframework.checker.index.qual

Annotation Type EnsuresLTLengthOf

@Documented
 @Retention(value=RUNTIME)
 @Target(value={METHOD,CONSTRUCTOR})
 @InheritedAnnotation
public @interface EnsuresLTLengthOf

Indicates that the value expressions evaluate to an integer whose value is less than the lengths of all the given sequences, if the method terminates successfully.

See Also:

LTLengthOf, IndexChecker

See the Checker Framework Manual:

Index Checker

Required Element Summary

Required Elements

Modifier and Type	Required Element and Description
String[]	targetValue Sequences, each of which is longer than the each of the expressions' value on successful method termination.
String[]	value The Java expressions that are less than the length of the given sequences on successful method termination.

Optional Element Summary

Optional Elements

Modifier and Type	Optional Element and Description
String[]	offset This expression plus each of the value expressions is less than the length of the sequence on successful method termination.

Element Detail

value

public abstract String[] value

The Java expressions that are less than the length of the given sequences on successful method termination.

See the Checker Framework Manual:

Syntax of Java expressions

targetValue

public abstract String[] targetValue

Sequences, each of which is longer than the each of the expressions' value on successful method termination.

offset

public abstract String[] offset

This expression plus each of the value expressions is less than the length of the sequence on successful method termination. The offset element must ether be empty or the same length as targetValue.

Default:

{}