Logika Hoare'a
Z Wikipedii
logika Hoare'a - formalizm matematyczny służący do opisu poprawności algorytmów. Wprowadzona została 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 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 {P1}C{P2} oraz {P2}D{P3}, to {P1}C; D{P3}.
Pozwala nam to rozbijać złożone fragmentu kodu na instrukcje elementarne, dla których weryfikacja poprawności zapisu {P}C{Q} jest łatwa.
