Логика Хоара

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

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

Тройки Хоара[править | править вики-текст]

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

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

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

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

Основная идея Хоара дать для каждой конструкции императивного языка пред и постусловие записанное в виде логической формулы. Поэтому и возникает в названии тройка — предусловие, конструкция языка, постусловие

  • Ясно, что для пустого оператора пред и постусловия совпадают.
  • Для оператора присваивания в постусловие кроме предусловия должно учитывать факт, что значение переменной стало другим.
  • Для составного оператора (в Python это отступы, в C это {}) имеем цепочку пред и постусловий . В результате для составного оператора можно оставить первое предусловие и последнее постусловие.
  • Правило вывода говорит, что можно усилить пред и ослабить постусловие если нам это понадобиться. Нет смысла волочь через всю программу какое-то утверждение, которое не помогает решить поставленную задачу.
  • Оператор ветвления или просто if. Его условно можно разбить на две ветки then и else. Если к предусловиюдобавить истинность логического условия (то, что стоит под if), то после выполнения ветки then должно следоватьпостусловие. Аналогично, если к предусловию добавить отрицание логического условия (то, что стоит под if), то после выполнения ветки else должно следовать постусловие
  • Оператор цикла. Это самое нетривиальное и сложное, поскольку цикл может выполняется много раз и даже не окончится. Чтобы решить проблему возможно многократного повтора тела цикла вводят инвариант цикла.Инвариант цикла это то, что истинно перед его выполнением, истинно после каждого выполнения тела цикла и следовательно истинно и после его окончания. Предусловие для оператора цикла это просто его инвариант цикла. Если истинно условие продолжения цикла (то, что стоит под while), то после выполнения тела цикла должна следовать истинность инвариант цикла. В результате после окончания цикла имеем в качестве постусловияистинность инвариант цикла и отрицание условия продолжения цикла.
  • Оператора цикла с полной корректностью. Для этого к предыдущему пункту добавляют ограничивающую функцию, с помощью которой легко доказать, что цикл будет выполнятся ограниченное число раз. На нее накладывают условия, что она всегда >=0, строго убывает после каждого выполнения тела цикла и в точности =0, когда цикл заканчивается.

Правильно работающую программу можно написать очень многими способами, а также она в большом количестве случаев будет эффективной. Этот произвол и именно он усложняет программирование. Для этого вводят стиль. Но этого оказывается мало. Для многих программ (например, связанных косвенно с жизнью человека) нужно доказать и их корректность. Оказалось, что доказательство корректности делает программу дороже на порядок (примерно в 10 раз).

Частичная и полная корректность[править | править вики-текст]

В стандартной логике Хоара может быть доказана только частичная корректность, так как завершение программы нужно доказывать отдельно. Таким образом, «интуитивное» понимание тройки Хоара можно выразить так: если 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 (582 дня) — история)» Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19-31. 1967.

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