java - 为两个嵌套的while循环查找循环不变量java

Question

我对不变量有点熟悉，我或多或少可以在一个小循环中找到它。在为以下 java 伪代码求解不变量时，我感到很困惑。谁能帮忙：

Input: an array A
i <- length(A)
# outer invariant
while i != 0 do
  k <- i
  j <- i - 1
  # inner invariant
  while j != 0 do
    if A[j] > A[k] then
      k <- j
    j <- j - 1
    # inner invariant
  swap(A, i, k)
  i <- i - 1
# outer invariant

Answer 1

您应该从内部循环开始计算嵌套循环的不变量：

while (j != 0) {
    if (A[j] > A[k]) {
        k = j;
    }
    j--;
}

你可以观察到

A[k] >= A[x], for any (j < x) && (x <= i)

在循环结束时，j == 0，因此使用Hoare Triplele作为while循环，您可以在内部循环结束时声明

A[k] >= A[x], for any (0 < x <= i)

A[k]这是另一种说法MAX(A[0:i])。

现在您可以继续外循环：由于i从A.length下到零进行，因此不变量将是

A[y] < A[x], for any (y >= i) for any (y < x <= Length(A))

再次使用 Hoare Trippe，您可以得出在退出外循环时数组A按升序排序：

A[y] < A[x], for any (y >= 0) for any (y < x <= Length(A))

Answer 2

你的代码片段可以像下面这样缩减和格式化（你习惯 C 语言语法吗？）：

for ( i = n; i > 0 ; i -- ) {
    for ( j = i - 1 ; j > 0 ; j -- ) {
        // Constant time instructions here symbolized by c
    }
}

从上面的片段中传递给 Sigma Notation 不会太麻烦：