Logika Hoare'a

Z Wikipedii

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: {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 oczywiście 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₁}C{P₂} oraz {P₂}D{P₃}, to {P₁}C; D{P₃}.

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

To jest tylko zalążek artykułu związanego z matematyką. Jeśli potrafisz, rozbuduj go.