时间戳

首页 > 解决方案 > SPARK 可以用来证明 Quicksort 确实排序了吗？

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

问题描述

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

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

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

标签： adaformal-verificationspark-adaspark-2014

解决方案

是的，它可以，虽然我不是特别擅长 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]

推荐阅读