логика Хоара

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

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

Хоар тройной

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

${\displaystyle \{P\}C\{Q\}}$

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

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

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

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

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

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

Правила

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

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

${\displaystyle {\dfrac {}{\{P\}{\texttt {skip}}\{P\}}}}$

Схема аксиом присваивания

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

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

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

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

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

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

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

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

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

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

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

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

• ${\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq x\wedge x\leq 9\}}$,
• ${\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq x\wedge y\cdot y\leq 9\}}$,
• ${\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq y\cdot y\wedge x\leq 9\}}$, и
• ${\displaystyle \{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\}}$

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

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

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

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

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

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

${\displaystyle {\dfrac {\{P\}S\{Q\}\quad ,\quad \{Q\}T\{R\}}{\{P\}S;T\{R\}}}}$

Например, рассмотрим следующие два примера аксиомы присваивания:

${\displaystyle \{x+1=43\}y:=x+1\{y=43\}}$

и

${\displaystyle \{y=43\}z:=y\{z=43\}}$

По правилу последовательности можно сделать вывод:

${\displaystyle \{x+1=43\}y:=x+1;z:=y\{z=43\}}$

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

Условное правило

${\displaystyle {\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 , общее для частей then и else , также является постусловием всего оператора if...endif . ^[6] В частях then и else неотрицаемое и инвертированное условие B могут быть добавлены к предварительному условию P соответственно. Состояние B не должно иметь побочных эффектов. Пример приведен в следующем разделе.

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

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

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

${\displaystyle {\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}}}$

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

Правило следствия

${\displaystyle {\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}\}}}}$

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

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

${\displaystyle \{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\}}$

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

${\displaystyle \{0\leq x\leq 15\wedge x<15\}x:=x+1\{0\leq x\leq 15\}}$или упрощенно

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

для тогдашней части, и

${\displaystyle \{0\leq x\leq 15\wedge x\geq 15\}x:=0\{0\leq x\leq 15\}}$или упрощенно

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

для остальной части.

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

${\displaystyle \{0\leq x+1\leq 15\}x:=x+1\{0\leq x\leq 15\}}$, что логически эквивалентно

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

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

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

${\displaystyle \{0\leq 0\leq 15\}x:=0\{0\leq x\leq 15\}}$или эквивалентно

${\displaystyle \{{\texttt {true}}\}x:=0\{0\leq x\leq 15\}}$,

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

Пока правят

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

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

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

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

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

${\displaystyle \{x\leq 10\wedge x<10\}x:=x+1\{x\leq 10\}}$или упрощенно

${\displaystyle \{x<10\}x:=x+1\{x\leq 10\}}$,

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

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

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

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

${\displaystyle \{{\texttt {true}}\wedge x\cdot x\neq a\}{\texttt {skip}}\{{\texttt {true}}\}}$,

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

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

Хотя правило полной правильности

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

${\displaystyle {\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 не может уменьшаться вечно. (Например, обычный порядок < хорошо обоснован для целых положительных чисел , но ни для целых , ни для положительных действительных чисел ; все эти множества подразумеваются в математическом, а не в вычислительном смысле, все они, в частности, бесконечны.) ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {Z} }$ ${\displaystyle \mathbb {R} ^{+}}$

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

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

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

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

${\displaystyle [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]}$

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

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

${\displaystyle [x<10\wedge 10-x=z]x:=x+1[x\leq 10\wedge 10-x<z]}$,

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

${\displaystyle [x+1\leq 10\wedge 10-x-1<z]x:=x+1[x\leq 10\wedge 10-x<z]}$получается по правилу присваивания, а

${\displaystyle [x+1\leq 10\wedge 10-x-1<z]}$может быть усилено правилом следствий. ${\displaystyle [x<10\wedge 10-x=z]}$

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

Смотрите также

• Утверждение (разработка программного обеспечения)
• Денотационная семантика
• Проектирование по договору
• Динамическая логика
• Формальная проверка
• Инвариант цикла
• Семантика преобразователя предикатов
• Статический анализ программы

Примечания

1. Первоначально Хоар написал « » вместо « ». ${\displaystyle P\{C\}Q}$ ${\displaystyle \{P\}C\{Q\}}$
2. В этой статье для правил используется естественная дедуктивная нотация. Например, неформально означает: «Если выполняются и α , и β , то выполняется и φ »; α и β называются предшественниками правила, φ называется его последователем. Правило без антецедентов называется аксиомой и записывается как . ${\displaystyle {\dfrac {\alpha ,\beta }{\phi }}}$ ${\displaystyle {\dfrac {}{\quad \phi \quad }}}$
3. Статья Хоара 1969 года не содержала правила полной корректности; ср. его обсуждение на стр.579 (вверху слева). Например, учебник Рейнольдса ^[3] дает следующую версию правила полной корректности: когда z — целочисленная переменная, которая не встречается в свободном виде в P , B , S или t , а t — целочисленное выражение (переменные Рейнольдса переименован в соответствии с настройками этой статьи). ${\displaystyle {\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]}}}$

Рекомендации

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

дальнейшее чтение

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

Внешние ссылки

• KeY-Hoare — это полуавтоматическая система проверки, построенная на базе средства доказательства теорем KeY . Он использует исчисление Хоара для простого языка while.
• j-Algo-modul Исчисление Хоара — Визуализация исчисления Хоара в программе визуализации алгоритма j-Algo