KeSort:验证泛型集合的OpenJKK排序方法

验证泛型集合的 OpenJDK 排序方法

?

TimSort是Java标准库和许多其他编程框架提供的主要排序算法。我们最初的目标是用机械证明对TimSort进行功能验证。但是，在我们的验证尝试中，我们发现了一个错误，该错误导致实现因未捕获的异常而崩溃。

?

我们确定了错误发生的条件，并从中得出了一个不影响性能的无错误版本。我们正式指定新版本并验证终止以及是否存在包括错误在内的异常。这种验证是使用 KeY 机械地进行的，KeY 是最先进的 Java 交互式验证工具。我们提供对证明的详细描述和分析。证明的复杂性需要 KeY 中的扩展和新功能，包括符号状态合并。

?

我们使用最先进的Java验证工具KeY ，这是一个半自动的交互式定理证明器，几乎涵盖了完整的顺序Java。KeY通常自动找到超过99%的证明步骤，而其余的则由人类专家以交互方式执行。

?

java.util.Arrays.sort对于非基元类型的默认实现是TimSort，这是一种基于合并排序和插入排序的混合排序算法。该算法根据连续（不相交）运行（已排序的数组段）从左到右增量排序输入数组的指定段。

?

如果这些运行不够大，则使用二进制插入排序进行扩展。生成的游程的起始位置和长度存储在堆栈上。在执行期间，其中一些运行被合并，由堆栈顶部元素上的条件触发。最后，合并所有运行，生成一个排序数组。

?

TimSort 的接口由清单 1 的第 29 行和第 1 行上的两个静态方法给出。其中 a 是输入数组。参数 lo 和 hi 是必须排序的部分的下限（包括）和上限（不包括）。要对整个数组进行排序，可以省略它们，请参见第 29-31 行。

?

运行堆栈由在第 5 行构造的对象变量 ts 封装。它由对象 ts 的两个实例变量 runBase 和 runLen 表示，它们引用整数数组。这些数组 runBase 和 runLen 分别包含堆栈上的起始位置和运行长度。堆栈的（变量）大小保存在实例变量 stackSize 中。这些数组 runBase.length 和 runLen.length 的分配长度在 ts 的构造函数中根据输入数组的长度确定。

?

在每个循环迭代中，将构造下一个运行。在第 9 行中，通过识别最大下降或上升段来构建从当前位置 lo 开始的最大运行，在下降段的情况下反转顺序。如果生成的运行太短（即小于 minRun），则使用二进制插入排序将其扩展到长度为 minRun 的运行（“二进制”是指它使用二进制搜索的事实）。变量 nRemaining 表示尚未处理的元素数。在第 17 行中，通过清单 2 中的方法 pushRun 将起始位置和运行长度推到对象变量 ts 的堆栈上。

?

在第 18 行中，调用了 mergeCollapse 方法，该方法重复合并运行，直到堆栈的前三个元素满足清单 4 的第 5 行和第 4 行中给出的条件，因为 i = stackSize。实际合并是通过调用 mergeAt（n） 来完成的，它合并长度分别由 runLen[n] 和 runLen[n+1] 表示的两个运行。

在不赘述的情况下，我们注意到 mergeAt具有一个优化功能，它识别两个运行中不需要考虑合并的部分，然后从左到右或从右到左合并（分别通过调用 mergeLo 或 mergeHi），使用一个临时数组保存两者中较小的一个副本。

?

上述循环不变量是 TimSort 的基础，因此我们有时将其简称为不变量。我们还将引用满足（元素）不变量的 runLen 的特定元素，这意味着这样的元素大于下一个元素并且大于下一个元素的总和。

?

不变量用于计算 runLen 的长度，如 Sect 中更详细的解释。但是，与一些人中的建议相反，合并折叠方法通常不会重新建立不变性。

?

不变性会影响执行期间运行长度堆栈的最大大小;回想一下，此堆栈是由 runLen 和 stackSize 实现的。runLen 的长度在 TimSort 的构造函数中声明，基于输入数组 a 的长度，假设不变成立。出于性能原因，选择尽可能小的 runLen.length 至关重要。

?

我们提出了TimSort错误的两种可能的修复方法。第一种是根据对实现的操作笔和纸的最坏情况分析，使用更大的堆栈大小。虽然代码更改是微不足道的（修改分配表中的几个整数），但我们不赞成这个解决方案，因为它修复了症状，而不是 TimSort 的基本不变性被破坏的根本问题。

?

简而言之，在采用此修复程序（如在Java OpenJDK中所做的那样）时，人们使用的算法本身并不完全理解它为什么以及如何工作。我们不知道如何为算法的原始实现制定正确的不变量。在我们发现之后，事实证明该错误存在于TimSort的几个实现中。