Логика Хоара

Логика Хоара (англ. Hoare logic, также Floyd—Hoare logic, или Hoare rules) — формальная система с набором логических правил, предназначенных для доказательства корректности компьютерных программ. Была предложена в 1969 году английским учёным в области информатики и математической логики Хоаром, позже развита самим Хоаром и другими исследователями.^[1] Первоначальная идея была предложена в работе Флойда, который опубликовал похожую систему^[2] в применении к блок-схемам (англ. flowchart).

Тройки Хоара

Основной характеристикой логики Хоара является тройка Хоара (англ. Hoare triple). Тройка описывает, как выполнение фрагмента кода изменяет состояние вычисления. Тройка Хоара имеет следующий вид:

$\{P\}\;C\;\{Q\}$

где P и Q являются утверждениями (англ. assertions), а C — командой. P называется предусловием, а Q — постусловием. Если предусловие выполняется, команда делает верным постусловие. Утверждения являются формулами логики предикатов.

В логике Хоара есть аксиомы и правила вывода для всех конструкций простого императивного языка программирования. В дополнение к этим конструкциям, описанным в оригинальной работе Хоара, Хоаром и другими исследователями были разработаны правила и для остальных конструкций: одновременного выполнения, вызова процедуры, перехода и указателя.

Частичная и полная корректность

В стандартной логике Хоара может быть доказана только частичная корректность, так как завершение программы нужно доказывать отдельно. Таким образом, «интуитивное» понимание тройки Хоара можно выразить так: если P имеет место до выполнения C, то либо имеет место Q, либо C никогда не завершится. Действительно, если C не завершается, никакого «после» нет, поэтому Q может быть любым утверждением. Более того, мы можем выбрать Q со значением «ложь», чтобы показать, что C никогда не завершится.

Полная корректность также может быть доказана с использованием расширенной версии правила для оператора While.

Правила

Аксиома пустого оператора

Правило для пустого оператора утверждает, что оператор skip (пустой оператор) не меняет состояния программы, поэтому утверждение, верное до skip, остаётся верным после его выполнения.

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

Аксиома оператора присваивания

Аксиома оператора присваивания утверждает, что после присваивания, значение любого предиката относительно правой части присваивания не меняется с заменой правой на левую часть:

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

Здесь $P[E/x]$ означает выражение P в котором все вхождения свободной переменной x заменены выражением E.

Смысл аксиомы присваивания заключается в том, что истинность $\{P[E/x]\}$ эквивалентна $\{P\}$ после выполнения присваивания. Таким образом, если $\{P[E/x]\}$ имело значение «истина» до присваивания, согласно аксиоме присваивания $\{P\}$ будет иметь значение «истина» после присваивания. И наоборот, если $\{P[E/x]\}$ было равно «ложь» до оператора присваивания, $\{P\}$ должно быть равно «ложь» после.

Примеры корректных троек:

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

Аксиома присваивания в формулировке Хоара не применима, когда более одного идентификатора ссылаются на одно и то же значение. Например,

$\{ y = 3\} \ x := 2\ \{y = 3 \}$

является неверным утверждением, если x и y ссылаются на одну и ту же переменную, так как никакое предусловие не может обеспечить, чтобы y было равно 3 после того, как x присвоено 2.

Правило композиции

Правило композиции Хоара применяется к последовательному выполнению программ S и T, где S выполняется до T, что записывается как S;T.

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

Например, рассмотрим два экземпляра аксиомы присваивания:

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

и

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

Согласно правилу композиции, мы получаем:

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

Правило условного оператора

$\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\} } \!$

Правило вывода

$\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 } \!$

Правило оператора цикла

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

Здесь P является инвариантом цикла.

Правило оператора цикла с полной корректностью

$\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 relation) "<" с каждой итерацией. При этом условие B должно подразумевать, что t не является минимальным элементом своей области определения, в противном случае посылка данного правила будет ложной. Поскольку отношение "<" является полностью фундированным, каждый шаг цикла определяется уменьшающимися членами конечного линейно упорядоченного множества.

В записи данного правила используются квадратные, а не фигурные скобки, для того чтобы обозначить полную корректность правила. (Это один из вариантов обозначения полной корректности.)

Примеры

Пример 1

$\{ x+1 = 43 \}\ y:=x+1\ \{ y = 43 \} \!$ — на основании аксиомы присваивания.

Поскольку $( x + 1 = 43 \Leftrightarrow x = 42 )$, на основании правила вывода получаем:

$\{x=42\}\ y:=x + 1\ \{y=43 \land x=42\}\!$

Пример 2

$\{x + 1 \leq N \}\ x:= x+1\ \{x \leq N\}\ \!$ — на основании аксиомы присваивания.

Если x и N целые, то $(x < N) \implies (x+1 \leq N)$, и на основании правила вывода получаем:

$\{x < N \}\ x:=x+1\ \{x \leq N\}\ \!$

См. также

• Тестирование программного обеспечения
• Контрактное программирование
• Формальная верификация

Ссылки

1. ↑ C. A. R. Hoare. «An axiomatic basis for computer programming». Communications of the ACM, 12(10):576—580,583 October 1969. DOI:10.1145/363235.363259
2. ↑ R. W. Floyd. «Assigning meanings to programs.» Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19-31. 1967.

Литература

• Гуц А. К. Математическая логика и теория алгоритмов. Изд.2, доп., 2009
• http://djvu-student.narod.ru/02-matematicheskaya-logika/metodichka/metoda_matlogika_i_teor_algoritm_g6.html

Это заготовка статьи о компьютерах. Вы можете помочь проекту, исправив и дополнив её. Это примечание по возможности следует заменить более точным.