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.