логика Хоара

Логика Хоара (также известная как логика Флойда-Хора или правила Хоара ) — это формальная система с набором логических правил для строгого рассуждения о правильности компьютерных программ . Она была предложена в 1969 году британским ученым-компьютерщиком и логиком Тони Хоаром и впоследствии усовершенствована Хоаром и другими исследователями. ^[1] Оригинальные идеи были заложены в работе Роберта Флойда , опубликовавшего аналогичную систему. ^[2] для блок-схем .

Тройка Хоара [ править ]

Центральной особенностью логики Хоара является тройка Хоара . Тройка описывает, как выполнение фрагмента кода меняет состояние вычислений. Тройка Хоара имеет вид

\{P\}C\{Q\}

где $P$ и $Q$ являются утверждениями и $C$ это команда . ^{[примечание 1]} $P$ называется предварительным условием и $Q$ постусловие . : когда предусловие выполнено, выполнение команды устанавливает постусловие Утверждения — это формулы в логике предикатов .

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

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

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

«Завершение» здесь и далее в этой статье подразумевается в более широком смысле, что вычисление в конечном итоге будет завершено, то есть подразумевает отсутствие бесконечных циклов; это не означает отсутствия нарушений предела реализации (например, деления на ноль), что приводит к преждевременной остановке программы. В своей статье 1969 года Хоар использовал более узкое понятие завершения, которое также влекло за собой отсутствие нарушений предела реализации, и выразил свое предпочтение более широкому понятию завершения, поскольку оно сохраняет утверждения независимыми от реализации: ^[4]

Еще один недостаток аксиом и правил, приведенных выше, заключается в том, что они не дают оснований для доказательства успешного завершения программы. Невозможность завершения может быть связана с бесконечным циклом; или это может быть связано с нарушением ограничения, определенного реализацией, например, диапазона числовых операндов, размера хранилища или ограничения времени операционной системы. Таким образом, обозначение « $P\{Q\}R$ следует интерпретировать «при условии, что программа успешно завершается, свойства ее результатов описываются выражением $R$ ». Довольно легко адаптировать аксиомы так, чтобы их нельзя было использовать для предсказания «результатов» незавершающихся программ; но фактическое использование аксиом теперь будет зависеть от знания многих функций, зависящих от реализации, например, размера и скорости компьютера, диапазона чисел и выбора метода переполнения. Помимо доказательств отсутствия бесконечных циклов, вероятно, лучше доказать «условную» корректность программы и полагаться на то, что реализация выдаст предупреждение, если ей пришлось отказаться от выполнения программы в результате нарушения какого-либо условия. предел реализации.

Правила [ править ]

Схема аксиом пустого утверждения [ править ]

Правило пустого оператора утверждает, что Оператор пропуска не меняет состояние программы, поэтому все, что было верно до этого, Skip также остается верным и после этого. ^{[примечание 2]}

{\dfrac {}{\{P\}{\texttt {skip}}\{P\}}}

Схема аксиом присваивания [ править ]

Аксиома присваивания гласит, что после присваивания любой предикат, который ранее был истинным для правой части присваивания, теперь справедлив для переменной. Формально, пусть $P$ в котором переменная $x$ свободна — утверждение , . Затем:

{\dfrac {}{\{P[E/x]\}x:=E\{P\}}}

где $P[E/x]$ утверждение $P,$ котором каждое свободное x $E.$ заменено в выражением $обозначает$ вхождение

Схема аксиом присваивания означает, что истинность $P[E/x]$ эквивалентно истине после присвоения $P$ . Так было $P[E/x]$ истинно до присваивания, согласно аксиоме присваивания, тогда $P$ будет истинным после этого. И наоборот, были $P[E/x]$ ложь (т.е. $\neg P[E/x]$ true) до оператора присваивания, $P$ затем должно быть ложным.

Примеры допустимых троек включают в себя:

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

Все предусловия, которые не изменяются выражением, могут быть перенесены в постусловие. В первом примере присвоение $y:=x+1$ не меняет того факта, что $x+1=43$ , поэтому оба утверждения могут появиться в постусловии. Формально этот результат получается применением схемы аксиом, где $P$ равно ( $y=43$ и $x+1=43$ ), что дает $P[(x+1)/y]$ существование ( $x+1=43$ и $x+1=43$ ), которое, в свою очередь, можно упростить до заданного предусловия $x+1=43$ .

