标签: key-formal-verification

我正在与 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 …

有哪些代码示例展示了KeY的实力？

细节

有这么多形式方法工具可用，我想知道 KeY 在哪里比它的竞争对手更好，以及如何？一些可读的代码示例对于比较和理解会很有帮助。

更新

在 Key 网站上搜索，我找到了书中的代码示例——那里有合适的代码示例吗？

此外，我找到了一篇关于 KeY 在 Java 8 的 mergeCollapse in TimSort 中发现的错误的论文。TimSort 中展示了 KeY 实力的最小代码是什么？然而，我不明白为什么模型检查应该找不到错误——一个包含 64 个元素的位数组不应该太大而无法处理。其他演绎验证工具是否也能找到错误？

是否存在具有合适代码示例的既定验证竞赛？