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 立即自动验证。KeyY 有许多验证引擎所依赖的设置。也许其中一些设置使 Key 失败。

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

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

希望这可以帮助！