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

Question

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

SPARK 能否用于证明，例如，Quicksort 实际上对给定的数组进行排序？

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

Answer 1

是的，可以，尽管我还不是特别擅长 SPARK-proving（目前）。 quick-sort 的工作原理如下：

1. 我们注意到快速排序背后的思想是分区。
2. A 'pivot' 被选中，这用于将 collection 分成三组：equal-to、less-than 和 greater-than。 （这种排序会影响下面的过程；我使用它是因为它与 in-order 版本不同，以说明它主要是关于分组，而不是排序。）
3. 如果 collection 的长度为 0 或 1，则您已排序；如果 2 则检查 possibly-correct 排序，然后对它们进行排序；否则继续。
4. 将枢轴移动到第一个位置。
5. 从第二个位置position扫描到最后一个位置，根据考虑的值：
   1. Less – 与 Greater 分区中的第一项交换。
   2. Greater – Null-op.
   3. Equal — 与Less的第一项交换，与Greater的第一项交换。
6. 递归调用 Less & Greater 分区。
7. 如果函数 return Less & Equal & Greater，如果过程 re-arrange in out 输入到那个顺序。

以下是您的处理方式：

1. Prove/assert 0 和 1 情况为真，
2. 证明您对 2 项的处理，
3. 证明给定一个 input-collection 和主元有一组三个值 (L,E,G) 是元素的计数 less-than/equal-to/greater-than 主元 [这可能是一个 ghost-subprogram],
4. 证明L+E+G等于你的collection,
的长度
5. 证明 [在 post-condition] 给定主元和 (L,E,G) 元组，输出符合 L 项 less-than 主元后跟 E 个相等的项目，然后 G 个更大的项目。

应该就可以了。 [IIUC]