5

有哪些代码示例可以展示KeyY的强大功能？

细节

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

更新

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

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

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

4

1 回答 1

6

这是一个非常难的问题，这就是为什么它在一年多前被问到之后仍未得到回答（尽管我们来自 Key 社区的人很清楚......）。

互动的力量

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

证明检查的反馈

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

TimSort：一个复杂的算法问题

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

Key的实力

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

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

持续发展

顺便说一句，我还想指出，KeyY 现在越来越多地转变为一个平台，用于对不同类型的程序属性（不仅仅是 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是一项针对基于逻辑的验证工具的既定竞赛，将于 2019 年进行第 7 次迭代。过去事件的具体挑战可以从我链接的网站的“存档”部分下载。2017 年有两支 KeyY 团队参加。当年的总冠军是Why3。一个有趣的观察是，有一个问题，Pair Insertion Sort，它是作为简化和优化的 Java 版本出现的，没有团队成功地在现场验证真实世界的优化版本。然而，Key 团队在事件发生后的几周内完成了该证明。我认为这突出了我的观点：困难算法问题的关键证明需要时间并且需要专业知识，但他们

于 2018-12-17T08:41:32.543 回答