Annotation Interface EnsuresLTLengthOfIf
@Documented
@Retention(RUNTIME)
@Target({METHOD,CONSTRUCTOR})
@ConditionalPostconditionAnnotation(qualifier=LTLengthOf.class)
@InheritedAnnotation
@Repeatable(List.class)
public @interface EnsuresLTLengthOfIf
Indicates that the given expressions evaluate to an integer whose value is less than the lengths
of all the given sequences, if the method returns the given result (either true or false).
As an example, consider the following method:
@EnsuresLTLengthOfIf( expression = "end", result = true, targetValue = "array", offset = "#1  1" ) public boolean tryShiftIndex(@NonNegative int x) { int newEnd = end  x; if (newEnd < 0) { return false; } end = newEnd; return true; }Calling this function ensures that the field
end
of the this
object is of type
@LTLengthOf(value = "array", offset = "x  1")
, for the value x
that is passed as
the argument. This allows the Index Checker to verify that end + x
is an index into
array
in the following code:
public void useTryShiftIndex(@NonNegative int x) { if (tryShiftIndex(x)) { Arrays.fill(array, end, end + x, null); } }
 See Also:
 See the Checker Framework Manual:
 Index Checker

Nested Class Summary
Modifier and TypeClassDescriptionstatic @interface
A wrapper annotation that makes theEnsuresLTLengthOfIf
annotation repeatable. 
Required Element Summary
Modifier and TypeRequired ElementDescriptionString[]
Java expression(s) that are less than the length of the given sequences after the method returns the given result.boolean
The return value of the method that needs to hold for the postcondition to hold.String[]
Sequences, each of which is longer than each of the expressions' value after the method returns the given result. 
Optional Element Summary

Element Details

result
boolean resultThe return value of the method that needs to hold for the postcondition to hold. Returns:
 the return value of the method that needs to hold for the postcondition to hold

expression
String[] expressionJava expression(s) that are less than the length of the given sequences after the method returns the given result. Returns:
 Java expression(s) that are less than the length of the given sequences after the method returns the given result
 See the Checker Framework Manual:
 Syntax of Java expressions

targetValue
Sequences, each of which is longer than each of the expressions' value after the method returns the given result.



offset
This expression plus each of the expressions is less than the length of the sequence after the method returns the given result. Theoffset
element must ether be empty or the same length astargetValue
. Returns:
 the offset expressions
 Default:
 {}
