verification - KeY验证工具在哪里发光？

Question

有哪些代码示例可以证明KeY的优势？

细节

有了这么多的正式方法工具，我想知道KeY在哪些方面比其竞争对手更好，以及如何？一些可读的代码示例对于比较和理解非常有帮助。

更新

搜索the KeY website时，我发现了the book中的代码示例-那里是否有合适的代码示例？

此外，我找到了a paper about the bug that KeY found in Java 8’s 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是基于逻辑的验证工具的既定竞赛，它将在2019年进行第七次迭代。可以从我链接的网站的“存档”部分下载过去事件的具体挑战。 2017年，有两个KeY团队参加了比赛。当年的总冠军是Why3。有趣的发现是，存在一个问题，“对插入排序”，它是经过简化和优化的Java版本，没有一个团队能够在现场成功验证实际的优化版本。但是，KeY团队在事件发生后的几周内完成了该证明。我认为这凸显了我的观点：困难算法问题的KeY证明需要花费时间并需要专业知识，但是由于策略和交互的强大结合，它们很可能会成功。