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

Question

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

\programVariables {
        int i;
}

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

Answer 1

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

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

Answer 2

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

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

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

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