java - 为什么这个Key动态逻辑问题得到证明，肯定将2147483647的java int增加1应该是-2147483648？

Question

以下是 Key Dynamic Logic 问题文件 (.key) 的条目。当我使用 Key theorem proover 运行时，该文件得到了证明。为什么这个Key动态逻辑问题得到证明，肯定将2147483647的java int增加1应该是-2147483648？

\programVariables {
        int i;
}

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

score 2 · Accepted Answer

KeyY 允许更多整数溢出选项。它们可以通过 Options-> Taclet Options -> intRules 访问（或者可能在其他版本中类似的东西）。

一个选项，在我的例子中是默认选项，忽略溢出并证明了问题，另外两个警告溢出或行为与 java 完全相同，但没有证明问题。我在 2.6.3 版本中尝试过此操作（否则它可能仍然是您的版本中的错误，或者并非总是触发，但这似乎不太可能）。

score 0 · Accepted Answer

解决方案是同时调整 Taclet 选项和证明搜索策略。

选项 -> Taclet 选项 -> intRules -> intRules:javaSemantics

证明搜索策略（选项卡）-> 算术处理-> 模型搜索或 DefOps

我觉得默认配置应该准确地反映 Java 语义，作为对 Java 进行验证的重点。我知道在某些特定情况下，偏离实际的 Java 语义会很有用，但这不应该是默认情况。

2 回答 2