Logika Hoare’a

Z Wikipedii, wolnej encyklopedii
Przejdź do nawigacji Przejdź do wyszukiwania

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 oznacza, że fragment kodu o ile na wejściu będzie miał stan spełniający warunek oraz zakończy swoje działanie, to na wyjściu da stan spełniający warunek Formułę nazywamy warunkiem wstępnym, a formułę nazywamy warunkiem końcowym.

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

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

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

bo operacja przypisania na zmienną nie zmieni wartości zmiennej

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

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

jeśli oraz to

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