Логика Хоара
Материал из Seo Wiki - Поисковая Оптимизация и Программирование
Логика Хоара (англ. Hoare logic, также Floyd—Hoare logic, или Hoare rules) — формальная система с набором логических правил, предназначенных для доказательства корректности компьютерных программ. Была предложена в 1969 году английским учёным в области информатики и математической логики Хоаром, позже развита Хоаром и другими исследователями.[1] Первоначальная идея была предложена в работе Флойда, который опубликовал похожую систему[2] в применении к блок-схемам (англ. flowchart).
Содержание |
[править] Тройки Хоара
Основной характеристикой логики Хоара является тройка Хоара (англ. Hoare triple). Тройка описывает, как выполнение фрагмента кода изменяет состояние вычисления. Тройка Хоара имеет следующий вид:
- <math>\{P\}\;C\;\{Q\}</math>
где P и Q являются утверждениями (англ. assertions), а C — командой. P называется предусловием, а Q — постусловием. Если предусловие выполняется, команда делает верным постусловие. Утверждения являются формулами логики предикатов.
В логике Хоара есть аксиомы и правила вывода для всех конструкций простого императивного языка программирования. В дополнение к этим конструкциям, описанным в оригинальной работе Хоара, Хоаром и другими исследователями были разработаны правила и для остальных конструкций: одновременного выполнения, вызова процедуры, перехода и указателя.
[править] Частичная и полная корректность
В стандартной логике Хоара может быть доказана только частичная корректность, так как завершение программы нужно доказывать отдельно. Таким образом, «интуитивное» понимание тройки Хоара можно выразить так: если P имеет место до выполнения C, то либо имеет место Q, либо C никогда не завершиться. Действительно, если C не завершается, никакого «после» нет, поэтому Q может быть любым утверждением. Более того, мы можем выбрать Q со значением «ложь», чтобы показать, что C никогда не завершится.
Полная корректность также может быть доказана с использованием расширенной версии правила для оператора While.
[править] Правила
[править] Аксиома пустого оператора
Правило для пустого оператора утверждает, что оператор skip (пустой оператор) не меняет состояния программы, поэтому утверждение, верное до skip, остаётся верным после его выполнения.
- <math> \frac{}{\{P\}\ \textbf{skip}\ \{P\}} \!</math>
[править] Аксиома оператора присваивания
Аксиома оператора присваивания утверждает, что после присваивания, значение любого предиката относительно правой части присваивания не меняется с заменой правой на левую часть:
- <math> \frac{}{\{P[E/x]\}\ x:=E \ \{P\} } \!</math>
Здесь <math>P[E/x]</math> означает выражение P в котором все вхождения свободной переменной x заменены выражением E.
Смысл аксиомы присваивания заключается в том, что истинность <math>\{P[E/x]\}</math> эквивалентна <math>\{P\}</math> после выполнения присваивания. Таким образом, если <math>\{P[E/x]\}</math> имело значение «истина» до присваивания, согласно аксиоме присваивания <math>\{P\}</math> будет иметь значение «истина» после присваивания. И наоборот, если <math>\{P[E/x]\}</math> было равно «ложь» до оператора присваивания, <math>\{P\}</math> должно быть равно «ложь» после.
Примеры корректных троек:
- <math>\{x + 1 = 43\}\ y := x + 1\ \{ y = 43 \}\!</math>
- <math>\{x + 1 \leq N \}\ x := x + 1\ \{x \leq N\}\ \!</math>
Аксиома присваивания в формулировке Хоара не применима, когда более одного идентификатора ссылаются на одно и то же значение. Например,
- <math>\{ y = 3\} \ x := 2\ \{y = 3 \}</math>
является неверным утверждением, если x и y ссылаются на одну и ту же переменную, так как никакое предусловие не может обеспечить, чтобы y было равно 3 после того, как x присвоено 2.
[править] Правило композиции
Правило композиции Хоара применяется к последовательному выполнению программ S и T, где S выполняется до T, что записывается как S;T.
- <math> \frac {\{P\}\ S\ \{Q\}\ , \ \{Q\}\ T\ \{R\} } {\{P\}\ S;T\ \{R\}} \!</math>
Например, рассмотрим два экземпляра аксиомы присваивания:
- <math>\{ x + 1 = 43\} \ y := x + 1\ \{y =43 \}</math>
и
- <math>\{ y = 43\} \ z := y\ \{z = 43 \}</math>
Согласно правилу композиции, мы получаем:
- <math>\{ x + 1 = 43\} \ y:=x + 1; z:= y\ \{z =43 \}</math>
[править] Правило условного оператора
- <math>\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>
\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>\frac { \{P \wedge B \}\ S\ \{P\} }
{ \{P \}\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ \{\neg B \wedge P\} }
\!</math>
Здесь P является инвариантом цикла.
[править] Правило оператора цикла с полной корректностью
- <math>
\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] }
\!</math>
В этом правиле, кроме сохранения инварианта цикла, доказывается завершение цикла при помощи терма, называемого переменной цикла (здесь t), значение которого строго уменьшается согласно отношения полной фундированности (well-founded relation) "<" с каждой итерацией. При этом условие B должно подразумевать, что t не является минимальным элементом своей области определения, в противном случае посылка данного правила будет ложной. Поскольку отношение "<" является полностью фундированным, каждый шаг цикла определяется уменьшающимися членами конечного линейно упорядоченного множества.
В записи данного правила используются квадратные, а не фигурные скобки, для того чтобы обозначить полную корректность правила. (Это один из вариантов обозначения полной корректности.)
[править] Примеры
Пример 1 <math> \{ x+1 = 43 \}\ y:=x+1\ \{ y = 43 \} \!</math> — на основании аксиомы присваивания. Поскольку <math>( x + 1 = 43 \Leftrightarrow x = 42 )</math>, на основании правила вывода получаем: <math>\{x=42\}\ y:=x + 1\ \{y=43 \land x=42\}\!</math> Пример 2 <math>\{x + 1 \leq N \}\ x:= x+1\ \{x \leq N\}\ \!</math> — на основании аксиомы присваивания. Если x и N целые, то <math> (x < N) \implies (x+1 \leq N)</math>, и на основании правила вывода получаем: <math>\{x < N \}\ x:=x+1\ \{x \leq N\}\ \!</math>
[править] См. также
[править] Ссылки
- ↑ 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
- ↑ 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
| Файл:Computer.svg | Это незавершённая статья о компьютерах. Вы можете помочь проекту, исправив и дополнив её. |
en:Hoare logic es:Lógica de Hoare fr:Logique de Hoare it:Logica di Hoare nl:Hoarelogica ja:ホーア論理 pl:Logika Hoare'a vi:Luận lý Hoare zh:霍尔逻辑