Key验证工具的亮点在哪里？

Question

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

细节

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

更新

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

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

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

Answer 1

这是一个非常困难的问题，这就是为什么在一年多前就有人问过这个问题之后还没有得到回答的原因（尽管我们来自 KeY 社区的人很清楚这一点......）。

互动的力量

首先，我想指出，KeY 基本上是唯一允许对Java 程序进行交互式证明的工具。尽管许多证明是自动工作的，而且我们手头有非常强大的自动策略，但有时需要交互才能理解证明失败的原因（太弱甚至错误的规范、错误的代码或“只是”证明者无能）并添加适当的更正或加强.

验证检查的反馈

尤其是在证明者无能力的情况下（规范和程序都可以，但是证明者自动成功的问题太难了），交互是一个强大的功能。许多程序证明者（如OpenJML、Dafny、Frama-C等）依赖后端的 SMT 求解器，它们提供或多或少的小验证条件。然后将这些条件的验证状态报告给用户，基本上是通过或失败——或超时。当断言失败时，用户可以更改程序或细化规范，但不能通过检查证明的状态来推断出问题的原因；这种风格有时被称为“自动激活”而不是交互式。虽然这在许多情况下非常方便（特别是当证明通过时，因为 SMT 求解器可以非常快速地证明某些东西），但很难挖掘 SMT 求解器输出的信息。甚至 SMT 求解器自己也不知道为什么会出错（尽管他们可以产生反例），

TimSort：一个复杂的算法问题

对于您提到的 TimSort 证明，我们必须使用大量交互来使它们通过。以排序算法的 mergeHi 方法为例，我所知道的一位最有经验的 Key 高级用户已经证明了这一点。在这个 460K 证明节点的证明中，3K 用户交互是必要的，包括很多简单的交互，比如隐藏分散注意力的公式，还有 478 个量词实例和大约 300 个切割（在线引理介绍）。该方法的代码具有许多困难的 Java 特性，例如带有标记中断的嵌套循环、整数溢出、位算术等；特别是，证明树中存在很多潜在的异常和其他分支原因（这也是为什么在证明中还使用了五个手动状态合并规则应用程序的原因）。证明这种方法的工作流程基本上是尝试一段时间的策略，然后检查证明状态，修剪证明并引入有用的引理以减少整体证明工作并重新开始；有时，如果策略无法直接找到正确的实例化，则手动实例化量词，并合并证明树分支以解决状态爆炸。我只想在这里声明，使用自动激活工具（至少目前）无法证明此代码，您无法以这种方式引导证明者，也无法获得正确的反馈以了解如何引导它。修剪证明并引入有用的引理以减少整体证明工作并重新开始；有时，如果策略无法直接找到正确的实例化，则手动实例化量词，并合并证明树分支以解决状态爆炸。我只想在这里声明，使用自动激活工具（至少目前）无法证明此代码，您无法以这种方式引导证明者，也无法获得正确的反馈以了解如何引导它。修剪证明并引入有用的引理以减少整体证明工作并重新开始；有时，如果策略无法直接找到正确的实例化，则手动实例化量词，并合并证明树分支以解决状态爆炸。我只想在这里声明，使用自动激活工具（至少目前）无法证明此代码，您无法以这种方式引导证明者，也无法获得正确的反馈以了解如何引导它。

Key的强度

最后，我想说KeY 在证明困难的算法问题（如排序等）方面很强大，在这些问题中你有复杂的量化不变量和带有溢出的整数运算，以及你需要通过检查和动态查找量词实例化和小引理与证明状态交互。半交互式验证的 Key 方法通常也适用于 SMT 求解器超时的情况，这样用户无法判断是否有问题或需要额外的引理。

Key 当然也可以证明“简单”的问题，但是您需要注意您的程序不包含不受支持的 Java 功能，如浮点数或多线程；此外，如果 JML 中尚未指定库方法，则它们可能是一个大问题（但此问题也适用于其他方法）。

持续发展

顺便说一句，我还想指出，KeY 现在越来越多地转变为一个平台，用于对不同类型的程序属性（不仅仅是 Java 程序的功能正确性）进行静态分析。一方面，我们开发了Symbolic Execution Debugger等工具非专家也可以使用它来检查顺序 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);
  }
}

验证大赛

VerifyThis是一个既定的基于逻辑验证工具的竞争，这将有第7次迭代在2019年对过去事件的具体挑战，可以从网站我联系的“档案”栏目下载。2017年有两支KeY团队参加。当年的总冠军是Why3。一个有趣的观察是，有一个问题，即配对插入排序，它是作为简化和优化的 Java 版本出现的，没有团队能够成功地在现场验证真实世界的优化版本。然而，一个 Key 团队在事件发生后的几周内完成了这个证明。我认为这突出了我的观点：困难算法问题的关键证明需要时间和专业知识，但他们'