import java.util.Arrays;
import org.checkerframework.checker.index.qual.EnsuresLTLengthOf;
import org.checkerframework.checker.index.qual.EnsuresLTLengthOfIf;
import org.checkerframework.checker.index.qual.LTEqLengthOf;
import org.checkerframework.checker.index.qual.NonNegative;

class LTLengthOfPostcondition {

    Object[] array;

    @NonNegative @LTEqLengthOf("array") int end;

    @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;
    }

    public void useShiftIndex(@NonNegative int x) {
        // :: error: (argument.type.incompatible)
        Arrays.fill(array, end, end + x, null);
        shiftIndex(x);
        Arrays.fill(array, end, end + x, null);
    }

    @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;
    }

    public void useTryShiftIndex(@NonNegative int x) {
        if (tryShiftIndex(x)) {
            Arrays.fill(array, end, end + x, null);
        }
    }
}
