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 有许多验证引擎所依赖的设置。也许其中一些设置会导致 KeyY 失败。

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

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

希望这可以帮助！