org.checkerframework.checker.index.qual

Annotation Type EnsuresLTLengthOfIf

@Documented
 @Retention(value=RUNTIME)
 @Target(value={METHOD,CONSTRUCTOR})
 @ConditionalPostconditionAnnotation(qualifier=LTLengthOf.class)
 @InheritedAnnotation
 @Repeatable(value=EnsuresLTLengthOfIf.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 and Description
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.
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 and Description
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

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

public abstract boolean result

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

targetValue

@JavaExpression
 @QualifierArgument(value="value")
public abstract String[] targetValue

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

offset

@JavaExpression
 @QualifierArgument(value="offset")
public abstract 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:

{}