Logika Hoare’a

Szablon:Dopracować Logika Hoare’a – formalizm matematyczny służący do opisu poprawności algorytmów. Wprowadzony został przez brytyjskiego naukowca Charlesa A.R. Hoare’a w roku 1969.

Napis $\{P\}C\{Q\}$ oznacza, że fragment kodu $C,$ o ile na wejściu będzie miał stan spełniający warunek $P,$ oraz zakończy swoje działanie, to na wyjściu da stan spełniający warunek $Q.$ Formułę $P$ nazywamy warunkiem wstępnym, a formułę $Q$ nazywamy warunkiem końcowym.

Przykład:
do instrukcji przypisania $x:=5$ możemy dopisać następujące warunki wstępne i końcowe:

$\{\text{true}\}x:=5\{x=5\},$

co oznacza, że przy dowolnym stanie przed wykonaniem instrukcji, po wykonaniu instrukcji będziemy mieli stan, w którym zmiennej $x$ jest przypisana wartość 5.

prawdą będzie również formuła

$\{x=6,y=100\}x:=5\{x=5,y=100\},$

bo operacja przypisania na zmienną $x$ nie zmieni wartości zmiennej $y.$

$\{x=15\}x:=x+1\{x=16\},$

też będzie prawdą, ponieważ operacja przypisania na zmienną $x$ wartości tej zmiennej zwiększonej o 1, przy założeniu, że przed wykonaniem tej instrukcji zmienna $x$ ma wartość 15 da nam wynik, w którym zmienna $x$ będzie miała wartość 16.

W przypadku logiki Hoare’a dozwolone jest m.in. następujące rozumowanie:

jeśli $\{P_1\}C\{P_2\}$ oraz $\{P_2\}D\{P_3\},$ to $\{P_1\}C;D\{P_3\}.$

Pozwala nam to rozbijać złożone fragmenty kodu na instrukcje elementarne, dla których weryfikacja poprawności zapisu $\{P\}C\{Q\}$ jest łatwa.