Схема аксиом присваивания эквивалентна утверждению: чтобы найти предусловие, сначала возьмите постусловие и замените все вхождения левой части присваивания правой частью присваивания. Будьте осторожны и не пытайтесь сделать это наоборот, следуя этому неправильному образу мышления: $\{P\}x:=E\{P[E/x]\}$ ;это правило приводит к бессмысленным примерам, таким как:

\{x=5\}x:=3\{3=5\}

Еще одно неверное правило, кажущееся заманчивым на первый взгляд: $\{P\}x:=E\{P\wedge x=E\}$ ; это приводит к бессмысленным примерам вроде:

\{x=5\}x:=x+1\{x=5\wedge x=x+1\}

Хотя данное постусловие $P$ однозначно определяет предусловие $P[E/x]$ , обратное неверно. Например:

$\{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq x\wedge x\leq 9\}$ ,
$\{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq x\wedge y\cdot y\leq 9\}$ ,
$\{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq y\cdot y\wedge x\leq 9\}$ , и
$\{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq y\cdot y\wedge y\cdot y\leq 9\}$

являются действительными экземплярами схемы аксиом присваивания.

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

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

неверно, если $x$ и $y$ относятся к одной и той же переменной ( псевдоним ), хотя это правильный пример схемы аксиом присваивания (с обоими $\{P\}$ и $\{P[2/x]\}$ существование $\{y=3\}$ ).

Правило композиции [ править ]

Проверка swap-кода
без вспомогательных переменных

The three statements below (line 2, 4, 6) exchange the values of the variables $a$ and $b$ , without needing an auxiliary variable. In the verification proof, the initial value of $a$ and $b$ is denoted by the constant $A$ and $B$ , respectively. The proof is best read backwards, starting from line 7; for example, line 5 is obtained from line 7 by replacing $a$ (target expression in line 6) by $a-b$ (source expression in line 6). Some arithmetical simplifications are used tacitly, viz. $a-(a-b)=b$ (line 5→3), and $a+b-b=a$ (line 3→1).
Nr	Code	Assertions
1:		$\{a=A\wedge b=B\}$
2:	$a:=a+b;$
3:		$\{a-b=A\wedge b=B\}$
4:	$b:=a-b;$
5:		$\{b=A\wedge a-b=B\}$
6:	$a:=a-b$
7:		$\{b=A\wedge a=B\}$

Правило композиции Хоара применяется к последовательно выполняемым программам $S$ и $T$ , где $S$ выполняется до $T$ и записывается $S;T$ ( $Q$ называется средним условием ): ^[5]

