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

问题描述

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

SPARK 可以用来证明，例如，Quicksort 实际上对给定的数组进行排序吗？

（很想看一个例子，假设这很简单）

解决方法

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

1. 我们注意到快速排序背后的想法是分区。
2. 选择了一个“枢轴”，这用于将集合分成三组：等于、小于和大于。 （这个排序会影响下面的过程；我使用这个是因为它与有序版本不同，以说明它主要是关于分组，而不是排序。）
3. 如果集合的长度为 0 或 1，则您已排序； if 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. 证明 [in the post-condition] 给定枢轴和 (L,G) 元组，输出符合 L 项小于枢轴，后跟 E 项相等，然后是更大的 G 项。

这应该可以做到。 [IIUC]