哪些代码示例证明了KeY的实力?
详细信息
有这么多可用的形式化方法工具,我想知道KeY在哪里比它的竞争对手更好,以及如何更好?一些可读的代码示例将非常有助于进行比较和理解。
更新
在KeY网站上搜索,我发现了书中的代码示例——那里有合适的代码示例吗?
此外,我在TimSort中发现了一篇关于KeY在Java8的mergeCollapse中发现的错误的论文。TimSort中展示KeY实力的最小代码是什么?然而,我不明白为什么模型检查不能找到错误——一个有64个元素的位数组不应该太大而无法处理。其他演绎验证工具是否也同样能够发现错误?
是否存在具有合适代码示例的既定验证竞争?
这是一个非常困难的问题,这就是为什么在一年多前就已经被问到了,但还没有得到回答(尽管我们KeY社区的人都很清楚…)。
交互的力量
首先,我想指出的是,KeY基本上是唯一允许Java程序的交互式证明的工具。尽管许多证明是自动工作的,而且我们手头有非常强大的自动策略,但有时需要交互来理解证明失败的原因(太弱甚至错误的规范、错误的代码或"只是"证明人的无能),并添加适当的更正或加强。
来自验证检查的反馈
特别是在证明者无能力的情况下(规范和程序都可以,但问题太难了,证明者无法自动成功),交互是一个强大的功能。许多程序证明程序(如OpenJML、Dafny、Frama-C等)在后端依赖SMT解算器,它们提供了或多或少的小验证条件。然后将这些条件的验证状态报告给用户,基本上是通过或失败或超时。当断言失败时,用户可以更改程序或细化规范,但不能检查证据的状态来推断出问题原因的信息;这种风格有时被称为"自动激活",而不是交互式的。虽然这在很多情况下都很方便(尤其是当证明通过时,因为SMT求解器可以非常快速地证明某些东西),但很难挖掘SMT求解器的输出以获取信息。即使是SMT求解者自己也不知道为什么出了问题(尽管他们可以给出一个反例),因为他们只是得到了一组公式,试图找到矛盾。
TimSort:一个复杂的算法问题
对于你提到的TimSort证明,我们必须使用大量的交互来让它们通过。例如,排序算法的mergeHi方法,我所知道的一位最有经验的KeY超级用户已经证明了这一点。在这个460K证明节点的证明中,3K用户交互是必要的,包括很多简单的交互,比如隐藏分散注意力的公式,还有478个量词实例化和大约300个剪切(在线引理介绍)。该方法的代码具有许多困难的Java特性,如带有标记中断的嵌套循环、整数溢出、位算术等等;特别是,在证明树中有很多潜在的异常和其他分支原因(这就是为什么在证明中还使用了五个手动状态合并规则应用程序)。证明这种方法的工作流程基本上是对策略进行一段时间的尝试,然后检查证明状态,修剪证明并引入一个有用的引理,以减少总体证明工作并重新开始;偶尔,如果策略本身无法直接找到正确的实例化,则会手动实例化量词,并合并证明树分支以解决状态爆炸问题。我只想在这里声称,用自动激活工具(至少目前)不可能证明这个代码,在自动激活工具中,你无法以这种方式指导证明者,也无法获得正确的反馈来了解如何指导它。
KeY的强度
最后,我想说,KeY在证明困难的算法问题s(如排序等)方面很强,其中你有复杂的量化不变量和带有溢出的整数算法,并且你需要通过检查和与证明状态交互来动态地找到量词实例化和小引理。半交互式验证的KeY方法通常也适用于SMT求解器超时的情况,这样用户就无法判断是出了问题还是需要额外的引理。
KeY当然也可以证明"简单"的问题,但是你需要注意你的程序不包含不支持的Java功能,比如浮点数或多线程;此外,如果库方法还没有在JML中指定,那么库方法可能会成为一个很大的问题(但这个问题也适用于其他方法)。
正在进行的开发
顺便说一句,我还想指出,KeY现在越来越多地被转换为一个平台,用于静态分析不同类型的程序属性(不仅仅是Java程序的功能正确性)。一方面,我们开发了符号执行调试器等工具,非专家也可以使用它来检查顺序Java程序的行为。另一方面,我们目前正忙于重构系统架构,以便为不同于Java的语言添加前端(在我们的内部项目"KeY RED"中);此外,目前正在努力实现Java前端的现代化,以便支持Lambdas等更新的语言功能。我们也在研究关系属性,比如编译器的正确性。虽然我们已经支持集成第三方SMT解决方案,但我们的集成逻辑核心仍将支持理解SMT和自动化失败的情况下的验证情况和手动交互。
TimSort代码示例
既然你要求一个代码示例。。。我想不出"这个"代码例子显示了KeY的实力,但也许是为了让你了解TimSort算法中mergeHi的复杂性,这里有一个简短的摘录和一些评论(整个方法大约有100行代码):
private void mergeHi(int base1, int len1, int base2, int len2) {
// ...
T[] tmp = ensureCapacity(len2); // Method call by contract
System.arraycopy(a, base2, tmp, 0, len2); // Manually specified library method
// ...
a[dest--] = a[cursor1--]; // potential overflow, NullPointerException, ArrayIndexOutOfBoundsException
if (--len1 == 0) {
System.arraycopy(tmp, 0, a, dest - (len2 - 1), len2);
return; // Proof branching
}
if (len2 == 1) {
// ...
return; // Proof branching
}
// ...
outer: // Loop labels...
while (true) {
// ...
do { // Nested loop
if (c.compare(tmp[cursor2], a[cursor1]) < 0) {
// ...
if (--len1 == 0)
break outer; // Labeled break
} else {
// ...
if (--len2 == 1)
break outer; // Labeled break
}
} while ((count1 | count2) < minGallop); // Bit arithmetic
do { // 2nd nested loop
// That's one complex statement below...
count1 = len1 - gallopRight(tmp[cursor2], a, base1, len1, len1 - 1, c);
if (count1 != 0) {
// ...
if (len1 == 0)
break outer;
}
// ...
if (--len2 == 1)
break outer;
count2 = len2 - gallopLeft(a[cursor1], tmp, 0, len2, len2 - 1, c);
if (count2 != 0) {
// ...
if (len2 <= 1)
break outer;
}
a[dest--] = a[cursor1--];
if (--len1 == 0)
break outer;
// ...
} while (count1 >= MIN_GALLOP | count2 >= MIN_GALLOP);
// ...
} // End of "outer" loop
this.minGallop = minGallop < 1 ? 1 : minGallop; // Write back to field
if (len2 == 1) {
// ...
} else if (len2 == 0) {
throw new IllegalArgumentException(
"Comparison method violates its general contract!");
} else {
System.arraycopy(tmp, 0, a, dest - (len2 - 1), len2);
}
}
验证竞争
Verify这是一项针对基于逻辑的验证工具的既定竞赛,将于2019年进行第7次迭代。过去事件的具体挑战可以从我链接的网站的"档案"部分下载。2017年,两个KeY团队参加了该活动。那年的总冠军是Why3。一个有趣的观察结果是,有一个问题,Pair Insertion Sort,它是一个简化和优化的Java版本,没有团队成功地在现场验证了真实世界的优化版本。然而,KeY团队在活动结束后的几周内完成了这一证明。我认为这突出了我的观点:困难算法问题的KeY证明需要时间,需要专业知识,但由于策略和交互的综合力量,它们很可能会成功。