логика Хоара

Логика Хоара (также известная как логика Флойда-Хора или правила Хоара ) — это формальная система с набором логических правил для строгого рассуждения о правильности компьютерных программ . Она была предложена в 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]