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

Question

Я пытаюсь лучше понять пределы проверки ключей для Java. Я придумал сценарий, в котором определенный элемент массива вызовет исключение нулевого указателя. Когда я пропускаю это через прувер, он проходит. Есть идеи, почему это так? Он должен завершиться ошибкой, поскольку нулевой указатель будет брошен на элемент массива 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 Семантика случаев спецификации нормального поведения") ключевой книги.