import org.checkerframework.checker.index.qual.LTLengthOf;

@SuppressWarnings("lowerbound")
public class UpperBoundRefinement {
  // If expression i has type @LTLengthOf(value = "f2", offset = "f1.length") int and expression
  // j is less than or equal to the length of f1, then the type of i + j is @LTLengthOf("f2")
  void test(int[] f1, int[] f2) {
    @LTLengthOf(value = "f2", offset = "f1.length") int i = (f2.length - 1) - f1.length;
    @LTLengthOf("f1") int j = f1.length - 1;
    @LTLengthOf("f2") int x = i + j;
    @LTLengthOf("f2") int y = i + f1.length;
  }

  void test2() {
    double[] f1 = new double[10];
    double[] f2 = new double[20];

    for (int j = 0; j < f2.length; j++) {
      f2[j] = j;
    }
    for (int i = 0; i < f2.length - f1.length; i++) {
      // fill up f1 with elements of f2
      for (int j = 0; j < f1.length; j++) {
        f1[j] = f2[i + j];
      }
    }
  }

  public void test3(double[] a, double[] sub) {
    int a_index_max = a.length - sub.length;
    // Has type @LTL(value={"a","sub"}, offset={"-1 + sub.length", "-1 + a.length"})

    for (int i = 0; i <= a_index_max; i++) { // i has the same type as a_index_max
      for (int j = 0; j < sub.length; j++) { // j is @LTL("sub")
        // i + j is safe here. Because j is LTL("sub"), it should count as ("-1 + sub.length")
        double d = a[i + j];
      }
    }
  }
}