Najpierw musimy odgadnąć asercję, którą można wpisać pomiędzy początkowe przypisania a pętlę:
x := 1;
y := 0;
while x <= n do
(
y := y + x;
x := x + 1
)
Możemy na przykład "przeciągnąć" asercję początkową wprzód, otrzymując
.
Teraz wystarczy dowieść następujące dwie trójki Hoare'a:
x := 1;
y := 0;
while x <= n do
(
y := y + x;
x := x + 1
)
Zajmijmy się tą ostatnią.
Naszym zadaniem jest teraz odkrycie niezmiennika
takiego, że zachodzą poniższe dwie implikacje:
oraz prawdziwa jest trójka:
while x <= n do
(
y := y + x;
x := x + 1
)
Aby dowieść tej ostatniej, musimy pokazać:
y := y + x;
x := x + 1
Formalnie rzecz biorąc, powinniśmy teraz zgadnąć asercję, która może być wpisana pomiędzy dwie instrukcje przypisania:
y := y + x;
x := x + 1
a następnie niezależnie dowieść poprawność każdej z dwóch nstrukcji.
Ale w "odgadnięciu" pomoże nam reguła dla przypisania, która, intuicyjnie mówiąc, daje sposób na "przeciągnięcie" asercji w tył.
Jeśli zastosujemy ją do drugiego przypisania "x := x + 1", otrzymamy:
y := y + x;
x := x + 1
Teraz musimy tylko pokazać trójkę:
y := y + x;
Użyjmy więc ponownie reguły dla przypisania, otrzymując:
// tę implikację należy udowodnić
y := y + x;
Skoro dwie asercje spotkały się, wystarczy teraz udowodnić implikację.
I tak dalej. To znaczy, podobnie postępujemy z pozostałymi przypisaniami. A wszędzie, gdzie spotykają się dwie asercje, dowodzimy implikacji.
Podsumowując, poniższe anotacje całego programu powinny stanowić dowód poprawności częściowej:
x := 1;
y := 0;
// 1
while x <= n do
(
// 2
y := y + x;
x := x + 1
)
// 3
A jedyne co pozostaje do zrobienia to tylko udowodnienie następujących implikacji:

![{\displaystyle N\land x\leq n\,\implies \,N[x\mapsto x{+}1][y\mapsto y{+}x]}](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/png/2e209b7c3ffcb8b612ee23b79e59b92f5ac90a99)

Co ciekawe, to wszystko uczyniliśmy nie wiedząc wogóle, jaki jest niezmiennik pętli!
Ale nadszedł wreszcie moment, w którym powinniśmy taki niezmiennik podać.
Musimy go odgadnąć poprzez staranną obserwację tego, co dzieje się wewnątrz pętli.
Należy oczywiście uwzględnić również implikacje, które wypisaliśmy powyżej.
Spróbujmy
.
Nierówność
jest niezbędna. Potrzebujemy jej po to, aby z
wywnioskować
.
Implikacje są prawdziwe, więc niezmiennik został wybrany poprawnie.
Zauważmy, że niezmiennik nie zawiera wymagania
. Moglibyśmy je jednak dodać, otrzymując
.
Wszystkie implikacje pozostają prawdziwe, więc jest to też poprawny wybór. Ponadto wiedząc, że
możemy, dla czytelności, zapisywać niezmiennik w meta-notacji:
Pytanie: dlaczego nie potrzebowaliśmy warunku
? Jak będzie działał nasz program, jeśli zmienną x zainicjujemy wartością ujemną (zamiast x := 1), np. x := -2, y := 3?
Notacja:
Niezmiennik pętli będziemy zwykle wpisywać pomiędzy słowem kluczowym while a dozorem pętli. W naszym przypadku otrzymamy następujące anotacje:
x := 1;
y := 0;
// 1
while
x <= n do
(
...
Wariant:
Wróćmy na chwilę do naszej pierwszej decyzji, polegającej na wpisaniu następującej asercji
pomiędzy początkowe przypisania a pętlę. Mogliśmy uczynić inaczej i wpisać w to miejsce po prostu niezmiennik
. Wtedy należałoby wykazać:
x := 1;
y := 0;
co można, za pomocą znanego nam już "przepychania w tył", zredukować do udowodnienia implikacji:
// 1
x := 1;
y := 0;
Ostatecznie, anotacje programu wyglądałyby tak:
// 1
x := 1;
y := 0;
while
x <= n do
(
// 2
y := y + x;
x := x + 1
)
// 3
a pierwsza z trzech implikacji to:
.