Логика Хоара

Эта статья находится на начальном уровне проработки, в одной из её версий выборочно используется текст из источника, распространяемого под свободной лицензией
Материал из энциклопедии Руниверсалис

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

Тройки Хоара

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

[math]\displaystyle{ \{P\}\;C\;\{Q\} }[/math]

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

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

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

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

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

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

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

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

Правила

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

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

[math]\displaystyle{ \frac{}{\{P\}\ \textbf{skip}\ \{P\}} }[/math]

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

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

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

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

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

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

  • [math]\displaystyle{ \{x + 1 = 43\}\ y := x + 1\ \{ y = 43 \} }[/math]
  • [math]\displaystyle{ \{x + 1 \leq N \}\ x := x + 1\ \{x \leq N\} }[/math]

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

[math]\displaystyle{ \{ y = 3\} \ x := 2\ \{y = 3 \} }[/math]

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

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

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

[math]\displaystyle{ \frac {\{P\}\ S\ \{Q\}\ , \ \{Q\}\ T\ \{R\} } {\{P\}\ S;T\ \{R\}} }[/math]

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

[math]\displaystyle{ \{ x + 1 = 43\} \ y := x + 1\ \{y =43 \} }[/math]

и

[math]\displaystyle{ \{ y = 43\} \ z := y\ \{z = 43 \} }[/math]

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

[math]\displaystyle{ \{ x + 1 = 43\} \ y:=x + 1; z:= y\ \{z =43 \} }[/math]

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

[math]\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\} } }[/math]

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

[math]\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 } }[/math]

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

[math]\displaystyle{ \frac { \{P \wedge B \}\ S\ \{P\} } { \{P \}\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ \{\neg B \wedge P\} } }[/math]

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

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

[math]\displaystyle{ \frac { \lt \;\text{is well-founded,}\;[P \wedge B \wedge t = z ]\ S\ [P \wedge t \lt z ]} { [P]\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ [\neg B \wedge P] } }[/math]

В этом правиле, кроме сохранения инварианта цикла, доказывается завершение цикла при помощи терма, называемого переменной цикла (здесь t), значение которого строго уменьшается согласно отношению полной фундированности (well-founded relation) "<" с каждой итерацией. При этом условие B должно подразумевать, что t не является минимальным элементом своей области определения, в противном случае посылка данного правила будет ложной. Поскольку отношение "<" является полностью фундированным, каждый шаг цикла определяется уменьшающимися членами конечного линейно упорядоченного множества.

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

Примеры

Пример 1
[math]\displaystyle{ \{ x+1 = 43 \}\ y:=x+1\ \{ y = 43 \} }[/math] — на основании аксиомы присваивания.
Поскольку [math]\displaystyle{ ( x + 1 = 43 \Leftrightarrow x = 42 ) }[/math], на основании правила вывода получаем:
[math]\displaystyle{ \{x=42\}\ y:=x + 1\ \{y=43 \land x=42\} }[/math]
Пример 2
[math]\displaystyle{ \{x + 1 \leq N \}\ x:= x+1\ \{x \leq N\} }[/math] — на основании аксиомы присваивания.
Если x и N целые, то [math]\displaystyle{ (x \lt N) \implies (x+1 \leq N) }[/math], и на основании правила вывода получаем:
[math]\displaystyle{ \{x \lt N \}\ x:=x+1\ \{x \leq N\} }[/math]

См. также

Ссылки

  1. ↑ C. A. R. Hoare. «An axiomatic basis for computer programming Архивная копия от 17 июля 2011 на Wayback Machine». Communications of the ACM, 12(10):576—580,583 October 1969. doi:10.1145/363235.363259
  2. ↑ R. W. Floyd. «Assigning meanings to programs. Архивировано 9 декабря 2008 года.  (недоступная ссылка с 13-05-2013 [4213 дней] — история)» (недоступная ссылка) Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19-31. 1967.

Литература

Источник — https://xn--h1ajim.xn--p1ai/index.php?title=Логика_Хоара&oldid=5800772