Логіка Гоара

Аксіома про порожній оператор каже нам що він не змінює стан програми, тому що було правдою до його виконання, залишається таким же і після.

${\displaystyle {\frac {}{\{P\}\ {\textbf {skip}}\ \{P\}}}\!}$

Аксіома про присвоєння каже що після присвоєння для змінної виконується предикат, який виконувався для правої частини оператора присвоєння:

${\displaystyle {\frac {}{\{P[E/x]\}\ x:=E\ \{P\}}}\!}$

Тут ${\displaystyle P[E/x]}$ позначає вираз P у якому всі вільні входження змінної x були замінені виразом E.

Аксіома про присвоєння означає що істинність ${\displaystyle \{P[E/x]\}}$ еквівалентна істинності ${\displaystyle \{P\}}$ після присвоєння. Тобто якщо ${\displaystyle \{P[E/x]\}}$ була істинна до присвоєння, то ${\displaystyle \{P\}}$ буде після. І навпаки, якщо ${\displaystyle \{P[E/x]\}}$ була хибною до присвоєння, то ${\displaystyle \{P\}}$ теж має бути хибною після.

Приклади правильних трійок:

• ${\displaystyle \{x+1=43\}\ y:=x+1\ \{y=43\}\!}$
• ${\displaystyle \{x+1\leq N\}\ x:=x+1\ \{x\leq N\}\ \!}$

Правило композиції застосовується до послідовно виконуваних програм S та T, де S виконується до T і записується S;T.

${\displaystyle {\frac {\{P\}\ S\ \{Q\}\ ,\ \{Q\}\ T\ \{R\}}{\{P\}\ S;T\ \{R\}}}\!}$

Наприклад, розглянемо такі два присвоєння:

${\displaystyle \{x+1=43\}\ y:=x+1\ \{y=43\}}$

та

${\displaystyle \{y=43\}\ z:=y\ \{z=43\}}$

З правила композиції:

${\displaystyle \{x+1=43\}\ y:=x+1;z:=y\ \{z=43\}}$

З трійки для умовного оператора можна вивести дві трійки: одну для випадку істинності умови, іншу для її хибності:

${\displaystyle {\frac {\{B\wedge P\}\ S\ \{Q\}\ ,\ \{\neg B\wedge P\}\ T\ \{Q\}}{\{P\}\ {\textbf {if}}\ B\ {\textbf {then}}\ S\ {\textbf {else}}\ T\ {\textbf {endif}}\ \{Q\}}}\!}$

Передумову та/або постумову можна замінити, якщо для них виконуються певні імплікації:

${\displaystyle {\frac {P^{\prime }\rightarrow \ P\ ,\ \lbrace P\rbrace \ S\ \lbrace Q\rbrace \ ,\ Q\rightarrow \ Q^{\prime }}{\lbrace P^{\prime }\ \rbrace \ S\ \lbrace Q^{\prime }\rbrace }}\!}$

${\displaystyle {\frac {\{P\wedge B\}\ S\ \{P\}}{\{P\}\ {\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {done}}\ \{\neg B\wedge P\}}}\!}$

Тут P інваріант циклу.

${\displaystyle {\frac {<\;{\textrm {is\ well-founded,}}\;[P\wedge B\wedge t=z]\ S\ [P\wedge t<z]}{[P]\ {\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {done}}\ [\neg B\wedge P]}}\!}$

В цьому правилі на додачу до інваріанта циклу, також доводять завершуваність додаванням варіанта циклу (тут t), чиє значення строго спадає згідно з фундованим відношенням протягом кожної ітерації. Через те що відношення «<» well-founded, кожна ітерація циклу перелічується спадними членами скінченного ланцюга. Також зауважте, що тут для позначення тотальної коректності використовуються квадратні дужки. (Це одне з можливих позначень тотальної коректності.)

Аксіоми можна використовувати для перевірки узгодженості передачі даних від оператора до оператора, для аналізу структурних властивостей текстів програм, для встановлення умов закінчення циклу. Крім того, правила можна використовувати для аналізу результатів виконання програми, що пов'язано з семантикою програми.