Zacznijmy od niezmiennika pierwszej pętli
∀ k ∀ m (k < l ∧ l ≤ m ≤ N+1) ⇒ A[k]+...+A[m-1] <> W ∧
∀ m (l ≤ m < p) ⇒ A[l]+...+A[m-1] < W ∧
1 ≤ l ≤ p ≤ N+1 ∧ N,W > 0 ∧ suma=A[l]+....A[p-1] ∧
A jest tablicą o wartościach dodatnich
oznaczanego przez N(l,p,suma). Mówi ono, że wszystkie segmenty o początku mniejszym od l i dowolnym końcu mają sumy różne od W, i że wszystkie segmenty o początku w l i końcu mniejszym od p mają sumy mniejsze niż W. Poza tym opisane są zależności między 1, l, p, N i suma.
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,W > 0, A jest tablicą o wartościach dodatnich
1: l:=1; p:=1; suma:=0;
// N(l,p,suma)
2: <b>while</b> (suma <> W) <b>and</b> (p <= N) <b>do</b>
// N(l,p,suma) ∧ (suma <> W) ∧ (p ≤ N)
3: <b>if</b> suma < W <b>then</b> <b>begin</b>
// N(l,p,suma) ∧ (suma < W) ∧ (p ≤ N)
4: suma:=suma+A[p]; p:=p+1;
// N(l,p,suma) <b>end</b>
5: <b>else</b> <b>begin</b>
// N(l,p,suma) ∧ (suma > W) ∧ (p ≤ N)
6: suma:= suma-A[l]; l:=l+1;
// N(l,p,suma)
7: <b>end</b>;
// N(l,p,suma) ∧ (suma=W ∨ p = N+1)
8: <b>while</b> (suma > W) <b>do</b> <b>begin</b>
// N(l,p,suma) ∧ p = N+1 ∧ suma > W
9: suma:= suma-A[l];
l:=l+1;
10: <b>end</b>;
// N(l,p,suma) ∧ (suma=W ∨ (p=N+1 ∧ suma < W))
11: znalezione:=(suma=W);
//znalezione ⇔ (∃ l ∃ p 1 ≤ l ≤ p ≤ N+1 ∧ A[l]+...A[p-1] = W)
1 Korzystamy z reguły na przypisanie. N(l,p,suma) z wartościami l=1, p=1, suma=0 jest równe
∀ k ∀ m (k < 1 ∧ 1 ≤ m ≤ N+1) ⇒ A[k]+...+A[m-1] <> W ∧
∀ m (l ≤ m < 1) ⇒ A[l]+...+A[m-1] < W ∧
1 ≤ 1 ≤ 1 ≤ N+1 ∧ N,W > 0 ∧ 0=0 ∧
A jest tablicą o wartościach dodatnich
i jest trywialnie prawdziwe.
2 Korzystamy z reguły na while; trzeba pokazać, że N(l,p,suma) jest niezmiennikiem ciała pętli, czyli że zaczynając z N(l,p,suma) ∧ suma <> W ∧ p ≤ N po wykonaniu pętli zachodzi N(l,p,suma).
3 Korzystamy z reguły na if; trzeba zrobić osobne sprawdzenia dla każdej gałęzi.
4 Zgodnie z regułą na przypisanie, musimy dowieść, że N(l,p,suma) ∧ (suma < W) ∧ (p ≤ N) wynika N(l,p+1,suma+A[p]),czyli
∀ k ∀ m (k < l ∧ l ≤ m ≤ N+1) ⇒ A[k]+...+A[m-1] <> W ∧
∀ m (l ≤ m < p+1) ⇒ A[l]+...+A[m-1] < W ∧
1 ≤ l ≤ p+1 ≤ N+1 ∧ N,W > 0 ∧
suma+A[p]=A[l]+....A[p] ∧
A jest tablicą o wartościach dodatnich
Jedyna część, która nie jest oczywista, to że A[l]+...A[p-1] < W, ale to wynika z (suma < W) i suma=A[l]+....A[p-1]
5 W drugiej gałęzi wiemy dodatkowo, że suma > W
6 Zgodnie z regułą na przypisanie, musimy dowieść, że N(l,p,suma) ∧ (suma > W) ∧ (p ≤ N) wynika N(l+1,p,suma-A[l]),czyli
∀ k ∀ m (k < l+1 ∧ l+1 ≤ m ≤ N+1) ⇒ A[k]+...+A[m-1] <> W ∧
∀ m (l+1 ≤ m < p) ⇒ A[l+1]+...+A[m-1] < W ∧
1 ≤ l+1 ≤ p ≤ N+1 ∧ N,W > 0 ∧
suma-A[l]=A[l+1]+....A[p-1] ∧
A jest tablicą o wartościach dodatnich
Spójrzmy najpierw na pierwszą linię niezmiennika: dla k < l, A[k]+...+A[m-1] <> W z założenia; dla k=l mamy pokazać że dla dowolnych m A[l]+...+A[m-1] <> W. Ale wiemy, że dla m < p+1 zachodzi A[l]+...A[m-1] < W i że A[l]+...A[p-1] > W (bo suma > W). Tym bardziej więc dla m > p+1 będzie A[l]+...A[m-1] > W (bo A jest dodatnia).
Dla uzasadnienia drugiej linii wystarczy zauważyć, że gdy skracamy segment o wartości mniejszej niż W, to jego wartość spada, bo A jest tablica dodatnią.
Pozostaje uzasadnienie l+1 ≤ p. Ponieważ suma > W to l < p, a więc też l+1 ≤ p.
7 Po pętli while wiemy, że zachodzi N(l,p,suma) i zaprzeczenie dozoru, czyli (suma=W ∨ p > N). Z niezmiennika wiemy, że p ≤ N+1, a więc musi być p=N+1.
8 Pokażemy, że N(l,p,suma) ∧ (suma=W ∨ p = N+1) jest niezmiennikiem tej pętli.
9 Zauważmy najpierw, że N(l,p,suma) ∧ (suma=W ∨ p = N+1) ∧ suma > W jest równoważne N(l,p,suma) ∧ p = N+1 ∧ suma > W.
Zgodnie z regułą na przypisanie, musimy dowieść, że N(l,p,suma) ∧ p = N+1 ∧ suma > W implikuje N(l+1,p,suma-A[l]) ∧ (suma-A[l]=W ∨ p = N+1). Zdanie N(l+1,p,suma-A[l]) dowodzi się tak, jak w punkcie 6. Ponieważ p =N+1, to zachodzi (suma-A[l]=W ∨ p = N+1).
10 Po wyjściu z pętli mamy N(l,p,suma) ∧ (suma=W ∨ p = N+1) i zaprzeczenie dozoru, czyli suma ≤ W, a więc N(l,p,suma) ∧ (suma=W ∨ (p=N+1 ∧ suma < W)).
11 Pozostaje udowodnić, że N(l,p,suma) ∧ (suma=W ∨ (p=N+1 ∧ suma < W)) implikuje (suma=W) ⇔ (∃ l ∃ p 1 ≤ l ≤ p ≤ N+1 ∧ A[l]+...A[p-1] = W) .
Jeśli suma=W to z N(l,p,suma), oczywiście wynika istnienie odpowiednich l i p. Jeśli suma <> W, to z założenia mamy p=N+1 i suma < W. I wtedy z niezmiennika wiemy, że
- segmenty o początkach mniejszych niż l mają sumy różne od W,
- segmenty o początkach w l i końcach mniejszych niż p mają sumy mniejsze niż W,
- segment o początku w l i końcu w p ma sumę mniejszą W,
- a więc też segmenty o początkach wiekszych od l i dowolnych końcach mają sumy mniejsze niż W.
Czyli nie isnieje segment o sumie równej W.