Key Java JML proover передает этот алгоритм, который считывает указанный элемент массива c, который вызывает исключение NullPointerException? вместо этого он должен потерпеть неудачу

Question

Я пытаюсь лучше понять пределы проверки ключей для Java. Я придумал сценарий, в котором указанный элемент массива c вызовет исключение нулевого указателя. Когда я пропускаю это через прувер, он проходит. Есть идеи, почему это так? Он должен завершиться ошибкой, поскольку нулевой указатель будет брошен в элемент массива 86454. Обратите внимание, что "normal_behaviour" означает, что он должен завершиться без исключений.

/*@ 
 @ normal_behaviour
 @ requires true;
 @ ensures \result == 7;
 @*/ 
public static int tmp() {
    Object[] arr = new Object[999999];
    arr[86454] = new Integer(6);
    for (int i=0;i<999999;i++){
        if (arr[i]!=null && arr[i].equals(new Integer(6))){
            throw new NullPointerException();
        }
    }
    return 7;
}

Answer 1

Ваша спецификация охватывает только нормальное поведение, а не исключительный случай.

Нормальное поведение означает, что все постусловия должны соблюдаться после выполнения метода. Следовательно, существует возвращаемое значение, и вам разрешен доступ к нему (\result). В исключительном случае ваше предложение requires не будет четко определено.

Если вы хотите указать случай, когда возникает исключение, вы должны использовать exceptional_behavior и в случае, если вы хотите показать для «свободы от исключений» используйте behavior. Оба в сочетании с предложением signals. Например, используйте следующее, чтобы показать свободу от исключений:

/*@ public behavior 
    requires true; 
    signals (Exception e) false;
*/

Этот контракт не может быть выполнен методом, который может вызвать исключение.

См. Глава 7 (особенно «7.3.3 Семантика случаев спецификации нормального поведения») ключевой книги.