java - Javaのネストされた2つのwhileループのループ不変式を見つける

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 Tripleを使用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
    }
}

上記のフラグメントからシグマ記法への受け渡しはそれほど面倒ではありません。