Tekst źródłowy strony Logika Hoare’a

{{Dopracować|źródła|data=2019-02}}
'''Logika Hoare’a''' – formalizm matematyczny służący do opisu [[dowód poprawności algorytmu|poprawności algorytmów]]. Wprowadzony został przez brytyjskiego naukowca [[Charles Antony Richard Hoare|Charlesa A.R. Hoare’a]] w roku 1969.

Napis <math>\{P\}C\{Q\}</math> oznacza, że fragment [[kod]]u <math>C,</math> o ile na wejściu będzie miał stan spełniający warunek <math>P,</math> oraz zakończy swoje działanie, to na wyjściu da stan spełniający warunek <math>Q.</math> Formułę <math>P</math> nazywamy [[warunek wstępny|warunkiem wstępnym]], a formułę <math>Q</math> nazywamy [[warunek końcowy|warunkiem końcowym]].

Przykład:<br />
do instrukcji przypisania <math>x:=5</math> możemy dopisać następujące warunki wstępne i końcowe:
: <math>\{\text{true}\}x:=5\{x=5\},</math>

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

prawdą będzie również formuła
: <math>\{x=6, y=100\}x:=5\{x=5, y=100\},</math>

bo operacja przypisania na zmienną <math>x</math> nie zmieni wartości zmiennej <math>y.</math>
: <math>\{x=15\}x:=x+1\{x=16\},</math>

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

W przypadku logiki Hoare’a dozwolone jest m.in. następujące rozumowanie:
: jeśli <math>\{P_1\}C\{P_2\}</math> oraz <math>\{P_2\}D\{P_3\},</math> to <math>\{P_1\}C;D\{P_3\}.</math>
Pozwala nam to rozbijać złożone fragmenty kodu na instrukcje elementarne, dla których weryfikacja poprawności zapisu <math>\{P\}C\{Q\}</math> jest łatwa.

[[Kategoria:Teoria obliczeń]]
[[Kategoria:Logika matematyczna]]