Done with checkerframework implementation

sources/src/main/java/org/apache/commons/text/AlphabetConverter.java

@@ -31,6 +31,7 @@ import java.util.Set;
 
 import org.apache.commons.lang3.ArrayUtils;
 import org.apache.commons.lang3.StringUtils;
+import org.checkerframework.checker.index.qual.NonNegative;
 
 /**
  * <p>
@@ -104,7 +105,12 @@ public final class AlphabetConverter {
             return ArrayUtils.EMPTY_INTEGER_OBJECT_ARRAY;
         }
         final Integer[] integers = new Integer[chars.length];
-        Arrays.setAll(integers, i -> (int) chars[i]);
+        Arrays.setAll(integers, i -> {
+            assert i >= 0 && i < chars.length : "@AssumeAssertion(index): i is a valid index for integers, and integers" +
+                    "has same length of chars";
+
+            return (int) chars[i];
+        });
         return integers;
     }
 
@@ -384,7 +390,7 @@ public final class AlphabetConverter {
 
         final StringBuilder result = new StringBuilder();
 
-        for (int j = 0; j < encoded.length();) {
+        for (@NonNegative int j = 0; j < encoded.length();) {
             final int i = encoded.codePointAt(j);
             final String s = codePointToString(i);
 
@@ -393,6 +399,9 @@ public final class AlphabetConverter {
                 j++; // because we do not encode in Unicode extended the
                      // length of each encoded char is 1
             } else {
+                assert encodedLetterLength >= 0 : "@AssumeAssertion(index): follows from constructor contract of " +
+                        "AlphabetConverter";
+
                 if (j + encodedLetterLength > encoded.length()) {
                     throw new UnsupportedEncodingException("Unexpected end "
                             + "of string while decoding " + encoded);

sources/src/main/java/org/apache/commons/text/StringSubstitutor.java

@@ -29,6 +29,7 @@ import org.apache.commons.text.lookup.StringLookup;
 import org.apache.commons.text.lookup.StringLookupFactory;
 import org.apache.commons.text.matcher.StringMatcher;
 import org.apache.commons.text.matcher.StringMatcherFactory;
+import org.checkerframework.checker.index.qual.*;
 
 /**
  * Substitutes variables within a string by values.
@@ -914,7 +915,9 @@ public class StringSubstitutor {
      * @throws StringIndexOutOfBoundsException if {@code length < 0}
      * @throws StringIndexOutOfBoundsException if {@code offset + length > source.length()}
      */
-    public String replace(final String source, final int offset, final int length) {
+    public String replace(final String source,
+                          final @IndexOrHigh("#1") int offset,
+                          final @NonNegative @LTLengthOf(value = "#1", offset = "#2 - 1") int length) {
         if (source == null) {
             return null;
         }

sources/src/main/java/org/apache/commons/text/similarity/LongestCommonSubsequence.java

@@ -86,6 +86,8 @@ public class LongestCommonSubsequence implements SimilarityScore<Integer> {
             dpRows[1] = temp;
 
             for (int j = 1; j <= n; j++) {
+                assert j < dpRows[1].length : "@AssumeAssertion(index): j <= n < dpRows[1].length == (n + 1)";
+
                 if (left.charAt(i - 1) == right.charAt(j - 1)) {
                     dpRows[1][j] = dpRows[0][j - 1] + 1;
                 } else {
@@ -117,7 +119,10 @@ public class LongestCommonSubsequence implements SimilarityScore<Integer> {
         final StringBuilder out = new StringBuilder();
 
         if (m == 1) { // Handle trivial cases, as per the paper
-            final char leftCh = left.charAt(0);
+            final int zero = 0;
+            assert zero < left.length(): "@AssumeAssertion(index): m == 1 && m = left.length()";
+
+            final char leftCh = left.charAt(zero);
             for (int j = 0; j < n; j++) {
                 if (leftCh == right.charAt(j)) {
                     out.append(leftCh);
@@ -134,6 +139,10 @@ public class LongestCommonSubsequence implements SimilarityScore<Integer> {
             final int[] l1 = algorithmB(leftFirstPart, right);
             final int[] l2 = algorithmB(reverse(leftSecondPart), reverse(right));
 
+            assert n < l1.length : "@AssumeAssertion(index): Due to implementation of algorithmB";
+            assert n < l2.length : "@AssumeAssertion(index): Due to implementation of algorithmB and reverse(...) not " +
+                    "changing the number of characters in the string";
+
             // Find k, as per the Step 4 of the algorithm
             int k = 0;
             int t = 0;
@@ -145,6 +154,9 @@ public class LongestCommonSubsequence implements SimilarityScore<Integer> {
                 }
             }
 
+            assert k <= right.length() : "@AssumeAssertion(index): loop updates k with value of j, and j is always in " +
+                    "interval [0, n]";
+
             // Step 5: solve simpler problems, recursively
             out.append(algorithmC(leftFirstPart, right.subSequence(0, k)));
             out.append(algorithmC(leftSecondPart, right.subSequence(k, n)));
@@ -194,7 +206,12 @@ public class LongestCommonSubsequence implements SimilarityScore<Integer> {
 
         // Check if we can save even more space
         if (leftSz < rightSz) {
-            return algorithmB(right, left)[leftSz];
+            final int[] toReturn = algorithmB(right, left);
+
+            assert leftSz < toReturn.length : "@AssumeAssertion(index): algorithmB returns an array of length = " +
+                    "#2.length + 1";
+
+            return toReturn[leftSz];
         }
         return algorithmB(left, right)[rightSz];
     }

sources/src/main/java/org/apache/commons/text/translate/JavaUnicodeEscaper.java

@@ -97,6 +97,13 @@ public class JavaUnicodeEscaper extends UnicodeEscaper {
     @Override
     protected String toUtf16Escape(final int codePoint) {
         final char[] surrogatePair = Character.toChars(codePoint);
+        assert surrogatePair.length == 1 || surrogatePair.length == 2:
+                "@AssumeAssertion(index): assertion matches the implementation of Character.toChars";
+
+        if (surrogatePair.length == 1) {
+            throw new IllegalStateException("Expecting codepoint not to be a BMP (1 char) codepoint");
+        }
+
         return "\\u" + hex(surrogatePair[0]) + "\\u" + hex(surrogatePair[1]);
     }