Annotation Interface EnsuresLTLengthOf
@Documented
@Retention(RUNTIME)
@Target({METHOD,CONSTRUCTOR})
@PostconditionAnnotation(qualifier=LTLengthOf.class)
@InheritedAnnotation
@Repeatable(List.class)
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.
Consider the following example, from the Index Checker's regression tests:
@EnsuresLTLengthOf(value = "end", targetValue = "array", offset = "#1 - 1")
public void shiftIndex(@NonNegative int x) {
int newEnd = end - x;
if (newEnd < 0) throw new RuntimeException();
end = newEnd;
}
where end
is annotated as @NonNegative @LTEqLengthOf("array") int end;
This method guarantees that end
has type @LTLengthOf(value="array", offset="x -
1")
after the method returns. This is useful in cases like this one:
public void useShiftIndex(@NonNegative int x) {
// :: error: (argument)
Arrays.fill(array, end, end + x, null);
shiftIndex(x);
Arrays.fill(array, end, end + x, null);
}
The first call to Arrays.fill
is rejected (hence the comment about an error). But, after
calling shiftIndex(x)
, end
has an annotation that allows the end + x
to
be accepted as @LTLengthOf("array")
.- See Also:
- See the Checker Framework Manual:
- Index Checker
-
Nested Class Summary
Modifier and TypeClassDescriptionstatic @interface
A wrapper annotation that makes theEnsuresLTLengthOf
annotation repeatable. -
Required Element Summary
-
Optional Element Summary
-
Element Details
-
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
Sequences, each of which is longer than the each of the expressions' value on successful method termination.
-
-
-
offset
This expression plus each of the value expressions is less than the length of the sequence on successful method termination. Theoffset
element must ether be empty or the same length astargetValue
.- Returns:
- the offset expressions
- Default:
- {}
-