Логика Хоара

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

Hoare Triple [ править ]

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

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

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

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

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

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

Полная корректность также может быть доказана с помощью расширенной версии правила While. ^{[ необходима цитата ]}

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

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

Схема аксиомы пустого оператора [ править ]

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

${\ Displaystyle {\ dfrac {} {\ {P \} {\ textbf {skip}} \ {P \}}}}$

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

Аксиома присваивания утверждает, что после присваивания любой предикат, который ранее был истинным для правой части присваивания, теперь выполняется для переменной. Формально, пусть будет утверждение , в котором переменная является свободным . Потом:${\ displaystyle P}$${\ displaystyle x}$

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

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

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

Примеры действительных троек включают:

• ${\ Displaystyle \ {х + 1 = 43 \} у: = х + 1 \ {у = 43 \}}$
• ${\ Displaystyle \ {х + 1 \ Leq N \} х: = х + 1 \ {х \ Leq N \}}$

Все предусловия, которые не изменяются выражением, могут быть перенесены в постусловие. В первом примере присвоение не меняет того факта, что оба оператора могут появиться в постусловии. Формально этот результат получается путем применения схемы аксиом с бытием ( и ), что дает бытие ( и ), которое, в свою очередь, может быть упрощено до данного предусловия .${\ displaystyle y: = x + 1}$${\ displaystyle x + 1 = 43}$${\ displaystyle P}$${\ 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 \ {х = 5 \} х: = 3 \ {3 = 5 \}}$

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

${\ Displaystyle \ {х = 5 \} х: = х + 1 \ {х = 5 \ клин х = х + 1 \}}$

Хотя данное постусловие однозначно определяет предусловие , обратное неверно. Например:${\ displaystyle 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\}}$

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

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

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

Три приведенных ниже оператора (строки 2, 4, 6) обмениваются значениями переменных и без необходимости во вспомогательной переменной. В проверочном доказательстве начальное значение и обозначается константой и соответственно. Доказательство лучше читать задом наперед, начиная со строки 7; например, строка 5 получается из строки 7 заменой (целевое выражение в строке 6) на (исходное выражение в строке 6). Некоторые арифметические упрощения используются неявно, а именно. (строка 5 → 3) и (строка 3 → 1).${\displaystyle a}$${\displaystyle b}$${\displaystyle a}$${\displaystyle b}$${\displaystyle A}$${\displaystyle B}$${\displaystyle a}$${\displaystyle a-b}$${\displaystyle a-(a-b)=b}$${\displaystyle a+b-b=a}$ № Код Утверждения 1:       ${\displaystyle \{a=A\wedge b=B\}}$ 2: ${\displaystyle a:=a+b;}$       3: ${\displaystyle \{a-b=A\wedge b=B\}}$ 4: ${\displaystyle b:=a-b;}$ 5: ${\displaystyle \{b=A\wedge a-b=B\}}$ 6: ${\displaystyle a:=a-b}$ 7: ${\displaystyle \{b=A\wedge a=B\}}$

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

${\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\}{\textbf {if}}\ B\ {\textbf {then}}\ S\ {\textbf {else}}\ T\ {\textbf {endif}}\{Q\}}}}$

Условное правило гласит , что Постусловие общего для и части также Постусловие всего заявления. В и в стороны, unnegated и инвертированный условие может быть добавлен к предпосылке , соответственно. Состояние не должно иметь побочных эффектов. Пример приведен в следующем разделе .${\displaystyle Q}$${\displaystyle {\textbf {then}}}$${\displaystyle {\textbf {else}}}$${\displaystyle {\textbf {if}}\cdots {\textbf {endif}}}$${\displaystyle {\textbf {then}}}$${\displaystyle {\textbf {else}}}$${\displaystyle B}$${\displaystyle P}$${\displaystyle B}$

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

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

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

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

условное правило может быть получено из других правил Хоара. Аналогичным образом, правила для других производных программных конструкций, как петли, петля, , , может быть уменьшены путем преобразования программы с правилами из оригинальной работы Хоары.${\displaystyle {\textbf {for}}}$${\displaystyle {\textbf {do}}\cdots {\textbf {until}}}$${\displaystyle {\textbf {switch}}}$${\displaystyle {\textbf {break}}}$${\displaystyle {\textbf {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}\}}}}$

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

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

${\displaystyle \{0\leq x\leq 15\}{\textbf {if}}\ x<15\ {\textbf {then}}\ x:=x+1\ {\textbf {else}}\ x:=0\ {\textbf {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 {\textbf {then}}}$

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

со стороны.${\displaystyle {\textbf {else}}}$

Однако правило присвоения детали требует выбора как ; применение правила, следовательно, дает${\displaystyle {\textbf {then}}}$${\displaystyle 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 {\textbf {else}}}$

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

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

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

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

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

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

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

${\displaystyle \{x\leq 10\}{\textbf {while}}\ x<10\ {\textbf {do}}\ x:=x+1\ {\textbf {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 можно использовать для формальной проверки следующей странной программы для вычисления точного квадратного корня из произвольного числа - даже если это целочисленная переменная, а не квадратное число:${\displaystyle x}$${\displaystyle a}$${\displaystyle x}$${\displaystyle a}$

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

После применения правила времени с бытием остается доказать${\displaystyle P}$${\displaystyle {\textbf {true}}}$

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

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

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

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

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

${\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]{\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {done}}[\neg B\wedge P\wedge t\in D]}}}$

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

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

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

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

может быть применено правило while для полной правильности, например, когда это неотрицательные целые числа с обычным порядком, а выражение является , что, в свою очередь, требует доказательства${\displaystyle D}$${\displaystyle 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]}$

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

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

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

Заметки [ править ]

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

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

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

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

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