{\dfrac {\{P\}S\{Q\}\quad ,\quad \{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\}

Другой пример показан в правом поле.

Условное правило [ править ]

{\dfrac {\{B\wedge P\}S\{Q\}\quad ,\quad \{\neg B\wedge P\}T\{Q\}}{\{P\}{\texttt {if}}\ B\ {\texttt {then}}\ S\ {\texttt {else}}\ T\ {\texttt {endif}}\{Q\}}}

Условное правило гласит, что постусловие $Q,$ общее для тогда и иначе часть также является постусловием целого оператор if...endif . ^[6]В тогда и В противном неотрицательное и отрицаемое условие $B$ можно добавить $случае к предварительному условию P$ соответственно.Состояние $B$ не должно иметь побочных эффектов.Пример приведен в следующем разделе .

Это правило не содержалось в оригинальной публикации Хоара. ^[1]Однако, поскольку заявление

{\texttt {if}}\ B\ {\texttt {then}}\ S\ {\texttt {else}}\ T\ {\texttt {endif}}

имеет тот же эффект, что и конструкция одноразового цикла

{\texttt {bool}}\ b:={\texttt {true}};{\texttt {while}}\ B\wedge b\ {\texttt {do}}\ S;b:={\texttt {false}}\ {\texttt {done}};b:={\texttt {true}};{\texttt {while}}\ \neg B\wedge b\ {\texttt {do}}\ T;b:={\texttt {false}}\ {\texttt {done}}

условное правило может быть получено из других правил Хоара.Аналогичным образом действуют правила для других производных программных конструкций, например для цикла, делать... до цикла, выключатель , перерыв , continue можно свести путем преобразования программы к правилам из оригинальной статьи Хоара.

Правило последствий [ править ]

{\dfrac {P_{1}\rightarrow P_{2}\quad ,\quad \{P_{2}\}S\{Q_{2}\}\quad ,\quad Q_{2}\rightarrow Q_{1}}{\{P_{1}\}S\{Q_{1}\}}}

Это правило позволяет усилить предусловие $P_{2}$ и/или ослабить постусловие $Q_{2}$ .Он используется, например, для достижения буквально идентичных постусловий для тогда и еще часть.

Например, доказательство

\{0\leq x\leq 15\}{\texttt {if}}\ x<15\ {\texttt {then}}\ x:=x+1\ {\texttt {else}}\ x:=0\ {\texttt {endif}}\{0\leq x\leq 15\}

необходимо применить условное правило, которое, в свою очередь, требует доказать

\{0\leq x\leq 15\wedge x<15\}x:=x+1\{0\leq x\leq 15\}

или упрощенно

\{0\leq x<15\}x:=x+1\{0\leq x\leq 15\}

для затем расстаться и

\{0\leq x\leq 15\wedge x\geq 15\}x:=0\{0\leq x\leq 15\}

или упрощенно

\{x=15\}x:=0\{0\leq x\leq 15\}

для еще часть.

Однако правило присваивания для тогда часть требует выбрать $P$ как $0\leq x\leq 15$ ; применение правил, следовательно, дает

\{0\leq x+1\leq 15\}x:=x+1\{0\leq x\leq 15\}

, что логически эквивалентно

\{-1\leq x<15\}x:=x+1\{0\leq x\leq 15\}

.

Правило последствий необходимо для усиления предусловия $\{-1\leq x<15\}$ полученное из правила присваивания $\{0\leq x<15\}$ требуется для условного правила.

Аналогично, для else часть, правило присваивания дает

\{0\leq 0\leq 15\}x:=0\{0\leq x\leq 15\}

или эквивалентно

\{{\texttt {true}}\}x:=0\{0\leq x\leq 15\}

,

следовательно, правило последствий должно применяться с $P_{1}$ и $P_{2}$ существование $\{x=15\}$ и $\{{\texttt {true}}\}$ , соответственно, чтобы еще раз усилить предусловие. Неформально, эффект правила последствий состоит в том, чтобы «забыть», что $\{x=15\}$ известно при входе в else часть, поскольку правило присваивания, используемое для else часть не нуждается в этой информации.

Пока правило [ править ]

{\dfrac {\{P\wedge B\}S\{P\}}{\{P\}{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}\{\neg B\wedge P\}}}

Здесь $P$ — инвариант цикла который должен сохраняться телом цикла $S.$ , После завершения цикла этот инвариант $P$ все еще сохраняется, и, более того, $\neg B$ должно быть, привело к завершению цикла.Как и в условном правиле, $B$ не должен иметь побочных эффектов.

Например, доказательство

\{x\leq 10\}{\texttt {while}}\ x<10\ {\texttt {do}}\ x:=x+1\ {\texttt {done}}\{\neg x<10\wedge x\leq 10\}

к тому времени правило требует доказать

\{x\leq 10\wedge x<10\}x:=x+1\{x\leq 10\}

или упрощенно

\{x<10\}x:=x+1\{x\leq 10\}

,

которое легко получить по правилу присваивания.Наконец, постусловие $\{\neg x<10\wedge x\leq 10\}$ можно упростить до $\{x=10\}$ .

Другой пример: правило while можно использовать для формальной проверки следующей странной программы для вычисления точного квадратного корня $x$ из произвольного числа $a$ , даже если $x$ — целочисленная переменная, а $a$ — не квадратное число:

\{{\texttt {true}}\}{\texttt {while}}\ x\cdot x\neq a\ {\texttt {do}}\ {\texttt {skip}}\ {\texttt {done}}\{x\cdot x=a\wedge {\texttt {true}}\}

После применения правила while, когда $P$ равно правда , осталось доказать

\{{\texttt {true}}\wedge x\cdot x\neq a\}{\texttt {skip}}\{{\texttt {true}}\}

,

что следует из правила пропуска и правила последствий.

На самом деле странная программа отчасти верна: если бы она завершилась, то наверняка $x$ (случайно) содержал бы значение $квадратного$ корня.Во всех остальных случаях оно не будет прекращено; поэтому это не совсем правильно.

Хотя правило абсолютной правильности [ править ]

Если вышеупомянутое обычное правило while заменить следующим, исчисление Хоара также можно будет использовать для доказательства полной корректности , т. е. завершения, а также частичной корректности. Обычно здесь вместо фигурных скобок используются квадратные скобки, чтобы указать на другое представление о корректности программы.

{\dfrac {<\ {\text{is a well-founded ordering on the set}}\ D\quad ,\quad [P\wedge B\wedge t\in D\wedge t=z]S[P\wedge t\in D\wedge t<z]}{[P\wedge t\in D]{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}[\neg B\wedge P\wedge t\in D]}}

В этом правиле, помимо сохранения инварианта цикла, также доказывается завершение с помощью выражения $t$ , называемого вариантом цикла , значение которого строго уменьшается по отношению к обоснованному отношению $<$ на некотором множестве доменов $D$ во время каждой итерации. Поскольку $<$ обосновано, строго убывающая цепочка членов $D$ может иметь только конечную длину, поэтому $t$ не может уменьшаться вечно. (Например, обычный порядок $<$ хорошо обоснован для натуральных чисел $\mathbb {N}$ , но ни в целых числах $\mathbb {Z}$ ни о положительных действительных числах $\mathbb {R} ^{+}$ ; все эти множества подразумеваются в математическом, а не в вычислительном смысле; в частности, все они бесконечны.)

Учитывая инвариант цикла $P$ , условие $B$ должно подразумевать, что $t$ не является минимальным элементом , $D$ поскольку в противном случае тело $S$ не могло бы уменьшать $t$ дальше, т. е. посылка правила была бы ложной. (Это одно из различных обозначений полной правильности.) ^{[примечание 3]}

Возвращаясь к первому примеру предыдущего раздела , для доказательства полной корректности

[x\leq 10]{\texttt {while}}\ x<10\ {\texttt {do}}\ x:=x+1\ {\texttt {done}}[\neg x<10\wedge x\leq 10]

правило while для полной корректности может быть применено, например, $D$ — это неотрицательные целые числа обычного порядка, а выражение $t$ — $10-x$ , что затем, в свою очередь, требует доказать

[x\leq 10\wedge x<10\wedge 10-x\geq 0\wedge 10-x=z]x:=x+1[x\leq 10\wedge 10-x\geq 0\wedge 10-x<z]

Неформально говоря, нам нужно доказать, что расстояние $10-x$ уменьшается в каждом цикле цикла, при этом всегда остается неотрицательным; этот процесс может продолжаться лишь конечное число циклов.

Предыдущую цель доказательства можно упростить до

[x<10\wedge 10-x=z]x:=x+1[x\leq 10\wedge 10-x<z]

,

что можно доказать следующим образом:

[x+1\leq 10\wedge 10-x-1<z]x:=x+1[x\leq 10\wedge 10-x<z]

получается по правилу присваивания, а

[x+1\leq 10\wedge 10-x-1<z]

может быть усилен до

[x<10\wedge 10-x=z]

по правилу последствий.

Во втором примере предыдущего раздела , конечно, не может быть найдено выражение $t$ , которое уменьшается на пустое тело цикла, поэтому завершение не может быть доказано.

См. также [ править ]

Примечания [ править ]

^ Хоар первоначально написал " $P\{C\}Q$ " скорее, чем " $\{P\}C\{Q\}$ ".
^ В этой статье для правил используются обозначения в стиле естественной дедукции . Например, ${\dfrac {\alpha ,\beta }{\phi }}$ неформально означает: «Если выполняются и $α$ , и $β$ , то выполняется и $φ$ »; $α$ и $β$ называются предшественниками правила, $φ$ называется его последователем. Правило без антецедентов называется аксиомой и записывается как ${\dfrac {}{\quad \phi \quad }}$ .
^ Статья Хоара 1969 года не содержала правила полной корректности; ср. его обсуждение на стр.579 (вверху слева). Например учебник Рейнольдса ^[3] дает следующую версию правила полной корректности: ${\dfrac {P\wedge B\rightarrow 0\leq t\quad ,\quad [P\wedge B\wedge t=z]S[P\wedge t<z]}{[P]{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}[P\wedge \neg B]}}$ когда $z$ — целочисленная переменная, которая не встречается в свободном виде в $P$ , $B$ , $S$ или $t$ , а $t$ — целочисленное выражение (переменные Рейнольдса переименованы, чтобы соответствовать настройкам этой статьи).

Ссылки [ править ]

^ Jump up to: ^а ^б Хоар, ЦАР (октябрь 1969 г.). «Аксиоматические основы компьютерного программирования» . Коммуникации АКМ . 12 (10): 576–580. дои : 10.1145/363235.363259 . S2CID 207726175 .
^ Р.В. Флойд . « Придание значения программам ». Труды симпозиума Американского математического общества по прикладной математике. Том. 19, стр. 19–31. 1967.
^ Jump up to: ^а ^б Джон К. Рейнольдс (2009). Теории языков программирования . Издательство Кембриджского университета. ) Здесь: Разд. 3.4, с. 64.
^ Хоар (1969), стр.578-579.
^ Хут, Майкл; Райан, Марк (26 августа 2004 г.). Логика в информатике (второе изд.). ЧАШКА. п. 276. ИСБН 978-0521543101 .
^ Апт, Кшиштоф Р.; Ольдерог, Эрнст-Рюдигер (декабрь 2019 г.). «Пятьдесят лет логики Хоара» . Формальные аспекты вычислений . 31 (6): 759. doi : 10.1007/s00165-019-00501-3 . S2CID 102351597 .

Дальнейшее чтение [ править ]

Роберт Д. Теннент. Specifying Software (учебник, включающий введение в логику Хоара, написанный в 2002 году) ISBN 0-521-00401-2

Внешние ссылки [ править ]

KeY-Hoare — это полуавтоматическая система проверки, построенная на базе средства доказательства теорем KeY . Он использует исчисление Хоара для простого языка while.
Модуль j-Algo Hoare Calculus ( j-Algo на GitHub , j-Algo на SourceForge ) — визуализация расчета Хоара в программе визуализации алгоритма j-Algo.

[3] Хоар первоначально написал " $P\{C\}Q$ " скорее, чем " $\{P\}C\{Q\}$ ".

[6] В этой статье для правил используются обозначения в стиле естественной дедукции . Например, ${\dfrac {\alpha ,\beta }{\phi }}$ неформально означает: «Если выполняются и $α$ , и $β$ , то выполняется и $φ$ »; $α$ и $β$ называются предшественниками правила, $φ$ называется его последователем. Правило без антецедентов называется аксиомой и записывается как ${\dfrac {}{\quad \phi \quad }}$ .

[9] Статья Хоара 1969 года не содержала правила полной корректности; ср. его обсуждение на стр.579 (вверху слева). Например учебник Рейнольдса ^[3] дает следующую версию правила полной корректности: ${\dfrac {P\wedge B\rightarrow 0\leq t\quad ,\quad [P\wedge B\wedge t=z]S[P\wedge t<z]}{[P]{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}[P\wedge \neg B]}}$ когда $z$ — целочисленная переменная, которая не встречается в свободном виде в $P$ , $B$ , $S$ или $t$ , а $t$ — целочисленное выражение (переменные Рейнольдса переименованы, чтобы соответствовать настройкам этой статьи).

[hoare-1] Jump up to: ^а ^б Хоар, ЦАР (октябрь 1969 г.). «Аксиоматические основы компьютерного программирования» . Коммуникации АКМ . 12 (10): 576–580. дои : 10.1145/363235.363259 . S2CID 207726175 .

[2] Р.В. Флойд . « Придание значения программам ». Труды симпозиума Американского математического общества по прикладной математике. Том. 19, стр. 19–31. 1967.

[Reynolds.2009-4] Jump up to: ^а ^б Джон К. Рейнольдс (2009). Теории языков программирования . Издательство Кембриджского университета. ) Здесь: Разд. 3.4, с. 64.

[5] Хоар (1969), стр.578-579.

[7] Хут, Майкл; Райан, Марк (26 августа 2004 г.). Логика в информатике (второе изд.). ЧАШКА. п. 276. ИСБН 978-0521543101 .

[8] Апт, Кшиштоф Р.; Ольдерог, Эрнст-Рюдигер (декабрь 2019 г.). «Пятьдесят лет логики Хоара» . Формальные аспекты вычислений . 31 (6): 759. doi : 10.1007/s00165-019-00501-3 . S2CID 102351597 .

[1]

[2]

[примечание 1]

[3]

[4]

[примечание 2]

[5]

[6]

[примечание 3]