0

我试图证明选择排序的正确性，其中我应该只使用数学谓词逻辑来证明程序的正确性，我发现很难将下面给出的英语语句写成谓词并继续证明正确性遵循推理规则，

void sort(int [] a, int n) {
  for (int i=0; i<n-1; i++) {
    int best = i;
    for (int j=i; j<n; j++) {
      if (a[j] < a[best]) {
        best = j;
      }
    }
    swap a[i] and a[best];
  }
}

我必须在谓词中写的语句是，

  1. a[0...i-1]已排序

  2. 中的所有条目a[i..n-1]都大于或等于 中的条目a[0..i-1]。

4

1 回答 1

0

关于子数组a[0...i-1]的语句 like 实际上是关于该子数组中所有元素的语句，因此您需要使用通用量词将其转换为关于单个成员的语句。

要说子数组已排序，我们可以这样说：“对于子数组中的任何一对索引 j < k，这些索引处的值是有序的。”

For all 0 <= j < i-1, for all j < k <= i-1, arr[j] <= arr[k].

第二个属性已经写成关于两个子数组的“所有条目”的语句，但让我们更明确地说：“对于第一个子数组中的任何一对索引 j 和第二个子数组中的 k，第一个子数组中的值是小于或等于第二个子数组中的值。”

For all 0 <= j <= i-1, for all i <= k <= n-1, arr[j] <= arr[k].
于 2019-11-25T14:10:28.383 回答