SPARK 可以用来证明 Quicksort 确实排序了吗？

Question

我不是 SPARK 的用户。我只是想了解语言的功能。

是否可以使用 SPARK 来证明，例如，Quicksort 实际上对给它的数组进行了排序？

（希望看到一个例子，假设这很简单）

Answer 1

是的，它可以，虽然我不是特别擅长 SPARK 证明（目前）。以下是快速排序的工作原理：

1. 我们注意到快速排序背后的想法是分区。
2. 选择了一个“枢轴”，用于将集合划分为三组：等于、小于和大于。 （这种排序会影响下面的过程；我使用它是因为它不同于按顺序的版本来说明它主要是关于分组，而不是排序。）
3. 如果集合的长度是0或1，那么你是排序的；如果2 然后检查并可能更正排序并对其进行排序；否则继续。
4. 将枢轴移动到第一个位置。
5. 从第二个位置扫描到最后一个位置，具体取决于所考虑的值：
   1. Less – 与Greater 分区中的第一项交换。
   2. Greater – 空操作。
   3. Equal — 与Less 的第一项交换，与Greater 的第一项交换。
6. 递归调用Less 和Greater 分区。
7. 如果函数返回 Less & Equal & Greater，如果过程将 in out 输入重新排列到该顺序。

以下是你做事的方式：

1. 证明/断言 0 和 1 案例为真，
2. 证明您对2 项目的处理能力，
3. 证明给定输入集合和枢轴有一组三个值(L,E,G)，它们是小于/等于/大于枢轴的元素的计数[这可能是一个幽灵子程序],
4. 证明L+E+G 等于您的集合的长度，
5. 证明[在后置条件中]给定枢轴和(L,E,G)元组，输出符合L小于枢轴的项目，然后是E相等的项目，然后是G项目更大。

应该这样做。 [IIUC]