Główną trudnością jest wymyślenie odpowiedniego niezmiennika pętli while. Tu, będzie to zdanie:
∀ i (1 ≤ i < m) ⇒ A[i] < 0 ∧
∀ j (m ≤ j < r) ⇒ A[j] = 0 ∧
∀ k (w < j ≤ N) ⇒ A[k] > 0 ∧
1 ≤ m ≤ r ∧ r-1 ≤ w ≤ N ∧ N > 0
oznaczane przez N(m,r,w). Poniżej znajduje się program wraz z anotacjami i dowody, że anotacje wraz z kodem który otaczają są poprawnymi trójkami Hoare'a.
// N > 0
1:m:=1; r:=1; w:=N;
// N(m,r,w)
2:while r <= w do
// N(m,r,w) ∧ r ≤ w
3: if A[r]=0 then
// N(m,r,w) ∧ r ≤ w ∧ A[r] = 0
// N(m,r+1,w)
4: r:=r+1
// N(m,r,w)
5: else
6: if A[r]<0 then begin
// N(m,r,w) ∧ r ≤ w ∧ A[r] < 0
7: pom:=A[r]; A[r]:=A[m]; A[m]:=pom;
// N(m+1,r+1,w)
8: m:=m+1; r:=r+1;
// N(m,r,w)
end
9: else begin
// N(m,r,w) ∧ r ≤ w ∧ A[r] > 0
10: pom:=A[r]; A[r]:=A[w]; A[w]:=pom;
// N(m,r,w-1)
11: w:=w-1;
// N(m,r,w)
12: end;
// N(m,r,w) ∧ r-1=w
1 Korzystamy z reguły na przypisanie. N(m,r,w) z wartościami m=1, r=1, w=1 jest równe
∀ i (1 ≤ i < 1) ⇒ A[i] < 0 ∧
∀ j (m ≤ j < 1) ⇒ A[j] = 0 ∧
∀ k (N < j ≤ N) ⇒ A[k] > 0 ∧
1 ≤ 1 ≤ 1 ∧ 0 ≤ N ≤ N ∧ N > 0
i jest trywialnie prawdziwe.
2 Korzystamy z reguły na while; trzeba pokazać, że N(m,r,w) jest niezmiennikiem ciała pętli, czyli że zaczynając z N(m,r,w) ∧ r ≤ w po wykonaniu pętli zachodzi N(m,r,w).
3 Korzystamy z reguły na if; trzeba pokazać, że z N(m,r,w) ∧ r ≤ w po wykonaniu każdej gałęzi zachodzi N(m,r,w).
4 Korzystając z reguły na przypisanie otrzymujemy, że N(m,r+1,w) powinno być prawdziwe przed instrukcją 4. A więc musimy dowieść implikacji
(N(m,r,w) ∧ r ≤ w ∧ A[r] = 0) ⇒ N(m,r+1,w)
Rozpatrując części N(m,r+1,w) widzimy, że
∀ i (1 ≤ i < m) ⇒ A[i] < 0 ∧
∀ k (w < j ≤ N) ⇒ A[k] > 0 ∧
1 ≤ m ∧ w ≤ N ∧ N > 0
wynikają trywialnie z N(m,r,w). Mamy też
∀ j (m ≤ j < r+1) ⇒ A[j] = 0
bo A[r] = 0.Ponieważ r ≤ w to
r+1-1 ∧ w
a ponieważ m ≤ r to
m ≤ r+1
5 W drugiej gałęzi instrukcji warunkowej z 3 znajduje się if. Schodząc do jego podgałęzi dodajemy do założeń, że A[r] <> 0.
6 Ciało podgałęzi spełniającej warunek A[r] < 0 składa się z dwóch grup przypisań.
7 Trzeba pokazać, że z N(m,r,w) ∧ r ≤ w ∧ A[r] < 0 wynika N(m+1,r+1,w) z zamienionymi wartościami A[r] i A[m]. Dokładniej, uzupełniając program o brakujące anotacje zgodnie z regułą na przypisanie, przed instrukcją A[m]:=pom mamy
∀ i (1 ≤ i < m) ⇒ A[i] < 0 ∧ pom < 0 ∧
∀ j (m ≤ j < r) ⇒ A[j] = 0 ∧ A[r] = 0 ∧
∀ k (w < j ≤ N) ⇒ A[k] > 0 ∧
1 ≤ m+1 ≤ r+1 ∧ r ≤ w ≤ N ∧ N > 0
przed A[r]:=A[m]
∀ i (1 ≤ i < m) ⇒ A[i] < 0 ∧ pom < 0 ∧
∀ j (m ≤ j < r) ⇒ A[j] = 0 ∧ A[m] = 0 ∧
∀ k (w < j ≤ N) ⇒ A[k] > 0 ∧
1 ≤ m+1 ≤ r+1 ∧ r ≤ w ≤ N ∧ N > 0
a przed pom:= A[r]
∀ i (1 ≤ i < m) ⇒ A[i] < 0 ∧ A[r] < 0 ∧
∀ j (m ≤ j < r) ⇒ A[j] = 0 ∧ A[m] = 0 ∧
∀ k (w < j ≤ N) ⇒ A[k] > 0 ∧
1 ≤ m+1 ≤ r+1 ∧ r ≤ w ≤ N ∧ N > 0
czyli coś co łatwo wynika z N(m,r,w) ∧ r ≤ w ∧ A[r] < 0.
8 Jest to trywialne użycie reguły na przypisanie.
9 Ciało podgałęzi spełniającej warunek A[r] > 0 składa się znów z dwóch grup przypisań.
10 Trzeba pokazać, że z N(m,r,w) ∧ r ≤ w ∧ A[r] > 0
wynika N(m,r,w-1) z zamienionymi wartościami A[r] i A[w] czyli
∀ i (1 ≤ i < m) ⇒ A[i] < 0 ∧
∀ j (m ≤ j < r) ⇒ A[j] = 0 ∧
∀ k (w < j ≤ N) ⇒ A[k] > 0 ∧ A[r] > 0 ∧
1 ≤ m ≤ r ∧
r-1 ≤ w-1 ≤ N ∧ N > 0
co jest łatwe.
11 Jest to trywialne użycie reguły na przypisanie.
12 Z reguły na while wiemy, że zachodzi N(m,r,w) i zaprzeczenie dozoru w while czyli r > w. Z niezmiennika wiemy, że r-1 ≤ w, a więc musi być r-1=w.
