Logika Hoare’a

Ten artykuł od 2019-02 wymaga zweryfikowania podanych informacji. Należy podać wiarygodne źródła w formie przypisów bibliograficznych. Część lub nawet wszystkie informacje w artykule mogą być nieprawdziwe. Jako pozbawione źródeł mogą zostać zakwestionowane i usunięte. Sprawdź w źródłach: Encyklopedia PWN • Google Books • Google Scholar • Federacja Bibliotek Cyfrowych • BazHum • BazTech • RCIN • Internet Archive (texts / inlibrary) Dokładniejsze informacje o tym, co należy poprawić, być może znajdują się w dyskusji tego artykułu. Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu.

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

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

${\displaystyle \{{\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 ${\displaystyle x}$ jest przypisana wartość 5.

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

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

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

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

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

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

jeśli ${\displaystyle \{P_{1}\}C\{P_{2}\}}$ oraz ${\displaystyle \{P_{2}\}D\{P_{3}\},}$ to ${\displaystyle \{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 ${\displaystyle \{P\}C\{Q\}}$ jest łatwa.