Логика Хоара - Hoare logic

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

Хоар тройной

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

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

где и - утверждения, а - команда . названо в предпосылке и в постусловии : когда предварительное условие выполнено, выполнение команды устанавливает постусловие. Утверждения - это формулы в логике предикатов . ${\ 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 года Хоар использовал более узкое понятие завершения, которое также влекло за собой отсутствие каких-либо ошибок времени выполнения: «Отказ завершить может быть из-за бесконечного цикла; или это может быть из-за нарушения определенного реализацией лимита для например, диапазон числовых операндов, размер хранилища или ограничение времени операционной системы ».

Правила

Схема аксиомы пустого оператора

Пустое утверждение правило утверждает , что пропуск оператор не изменяет состояние программы, таким образом , все , что справедливо , прежде чем пропустить справедливо и впоследствии.

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

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

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

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

где обозначает утверждение P , в которой каждый свободное вхождение из й было заменено выражением Е . ${\ 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 \ {х + 1 = 43 \} у: = х + 1 \ {у = 43 \}}$
• ${\ Displaystyle \ {х + 1 \ Leq N \} х: = х + 1 \ {х \ 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 \ {х = 5 \} х: = 3 \ {3 = 5 \}}$

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

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

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

• ${\ Displaystyle \ {0 \ Leq Y \ CDOT Y \ клин у \ CDOT Y \ Leq 9 \} х: = Y \ CDOT Y \ {0 \ Leq 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 \ клин у \ CDOT Y \ Leq 9 \} х: = Y \ CDOT Y \ {0 \ Leq Y \ CDOT Y \ клин х \ Leq 9 \}}$, и
• ${\ Displaystyle \ {0 \ Leq Y \ CDOT Y \ клин у \ CDOT Y \ Leq 9 \} х: = Y \ CDOT Y \ {0 \ Leq Y \ CDOT Y \ клин у \ CDOT Y \ Leq 9 \} }$

являются допустимыми примерами схемы аксиомы присваивания.

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

${\ Displaystyle \ {у = 3 \} х: = 2 \ {у = 3 \}}$

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

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

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

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

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

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

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

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

и

${\ Displaystyle \ {Y = 43 \} Z: = Y \ {Z = 43 \}}$

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

${\ Displaystyle \ {х + 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 . В частях then и else необязательное и отрицательное условие B может быть добавлено к предусловию P соответственно. Состояние B не должно иметь побочных эффектов. Пример приведен в следующем разделе .

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

${\ 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 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 х \ Leq 15 \ клин х <15 \} х: = х + 1 \ {0 \ Leq х \ Leq 15 \}}$, или упрощенный

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

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

${\ Displaystyle \ {0 \ Leq х \ Leq 15 \ клин х \ GEQ 15 \} х: = 0 \ {0 \ Leq х \ Leq 15 \}}$, или упрощенный

${\ Displaystyle \ {х = 15 \} х: = 0 \ {0 \ leq x \ leq 15 \}}$

для другой части.

Однако правило присваивания для части then требует выбора P как ; применение правила, следовательно, дает ${\ Displaystyle 0 \ Leq х \ 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 х <15 \}}$

Точно так же для части else правило присваивания дает

${\ Displaystyle \ {0 \ Leq 0 \ Leq 15 \} х: = 0 \ {0 \ Leq х \ Leq 15 \}}$, или эквивалентно

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

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

Пока правило

${\ displaystyle {\ dfrac {\ {P \ wedge B \} S \ {P \}} {\ {P \} {\ texttt {while}} \ B \ {\ texttt {do}} \ S \ {\ texttt {готово}} \ {\ neg B \ wedge 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 \ клин х \ leq 10 \}}$

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

${\ Displaystyle \ {х \ Leq 10 \ клин х <10 \} х: = х + 1 \ {х \ Leq 10 \}}$, или упрощенный

${\ Displaystyle \ {х <10 \} х: = х + 1 \ {х \ leq 10 \}}$,

которое легко получается с помощью правила присваивания. Наконец, постусловие можно упростить до . ${\ Displaystyle \ {\ отр х <10 \ клин х \ Leq 10 \}}$${\ Displaystyle \ {х = 10 \}}$

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

${\ displaystyle \ {{\ texttt {true}} \} {\ texttt {while}} \ x \ cdot x \ neq a \ {\ texttt {do}} \ {\ texttt {skip}} \ {\ texttt { готово}} \ {x \ cdot x = a \ wedge {\ texttt {true}} \}}$

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

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

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

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

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

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

${\ Displaystyle {\ dfrac {<\ {\ text {- это хорошо обоснованный порядок на множестве}} \ D \ quad, \ quad [P \ клин B \ клин t \ in D \ клин 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 \ клин P \ клин t \ in D]}}}$

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

Учитывая инвариант цикла P , условие B должно означать , что т не является минимальный элемент из D , иначе тело S не может уменьшить T дальше, то есть помещение правила было бы неверно. (Это одно из различных обозначений для полной правильности.)

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

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

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

${\ Displaystyle [х \ Leq 10 \ клин х <10 \ клин 10-х \ geq 0 \ клин 10-х = z] х: = х + 1 [х \ Leq 10 \ клин 10-х \ geq 0 \ клин 10-x <z]}$

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

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

${\ displaystyle [x <10 \ клин 10-x = z] x: = x + 1 [x \ leq 10 \ клин 10-x <z]}$,

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

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

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

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

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

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

Примечания

использованная литература

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

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

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

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