Проблема алгоритма с двумя суммами встречает openjml: основные вопросы

Question

Я пытаюсь разобраться в JML через OpenJML и подумал, что очень классным примером может быть двузначный вопрос о каноническом алгоритме:

https://leetcode.com/problems/two-sum

Каноническое решение - использовать хеш-таблицу для запоминания видимых элементов, что приводит к O (n) времени и сложностям с памятью. Ниже приведена программа на Java, которая реализует такую ​​идею и проходит все тесты в ссылке leetcode выше; он также включает предварительные и последующие условия JML:

https://gitlab.com/dario.mx/leetcode-jml/-/blob/master/src/easy/two-sum/TwoSum.java

Тем не менее, когда я пробую это на OpenJML, он не может подтвердить ни одно из моих постусловий. См. Внизу пример выполнения в командной строке. Не могли бы вы поделиться своими мыслями о природе этих предупреждений? Это отсутствие поддерживаемых функций Java, отсутствие возможностей для доказательства теорем или что-то мне не хватает?

Меня особенно смущают основные условия публикации о массиве результатов, который я прошу иметь длину 2 и содержать пару индексов из массива. Тем не менее OpenJML не может доказать ничего из этого, и даже больше говорит, что он не может доказать неотрицательность индекса; чего я не понимаю, индекс получает свое значение из положительного домена. Точно так же массив результатов дважды присваивается статическому массиву размера два; следовательно, почему он не может доказать мое постусловие о своем размере? Прежде чем разобраться в этих случаях, возможно, не стоит спрашивать об действительно интересном постусловии; тот, который говорит, что результирующие два индекса должны соответствовать элементам x и y в массиве, так что x + y == target.

Я упустил что-то фундаментальное? Пожалуйста, помогите мне увидеть свет:-)

Благодарю.

# ./openjml -esc examples/two-sum/TwoSum.java
examples/two-sum/TwoSum.java:24: warning: The prover cannot establish
an assertion (PossiblyNegativeIndex) in method twoSum
            int x = nums[i];
                        ^
examples/two-sum/TwoSum.java:33: warning: The prover cannot establish
an assertion (Postcondition: examples/two-sum/TwoSum.java:15: ) in
method twoSum
        return ans;
        ^
examples/two-sum/TwoSum.java:15: warning: Associated declaration:
examples/two-sum/TwoSum.java:33:
      @ ensures \result.length == 2;
        ^
examples/two-sum/TwoSum.java:33: warning: The prover cannot establish
an assertion (Postcondition: examples/two-sum/TwoSum.java:18: ) in
method twoSum
        return ans;
        ^
examples/two-sum/TwoSum.java:18: warning: Associated declaration:
examples/two-sum/TwoSum.java:33:
      @ ensures nums[\result[0]] + nums[\result[1]] == target;
        ^
examples/two-sum/TwoSum.java:33: warning: The prover cannot establish
an assertion (Postcondition: examples/two-sum/TwoSum.java:16: ) in
method twoSum
        return ans;
        ^
examples/two-sum/TwoSum.java:16: warning: Associated declaration:
examples/two-sum/TwoSum.java:33:
      @ ensures \exists int i, j; 0 <= i && i < j && j < nums.length;
        ^

./openjml.jar(specs/org/jmlspecs/lang/intmap.jml):23: warning: The
prover cannot establish an assertion (UndefinedNullDeReference:
./openjml.jar(specs/org/jmlspecs/lang/intmap.jml):28: ) in method
twoSum
      ensures this[k] == v ==> \result == this;
                  ^
./openjml.jar(specs/org/jmlspecs/lang/intmap.jml):28: warning:
Associated declaration:
./openjml.jar(specs/org/jmlspecs/lang/intmap.jml):23:
9 warnings