key-formal-verification - Key 难以处理三元运算符

Question

我正在和 KeY ( https://www.key-project.org ) 一起玩一个教学项目。

一方面，我很高兴 KeY 轻松证明了以下带 jml 注释的 Java 代码的正确性

/*@ ensures ((\result == a) || (\result == b));                                                                        
  @ ensures ((\result >= a) && (\result >= b));                                                                        
*/
public int max(int a, int b) {
    if(a <= b)
            return b;
    else
            return a;
}

但另一方面，我出人意料地无法证明以下等效程序的正确性

/*@ ensures ((\result == a) || (\result == b));                                                                        
  @ ensures ((\result >= a) && (\result >= b));                                                                        
*/
public int max(int a, int b) {
    return (a <= b) ? b : a;
}

有人知道我是否遗漏了什么吗？

Answer 1

感谢您查看 Key。

所述示例在我的 PC 上使用 Key 2.6.3 立即自动验证。
Key 有许多验证引擎所依赖的设置。也许其中一些设置使 Key 失败。

您应该从“证明搜索策略”面板中按“选择预定义”按钮，然后
再试一次。它应该工作。

您也可以考虑删除家中的目录“.key”
目录以完全重置 Key 的设置。也许一些设置
阻止工具成功。

希望这可以帮助!