Package org.checkerframework.checker.index.qual

Annotation Type 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:

LTLengthOf, EnsuresLTLengthOf

See the Checker Framework Manual:

Index Checker

Required Element Summary

Required Elements

Modifier and Type	Required Element	Description
java.lang.String[]	expression	Java expression(s) that are less than the length of the given sequences after the method returns the given result.
boolean	result	The return value of the method that needs to hold for the postcondition to hold.
java.lang.String[]	targetValue	Sequences, each of which is longer than each of the expressions' value after the method returns the given result.

Optional Element Summary

Optional Elements

Modifier and Type	Optional Element	Description
java.lang.String[]	offset	This expression plus each of the expressions is less than the length of the sequence after the method returns the given result.

Element Detail

expression

java.lang.String[] expression

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

result

boolean result

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

targetValue

@JavaExpression
@QualifierArgument("value")
java.lang.String[] targetValue

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

offset

@JavaExpression
@QualifierArgument("offset")
java.lang.String[] offset

This expression plus each of the expressions is less than the length of the sequence after the method returns the given result. The offset element must ether be empty or the same length as targetValue.

Returns:

the offset expressions

Default:

{}