用于选择排序的程序正确性，不变性和谓词逻辑

Question

我正在尝试证明Selection排序的正确性，在这种情况下，我应该仅使用数学谓词逻辑来证明程序的正确性，我发现很难将下面给出的英语语句作为谓词编写并继续进行证明遵循推理规则的正确性，

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]中的条目。

Answer 1

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

要说一个子数组已排序，我们可以这样说：

“对于子数组中的任何一对索引j

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].