Логика Хоара

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

Логика Хоара (также известная как логика Флойда–Хоара или правила Хоара ) — формальная система с набором логических правил для строгого рассуждения о корректности компьютерных программ . Она была предложена в 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 относятся к одной и той же переменной ( псевдоним ), хотя это правильный пример схемы аксиом присваивания (при этом и x, и y являются ). ${\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 loop, do...until loop, switch , break , continue могут быть сведены к правилам из оригинальной статьи Хоара путем преобразования программы .

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

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

для части else .

Однако правило назначения для части 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\}}$

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

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

по правилу while требуется доказать

${\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 должен был содержать (случайно) значение квадратного корня a . Во всех остальных случаях она не завершится; поэтому она не полностью верна.

В то время как правило для полной корректности

Если вышеприведенное обычное правило 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. Hoare, CAR (октябрь 1969). "Аксиоматическая основа компьютерного программирования". Communications of the ACM . 12 (10): 576–580. doi : 10.1145/363235.363259 . S2CID  207726175.
2. RW Floyd . «Придание значений программам». Труды симпозиумов Американского математического общества по прикладной математике. Т. 19, стр. 19–31. 1967.
3. Джон К. Рейнольдс (2009). Теории языков программирования . Cambridge University Press.) Здесь: Раздел 3.4, стр. 64.
4. Хоар (1969), стр.578-579
5. Хут, Майкл; Райан, Марк (2004-08-26). Логика в информатике (второе изд.). CUP. стр. 276. ISBN 978-0521543101.
6. Апт, Кшиштоф Р.; Ольдерог, Эрнст-Рюдигер (декабрь 2019 г.). «Пятьдесят лет логики Хоара». Формальные аспекты вычислений . 31 (6): 759. doi :10.1007/s00165-019-00501-3. S2CID  102351597.

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

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

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

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