gpt4 book ai didi

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

转载 作者:行者123 更新时间:2023-12-02 00:57:01 25 4
gpt4 key购买 nike

我正在和 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;
}

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

最佳答案

感谢您查看 Key。

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

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

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

希望这可以帮助!

关于key-formal-verification - Key 难以处理三元运算符,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/53605000/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com