Почему эта динамическая логическая проблема KeyY доказана, конечно, увеличение java int 2147483647 на 1 должно быть -2147483648?

Ниже приведена запись для файла задачи Key Dynamic Logic (.key). Файл проверен, когда я использую доказательство теоремы KeY. Почему эта динамическая логическая проблема KeyY доказана, конечно, увеличение java int 2147483647 на 1 должно быть -2147483648?

\programVariables {
        int i;
}

\problem {
        {i:=Integer.MAX_VALUE}
           \<{
               i++;
             }\> i=2147483648
}

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

Ответы (2)


arrow_upward
2
arrow_downward

KeyY предоставляет больше возможностей для целочисленного переполнения. Они доступны с помощью Options-> Taclet Options -> intRules (или, возможно, что-то подобное в других версиях).

Один вариант, используемый по умолчанию в моем случае, игнорирует переполнение и подтверждает проблему, два других предупреждают о переполнении или ведут себя точно так же, как java, и не подтверждают проблему. Я пробовал это с версией 2.6.3 (иначе это может быть ошибка в вашей версии или ошибка, которая не всегда срабатывает, но это маловероятно).

person Community    schedule 08.07.2020

arrow_upward
0
arrow_downward

Решение состоит в том, чтобы внести коррективы как в параметры Taclet, так и в стратегию поиска доказательств.

Параметры -> Параметры таклета -> intRules -> intRules:javaSemantics

Стратегия поиска доказательств (вкладка) -> Арифматическая обработка -> Поиск модели ИЛИ DefOps

Я считаю, что конфигурация по умолчанию должна точно отражать семантику Java, так как в целом смысл проверки на Java. Я понимаю, что могут быть некоторые конкретные сценарии, в которых было бы полезно отклониться от фактической семантики Java, однако это не должно быть случаем по умолчанию.

person newlogic    schedule 08.07.2020