Key验证工具的亮点在哪里？
Where does the KeY verification tool shine?
有哪些代码示例证明了KeY的实力？
详情
有这么多可用的形式化方法工具，我想知道 KeY 比它的竞争对手好在哪里，怎么样？一些可读的代码示例对于比较和理解非常有帮助。
更新
正在搜索 the KeY website, I found code examples from the book — 那里有合适的代码示例吗？
此外，我发现a paper about the bug that KeY found in Java 8’s mergeCollapse in TimSort。 TimSort 展示 Key 实力的最小代码是什么？然而，我不明白为什么模型检查无法找到错误 — 具有 64 个元素的位数组应该不会太大而无法处理。其他演绎验证工具是否同样能够找到错误？
是否已建立具有合适代码示例的验证竞赛？
这是一个非常棘手的问题，这就是为什么在一年多以前就已经提出过这个问题，但至今仍未得到回答（尽管我们来自 Key 社区的人都清楚这一点...）。
互动的力量
首先，我想指出 KeY 基本上是唯一允许对 Java 程序进行 交互式 证明的工具。尽管许多证明是自动工作的，而且我们手头有相当强大的自动策略，但有时需要交互来理解证明失败的原因（太弱甚至错误的规范、错误的代码或 "just" 证明者无能力）并添加适当的更正或强化。
验货反馈
尤其是在证明者无能力的情况下（规范和程序都可以，但问题太难证明者无法自动成功），交互是一个强大的功能。许多程序证明者（如 OpenJML, Dafny, Frama-C 等）依赖于后端的 SMT 求解器，它们为这些求解器提供或多或少的小验证条件。然后将这些条件的验证状态报告给用户，基本上是通过或失败——或超时。当断言失败时，用户可以更改程序或改进规范，但无法检查证明的状态以推断出有关错误原因的信息；这种风格有时被称为 "auto-active" 而不是交互式的。虽然这在许多情况下非常方便（尤其是当证明通过时，因为 SMT 求解器可以非常快速地证明某些东西），但可能很难从 SMT 求解器输出中挖掘信息。甚至 SMT 求解器自己也不知道为什么会出错（尽管他们可以产生反例），因为他们只是被提供了一组他们试图找到矛盾的公式。
TimSort：一个复杂的算法问题
对于你提到的TimSort证明，我们不得不使用大量的交互来让它们通过。以排序算法的 mergeHi 方法为例，它已被我所知的最有经验的 Key 高级用户之一证明。在这个 460K 证明节点的证明中，需要 3K 用户交互，包括相当多的简单交互，例如隐藏分散注意力的公式，还有 478 个量词实例化和大约 300 次切割（在线引理介绍）。该方法的代码具有许多困难的 Java 特征，例如带有标记中断的嵌套循环、整数溢出、位运算等；特别是，证明树中有很多潜在的异常和其他分支原因（这也是为什么在证明中还使用了五个手动状态合并规则应用程序）。证明该方法的工作流程基本上是尝试策略一段时间，之后检查证明状态，修剪证明并引入有用的引理以减少整体证明工作并重新开始；有时，如果策略本身无法直接找到正确的实例化，则手动实例化量词，并合并证明树分支以解决状态爆炸问题。我只想在这里声明，使用自动激活工具无法（至少目前）证明此代码，您无法以这种方式指导证明者，也无法获得了解如何指导它的正确反馈。
Key强度
最后，我想说 Key 在证明具有 复杂的量化不变量 的难题s（如排序等）方面表现出色=] 和 具有溢出的整数算法 ，以及您需要 通过 检查和 即时找到量词实例化和小引理的地方 与证明状态交互。半交互式验证的 Key 方法通常在 SMT 求解器超时的情况下也表现出色，这样用户无法判断是否有问题或需要额外的引理。
Key 当然也可以证明 "simple" 问题，但是您需要注意您的程序不包含不受支持的 Java 功能，例如浮点数或多线程；此外，如果库方法尚未在 JML 中指定，则它们可能是一个很大的问题（但这个问题也适用于其他方法）。
正在进行的开发
附带一提，我还想指出 KeY 现在越来越多地转变为一个平台，用于对不同类型的程序属性进行静态分析（不仅是 Java 程序的功能正确性).一方面，我们开发了诸如 Symbolic Execution Debugger 之类的工具，非专家也可以使用它来检查顺序 Java 程序的行为。另一方面，我们目前正忙于重构系统架构，以便为不同于 Java 的语言添加前端（在我们的内部项目 "KeY-RED" 中）；此外，正在努力使 Java 前端现代化，以便支持更新的语言功能，如 Lambdas 等。我们也在研究编译器正确性等关系属性。虽然我们已经支持第三方 SMT 求解器的集成，但我们的集成逻辑核心仍将在那里支持理解证明情况和在 SMT 和自动化失败的情况下进行手动交互。
TimSort 代码示例
既然你要了一个代码示例...我不知道 "the" 代码示例显示了 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);
}
}
验证竞赛
VerifyThis 是一个既定的基于逻辑的验证工具竞赛，将在 2019 年进行第 7 次迭代。过去事件的具体挑战可以从"archive" 我链接的网站部分。 2017 年有两支 KeY 队伍参加。那一年的总冠军是 Why3。一个有趣的观察是，有一个问题，对插入排序，作为一个简化和优化的 Java 版本出现，没有团队在现场成功验证真实世界的优化版本。然而，一个 Key 团队在事件发生后的几周内完成了该证明。我认为这突出了我的观点：困难算法问题的关键证明需要时间和专业知识，但由于策略和交互的综合力量，它们很可能会成功。
有哪些代码示例证明了KeY的实力？
详情
有这么多可用的形式化方法工具，我想知道 KeY 比它的竞争对手好在哪里，怎么样？一些可读的代码示例对于比较和理解非常有帮助。
更新
正在搜索 the KeY website, I found code examples from the book — 那里有合适的代码示例吗？
此外，我发现a paper about the bug that KeY found in Java 8’s mergeCollapse in TimSort。 TimSort 展示 Key 实力的最小代码是什么？然而，我不明白为什么模型检查无法找到错误 — 具有 64 个元素的位数组应该不会太大而无法处理。其他演绎验证工具是否同样能够找到错误？
是否已建立具有合适代码示例的验证竞赛？
这是一个非常棘手的问题，这就是为什么在一年多以前就已经提出过这个问题，但至今仍未得到回答（尽管我们来自 Key 社区的人都清楚这一点...）。
互动的力量
首先，我想指出 KeY 基本上是唯一允许对 Java 程序进行 交互式 证明的工具。尽管许多证明是自动工作的，而且我们手头有相当强大的自动策略，但有时需要交互来理解证明失败的原因（太弱甚至错误的规范、错误的代码或 "just" 证明者无能力）并添加适当的更正或强化。
验货反馈
尤其是在证明者无能力的情况下（规范和程序都可以，但问题太难证明者无法自动成功），交互是一个强大的功能。许多程序证明者（如 OpenJML, Dafny, Frama-C 等）依赖于后端的 SMT 求解器，它们为这些求解器提供或多或少的小验证条件。然后将这些条件的验证状态报告给用户，基本上是通过或失败——或超时。当断言失败时，用户可以更改程序或改进规范，但无法检查证明的状态以推断出有关错误原因的信息；这种风格有时被称为 "auto-active" 而不是交互式的。虽然这在许多情况下非常方便（尤其是当证明通过时，因为 SMT 求解器可以非常快速地证明某些东西），但可能很难从 SMT 求解器输出中挖掘信息。甚至 SMT 求解器自己也不知道为什么会出错（尽管他们可以产生反例），因为他们只是被提供了一组他们试图找到矛盾的公式。
TimSort：一个复杂的算法问题
对于你提到的TimSort证明，我们不得不使用大量的交互来让它们通过。以排序算法的 mergeHi 方法为例，它已被我所知的最有经验的 Key 高级用户之一证明。在这个 460K 证明节点的证明中，需要 3K 用户交互，包括相当多的简单交互，例如隐藏分散注意力的公式，还有 478 个量词实例化和大约 300 次切割（在线引理介绍）。该方法的代码具有许多困难的 Java 特征，例如带有标记中断的嵌套循环、整数溢出、位运算等；特别是，证明树中有很多潜在的异常和其他分支原因（这也是为什么在证明中还使用了五个手动状态合并规则应用程序）。证明该方法的工作流程基本上是尝试策略一段时间，之后检查证明状态，修剪证明并引入有用的引理以减少整体证明工作并重新开始；有时，如果策略本身无法直接找到正确的实例化，则手动实例化量词，并合并证明树分支以解决状态爆炸问题。我只想在这里声明，使用自动激活工具无法（至少目前）证明此代码，您无法以这种方式指导证明者，也无法获得了解如何指导它的正确反馈。
Key强度
最后，我想说 Key 在证明具有 复杂的量化不变量 的难题s（如排序等）方面表现出色=] 和 具有溢出的整数算法 ，以及您需要 通过 检查和 即时找到量词实例化和小引理的地方 与证明状态交互。半交互式验证的 Key 方法通常在 SMT 求解器超时的情况下也表现出色，这样用户无法判断是否有问题或需要额外的引理。
Key 当然也可以证明 "simple" 问题，但是您需要注意您的程序不包含不受支持的 Java 功能，例如浮点数或多线程；此外，如果库方法尚未在 JML 中指定，则它们可能是一个很大的问题（但这个问题也适用于其他方法）。
正在进行的开发
附带一提，我还想指出 KeY 现在越来越多地转变为一个平台，用于对不同类型的程序属性进行静态分析（不仅是 Java 程序的功能正确性).一方面，我们开发了诸如 Symbolic Execution Debugger 之类的工具，非专家也可以使用它来检查顺序 Java 程序的行为。另一方面，我们目前正忙于重构系统架构，以便为不同于 Java 的语言添加前端（在我们的内部项目 "KeY-RED" 中）；此外，正在努力使 Java 前端现代化，以便支持更新的语言功能，如 Lambdas 等。我们也在研究编译器正确性等关系属性。虽然我们已经支持第三方 SMT 求解器的集成，但我们的集成逻辑核心仍将在那里支持理解证明情况和在 SMT 和自动化失败的情况下进行手动交互。
TimSort 代码示例
既然你要了一个代码示例...我不知道 "the" 代码示例显示了 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);
}
}
验证竞赛
VerifyThis 是一个既定的基于逻辑的验证工具竞赛，将在 2019 年进行第 7 次迭代。过去事件的具体挑战可以从"archive" 我链接的网站部分。 2017 年有两支 KeY 队伍参加。那一年的总冠军是 Why3。一个有趣的观察是，有一个问题，对插入排序，作为一个简化和优化的 Java 版本出现，没有团队在现场成功验证真实世界的优化版本。然而，一个 Key 团队在事件发生后的几周内完成了该证明。我认为这突出了我的观点：困难算法问题的关键证明需要时间和专业知识，但由于策略和交互的综合力量，它们很可能会成功。