Annotating classes of util package

pom.xml

@@ -1135,22 +1135,6 @@
             </execution>
           </executions>
         </plugin>
-        <plugin>
-          <groupId>org.apache.maven.plugins</groupId>
-          <artifactId>maven-compiler-plugin</artifactId>
-          <version>3.3</version>
-          <configuration>
-            <source>${java.version}</source>
-            <target>${java.version}</target>
-            <annotationProcessors>
-              <annotationProcessor>org.checkerframework.checker.index.IndexChecker</annotationProcessor>
-            </annotationProcessors>
-            <compilerArgs>
-              <arg>-Xbootclasspath/p:${org.checkerframework:jdk8:jar}</arg>
-              <arg>-AonlyDefs=^org\.apache\.commons\.math4\.util\.</arg>
-            </compilerArgs>
-          </configuration>
-        </plugin>
       </plugins>
     </build>
   </profile>

src/main/java/org/apache/commons/math4/util/CentralPivotingStrategy.java

@@ -43,10 +43,11 @@ public class CentralPivotingStrategy implements PivotingStrategyInterface, Seria
      * @throws MathIllegalArgumentException when indices exceeds range
      */
     @Override
-    public int pivotIndex(final double[] work, final @LessThan("#3") @IndexFor("#1") int begin, final @Positive @LTEqLengthOf("#1") int end)
+    @SuppressWarnings("index:return.type.incompatible") // #1: begin + (end - begin)/2 = (begin + end)/2 where begin and end are @IndexFor("work"), hence, (begin + end)/2 is @IndexFor("work")
+    public @IndexFor("#1") int pivotIndex(final double[] work, final @LessThan("#3") @IndexFor("#1") int begin, final @Positive @LTEqLengthOf("#1") int end)
         throws MathIllegalArgumentException {
         MathArrays.verifyValues(work, begin, end-begin);
-        return begin + (end - begin)/2;
+        return begin + (end - begin)/2; // #1
     }
 
 }

src/main/java/org/apache/commons/math4/util/CombinatoricsUtils.java

@@ -26,6 +26,9 @@
 import org.apache.commons.numbers.combinatorics.Factorial;
 import org.apache.commons.numbers.combinatorics.BinomialCoefficient;
 
+import org.checkerframework.checker.index.qual.NonNegative;
+import org.checkerframework.checker.index.qual.LessThan;
+
 /**
  * Combinatorial utilities.
  *
@@ -57,7 +60,12 @@ private CombinatoricsUtils() {}
      * k between 20 and n-2 (S(n,n-1) is handled specifically and does not overflow)
      * @since 3.1
      */
