Логика Хоара

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

Логика Хоара (англ. 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. (недоступная ссылка с 13-05-2013 (432 дня) — история)» Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19-31. 1967.

Литература[править | править вики-текст]