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

Question

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

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

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

Answer 1

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

1. 我们注意到快速排序背后的想法是分区。
2. 选择了一个“枢轴”，它用于将集合划分为三组：等于、小于和大于。（这个排序会影响下面的过程；我使用它是因为它不同于按顺序的版本来说明它主要是关于分组，而不是排序。）
3. 如果集合是0或1长度，那么你是排序的；如果2然后检查并可能更正排序并对其进行排序；否则继续。
4. 将枢轴移动到第一个位置。
5. 根据考虑的值，从第二个位置扫描到最后一个位置：
   1. LessGreater– 与分区中的第一项交换。
   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]