Annotating classes of util package

pom.xml

@@ -365,6 +365,19 @@
   </contributors>
 
   <dependencies>
+
+    <dependency>
+      <groupId>org.checkerframework</groupId>
+      <artifactId>checker-qual</artifactId>
+      <version>2.8.2</version>
+    </dependency>
+
+    <dependency>
+      <groupId>org.checkerframework</groupId>
+      <artifactId>jdk8</artifactId>
+      <version>2.8.2</version>
+    </dependency>
+
     <dependency>
       <groupId>org.apache.commons</groupId>
       <artifactId>commons-statistics-distribution</artifactId>
@@ -460,6 +473,7 @@
   </dependencies>
 
   <properties>
+      <annotatedJdk>${org.checkerframework:jdk8:jar}</annotatedJdk>
     <!-- Do not change: "math" is the name of the component even if the
          name of the base package evolves with major release numbers
          (see "commons.osgi.symbolicName", below). -->
@@ -516,6 +530,47 @@
 
   <build>
       <plugins>
+          <plugin>
+    <!-- This plugin will set properties values using dependency information -->
+    <groupId>org.apache.maven.plugins</groupId>
+    <artifactId>maven-dependency-plugin</artifactId>
+    <executions>
+      <execution>
+        <goals>
+          <goal>properties</goal>
+        </goals>
+      </execution>
+    </executions>
+  </plugin>
+  <plugin>
+    <artifactId>maven-compiler-plugin</artifactId>
+    <version>3.6.1</version>
+    <configuration>
+      <source>1.8</source>
+      <target>1.8</target>
+      <compilerArguments>
+        <Xmaxerrs>10000</Xmaxerrs>
+        <Xmaxwarns>10000</Xmaxwarns>
+      </compilerArguments>
+      <annotationProcessorPaths>
+        <path>
+          <groupId>org.checkerframework</groupId>
+          <artifactId>checker</artifactId>
+          <version>2.8.2</version>
+        </path>
+      </annotationProcessorPaths>
+      <annotationProcessors>
+        <!-- Add all the checkers you want to enable here -->
+        <annotationProcessor>org.checkerframework.checker.index.IndexChecker</annotationProcessor>
+      </annotationProcessors>
+      <compilerArgs>
+        <!-- location of the annotated JDK, which comes from a Maven dependency -->
+        <arg>-Xbootclasspath/p:${annotatedJdk}</arg>
+        <arg>-AonlyDefs=^org\.apache\.commons\.math4\.util\.</arg>
+      </compilerArgs>
+    </configuration>
+  </plugin>
+
         <plugin>
           <groupId>org.apache.maven.plugins</groupId>
           <artifactId>maven-surefire-plugin</artifactId>
@@ -1048,5 +1103,40 @@
         </plugins>
       </build>
     </profile>
+    <profile>
+      <id>mathjax-java8</id>
+      <activation><jdk>[1.8,)</jdk></activation>
+      <properties>
+        <!-- MathJax requires additional Javadoc qualifier for Java8+ -->
+        <allowscript.javadoc.qualifier>--allow-script-in-comments</allowscript.javadoc.qualifier>
+      </properties>
+    </profile>
+    <profile>
+    <id>checker</id>
+    <dependencies>
+      <dependency>
+        <groupId>org.checkerframework</groupId>
+        <artifactId>checker</artifactId>
+        <version>2.8.2</version>
+        <scope>provided</scope>
+      </dependency>
+    </dependencies>
+    <build>
+      <plugins>
+        <plugin>
+          <groupId>org.apache.maven.plugins</groupId>
+          <artifactId>maven-dependency-plugin</artifactId>
+          <version>2.10</version>
+          <executions>
+            <execution>
+              <goals>
+                <goal>properties</goal>
+              </goals>
+            </execution>
+          </executions>
+        </plugin>
+      </plugins>
+    </build>
+  </profile>
   </profiles>
 </project>

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

@@ -20,6 +20,11 @@
 
 import org.apache.commons.math4.exception.MathIllegalArgumentException;
 
+import org.checkerframework.checker.index.qual.IndexFor;
+import org.checkerframework.checker.index.qual.LTEqLengthOf;
+import org.checkerframework.checker.index.qual.Positive;
+import org.checkerframework.checker.index.qual.LessThan;
+
 
 /**
  * A mid point strategy based on the average of begin and end indices.
@@ -38,10 +43,11 @@ public class CentralPivotingStrategy implements PivotingStrategyInterface, Seria
      * @throws MathIllegalArgumentException when indices exceeds range
      */
     @Override
-    public int pivotIndex(final double[] work, final int begin, final 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];