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

Я пытаюсь лучше понять ограничения проверки ключей для 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;
}

java formal-verification jml openjml key-formal-verification
person newlogic    schedule 13.07.2020    source источник

Ответы (1)


arrow_upward
0
arrow_downward

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

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

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

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

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

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

person wadoon    schedule 15.07.2020
comment
Предложение normal_behaviour не допускает никаких исключений по умолчанию. Нормальное поведение получает дополнительный пункт signal (Throwable t) false 8.2 из книги Key Deductive Software Verification (2016). Я не понимаю, как этот метод может быть передан верификатором, он всегда будет вызывать исключение NullPointerException. Requires не имеет никакого эффекта, так как для него установлено значение true, поэтому разрешено любое предварительное состояние. - person newlogic; 15.07.2020