-    public static long stirlingS2(final int n, final int k)
+    @SuppressWarnings("index:array.access.unsafe.high") /*
+    #1: i starts from 1, hence stirlingS2 has minimum 2 columns
+    #2: stirlingS2 has i + 1 columns, and j < i is checked
+    #3: k <= n as annotated and n < stirlingS2.length as annotated
+    */
+    public static long stirlingS2(final @NonNegative int n, final @NonNegative @LessThan("#1 + 1") int k)
         throws NotPositiveException, NumberIsTooLargeException, MathArithmeticException {
         if (k < 0) {
             throw new NotPositiveException(k);
@@ -78,12 +86,12 @@ public static long stirlingS2(final int n, final int k)
             stirlingS2 = new long[maxIndex][];
             stirlingS2[0] = new long[] { 1l };
             for (int i = 1; i < stirlingS2.length; ++i) {
-                stirlingS2[i] = new long[i + 1];
-                stirlingS2[i][0] = 0;
-                stirlingS2[i][1] = 1;
+                stirlingS2[i] = new long[i + 1]; // #0.1
+                stirlingS2[i][0] = 0; // #1
+                stirlingS2[i][1] = 1; // #1
                 stirlingS2[i][i] = 1;
                 for (int j = 2; j < i; ++j) {
-                    stirlingS2[i][j] = j * stirlingS2[i - 1][j] + stirlingS2[i - 1][j - 1];
+                    stirlingS2[i][j] = j * stirlingS2[i - 1][j] + stirlingS2[i - 1][j - 1]; // #2
                 }
             }
 
@@ -94,7 +102,7 @@ public static long stirlingS2(final int n, final int k)
 
         if (n < stirlingS2.length) {
             // the number is in the small cache
-            return stirlingS2[n][k];
+            return stirlingS2[n][k]; // #3
         } else {
             // use explicit formula to compute the number without caching it
             if (k == 0) {

src/main/java/org/apache/commons/math4/util/CompositeFormat.java

@@ -75,6 +75,7 @@ public static void parseAndIgnoreWhitespace(final String source,
      * @param pos input/output parsing parameter.
      * @return the first non-whitespace character.
      */
+    @SuppressWarnings("index:argument.type.incompatible") // #1: index < n (source.length) as checked by the condition of the loop and for the first time by the if statement
     public static char parseNextCharacter(final String source,
                                           final ParsePosition pos) {
          int index = pos.getIndex();
@@ -84,7 +85,7 @@ public static char parseNextCharacter(final String source,
          if (index < n) {
              char c;
              do {
-                 c = source.charAt(index++);
+                 c = source.charAt(index++); // #1
              } while (Character.isWhitespace(c) && index < n);
              pos.setIndex(index);
 
@@ -105,6 +106,7 @@ public static char parseNextCharacter(final String source,
      * @param pos input/output parsing parameter.
      * @return the special number.
      */
+    @SuppressWarnings("index:argument.type.incompatible") // #1: startIndex is @NonNegative, and as startIndex + n (@NonNegative) < source.length(), startIndex < source.length
     private static Number parseNumber(final String source, final double value,
                                       final ParsePosition pos) {
         Number ret = null;
@@ -118,7 +120,7 @@ private static Number parseNumber(final String source, final double value,
         final int startIndex = pos.getIndex();
         final int endIndex = startIndex + n;
         if (endIndex < source.length() &&
-            source.substring(startIndex, endIndex).compareTo(sb.toString()) == 0) {
+            source.substring(startIndex, endIndex).compareTo(sb.toString()) == 0) { // #1
             ret = Double.valueOf(value);
             pos.setIndex(endIndex);
         }
@@ -166,6 +168,7 @@ public static Number parseNumber(final String source, final NumberFormat format,
      * @param pos input/output parsing parameter.
      * @return true if the expected string was there
      */
+    @SuppressWarnings("index:argument.type.incompatible") // The substring function is called only when the previous two condition fail, i.e, only when startIndex < source.length() && endIndex <= source.length()
     public static boolean parseFixedstring(final String source,
                                            final String expected,
                                            final ParsePosition pos) {
@@ -174,7 +177,7 @@ public static boolean parseFixedstring(final String source,
         final int endIndex = startIndex + expected.length();
         if ((startIndex >= source.length()) ||
             (endIndex > source.length()) ||
-            (source.substring(startIndex, endIndex).compareTo(expected) != 0)) {
+            (source.substring(startIndex, endIndex).compareTo(expected) != 0)) { // #1
             // set index back to start, error index should be the start index
             pos.setIndex(startIndex);
             pos.setErrorIndex(startIndex);

src/main/java/org/apache/commons/math4/util/DoubleArray.java

@@ -16,6 +16,8 @@
  */
 package org.apache.commons.math4.util;
 
+import org.checkerframework.checker.index.qual.NonNegative;
+
 
 /**
  * Provides a standard interface for double arrays.  Allows different
@@ -57,7 +59,7 @@ public interface DoubleArray {
      * @throws ArrayIndexOutOfBoundsException if <code>index</code> is less than
      *         zero.
      */
-    void setElement(int index, double value);
+    void setElement(@NonNegative int index, double value);
 
     /**
      * Adds an element to the end of this expandable array

src/main/java/org/apache/commons/math4/util/KthSelector.java

@@ -21,6 +21,10 @@
 
 import org.apache.commons.math4.exception.NullArgumentException;
 
+import org.checkerframework.checker.index.qual.IndexFor;
+import org.checkerframework.checker.index.qual.NonNegative;
+import org.checkerframework.checker.index.qual.IndexOrHigh;
+
 
 /**
  * A Simple K<sup>th</sup> selector implementation to pick up the
@@ -76,7 +80,12 @@ public PivotingStrategyInterface getPivotingStrategy() {
      * @param k the index whose value in the array is of interest
      * @return K<sup>th</sup> value
      */
-    public double select(final double[] work, final int[] pivotsHeap, final int k) {
+    @SuppressWarnings({"index:array.access.unsafe.low", "index:argument.type.incompatible"}) /*
+    #1: node is always @NonNegative as it is changed only in #0.1 where it is minimum of 2*node + 1(or 2) and either pivotsHeap.length or end
+        pivotsHeap.length is @NonNegative as it is a length, end is also @NonNegative as it is initialized 0 and changed only in #0.2 where end = pivot >= k that is @NonNegative
+    #3: begin and end are @NonNegative as t is assign
+    */
+    public double select(final double[] work, final int[] pivotsHeap, final @IndexFor("#1") int k) {
         int begin = 0;
         int end = work.length;
         int node = 0;
@@ -85,15 +94,15 @@ public double select(final double[] work, final int[] pivotsHeap, final int k) {
             final int pivot;
 
             if (usePivotsHeap && node < pivotsHeap.length &&
-                    pivotsHeap[node] >= 0) {
+                    pivotsHeap[node] >= 0) { // #1
                 // the pivot has already been found in a previous call
                 // and the array has already been partitioned around it
-                pivot = pivotsHeap[node];
+                pivot = pivotsHeap[node]; // #1
             } else {
                 // select a pivot and partition work array around it
-                pivot = partition(work, begin, end, pivotingStrategy.pivotIndex(work, begin, end));
+                pivot = partition(work, begin, end, pivotingStrategy.pivotIndex(work, begin, end)); // #2
                 if (usePivotsHeap && node < pivotsHeap.length) {
-                    pivotsHeap[node] = pivot;
+                    pivotsHeap[node] = pivot; // #1
                 }
             }
 
@@ -102,15 +111,15 @@ public double select(final double[] work, final int[] pivotsHeap, final int k) {
                 return work[k];
             } else if (k < pivot) {
                 // the element is in the left partition
-                end  = pivot;
-                node = FastMath.min(2 * node + 1, usePivotsHeap ? pivotsHeap.length : end);
+                end  = pivot; // #0.2
+                node = FastMath.min(2 * node + 1, usePivotsHeap ? pivotsHeap.length : end); // #0.1
             } else {
                 // the element is in the right partition
                 begin = pivot + 1;
-                node  = FastMath.min(2 * node + 2, usePivotsHeap ? pivotsHeap.length : end);
+                node  = FastMath.min(2 * node + 2, usePivotsHeap ? pivotsHeap.length : end); // #0.1
             }
         }
-        Arrays.sort(work, begin, end);
+        Arrays.sort(work, begin, end); // #3
         return work[k];
     }
 
@@ -125,7 +134,7 @@ public double select(final double[] work, final int[] pivotsHeap, final int k) {
      * @param pivot initial index of the pivot
      * @return index of the pivot after partition
      */
-    private int partition(final double[] work, final int begin, final int end, final int pivot) {
+    private @NonNegative int partition(final double[] work, final @IndexFor("#1") int begin, final @IndexOrHigh("#1") int end, final @IndexFor("#1") int pivot) {
 
         final double value = work[pivot];
         work[pivot] = work[begin];

src/main/java/org/apache/commons/math4/util/MathArrays.java

@@ -48,9 +48,7 @@
 import org.checkerframework.checker.index.qual.LessThan;
 import org.checkerframework.checker.index.qual.NonNegative;
 import org.checkerframework.common.value.qual.MinLen;
-import org.checkerframework.checker.index.qual.PolySameLen;
-import org.checkerframework.checker.index.qual.PolyLowerBound;
-import org.checkerframework.checker.index.qual.PolyUpperBound;
+import org.checkerframework.framework.qual.PolyAll;
 
 /**
  * Arrays utilities.
@@ -328,7 +326,7 @@ public enum OrderDirection {
      * @param strict Whether the order should be strict.
      * @return {@code true} if sorted, {@code false} otherwise.
      */
-    public static  <T extends Comparable<? super T>> boolean isMonotonic(@PolyUpperBound @PolyLowerBound @PolySameLen T @MinLen(1) [] val,
+    public static  <T extends Comparable<? super T>> boolean isMonotonic(@PolyAll T @MinLen(1) [] val,
                                       OrderDirection dir,
                                       boolean strict) {
         T previous = val[0];
@@ -784,18 +782,21 @@ public int compare(PairDoubleInteger o1,
      * @param source Array to be copied.
      * @return the copied array.
      */
-     public static int[] copyOf(int[] source) {
-         return copyOf(source, source.length);
+    @SuppressWarnings("index:return.type.incompatible") // #1: source.length is the length of the returning array
+     public static int @SameLen("#1") [] copyOf(int[] source) {
+         return copyOf(source, source.length); // #1
      }
 
     /**
      * Creates a copy of the {@code source} array.
      *
      * @param source Array to be copied.
-     * @return the copied array.
+     * @
+     return the copied array.
      */
-     public static double[] copyOf(double[] source) {
-         return copyOf(source, source.length);
+     @SuppressWarnings("index:return.type.incompatible") // #1: source.length is the length of the returning array
+     public static double @SameLen("#1") [] copyOf(double[] source) {
+         return copyOf(source, source.length); // #1
      }
 
     /**
@@ -838,7 +839,7 @@ public static double[] copyOf(double[] source, @NonNegative int len) {
      * @param to Final index of the range to be copied, exclusive. (This index may lie outside the array.)
      * @return the copied array.
      */
-    @SuppressWarnings("index:argument.type.incompatible") // #1: As FastMath.min(len, source.length - from)) is the minimum of both the arguments, the expression <= source.length - fron and <= output
+    @SuppressWarnings("index:argument.type.incompatible") // #1: As FastMath.min(len, source.length - from)) is the minimum of both the arguments, FastMath.min(len, source.length - from)) <= source.length - from and <= output
     public static double[] copyOfRange(double[] source, @LTEqLengthOf("#1") @LessThan("#3") @NonNegative int from, @NonNegative int to) {
         final int len = to - from;
         final double[] output = new double[len];

src/main/java/org/apache/commons/math4/util/MultidimensionalCounter.java

@@ -178,14 +178,14 @@ public void remove() {
      * @throws NotStrictlyPositiveException if one of the sizes is
      * negative or zero.
      */
-    @SuppressWarnings("index:assignment.type.incompatible") // #1: By #0.1, this.size.length = size.length
+    @SuppressWarnings("index:assignment.type.incompatible") // #1: uniCounterOffset has length dimension by #0.1, hence, dimension is @LTEqLengthOf("this.uniCounterOffset")
     public MultidimensionalCounter(int @MinLen(1) ... size) throws NotStrictlyPositiveException {
-        dimension = size.length; // #1
-        this.size = MathArrays.copyOf(size); // #0.1
+        this.size = MathArrays.copyOf(size);
+        dimension = size.length; // #1:
 
-        uniCounterOffset = new int[dimension];
+        uniCounterOffset = new int[dimension]; // #0.1
 
-        last = dimension - 1; // #1
+        last = dimension - 1;
         int tS = size[last];
         for (int i = 0; i < last; i++) {
             int count = 1;
@@ -232,7 +232,7 @@ public int getDimension() {
      * {@code 0} and the value returned by {@link #getSize()} (excluded).
      */
     @SuppressWarnings("index:array.access.unsafe.high") // #1: i < last < dimension which is the length of indices and uniCounterOffset
-    public int[] getCounts(int index) throws OutOfRangeException {
+    public int[] getCounts(@NonNegative int index) throws OutOfRangeException {
         if (index < 0 ||
             index >= totalSize) {
             throw new OutOfRangeException(index, 0, totalSize);