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

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

Хоар тройной

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

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

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

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

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

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

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

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

Правила

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

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

${\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 \{x+1=43\}y:=x+1\{y=43\}}$
• ${\displaystyle \{x+1\leq N\}x:=x+1\{x\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 \{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\}}$

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

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

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

Условное правило гласит, что постусловие ${\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}}\}}$

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

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

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

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

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

Если выше обычного в то время как правило заменяется следующим, исчисление Хоара также может быть использовано для доказательства полная правильность, т.е. прекращение^{[заметка 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} ^{+}}$; все эти множества подразумеваются в математическом, а не в вычислительном смысле, в частности, все они бесконечны.)

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

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

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

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

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

Примечания

1. Первоначально Хоар написал "${\displaystyle P\{C\}Q}$" скорее, чем "${\displaystyle \{P\}C\{Q\}}$".
2. В этой статье используется естественный вычет обозначение стиля для правил. Например, ${\displaystyle {\dfrac {\alpha ,\beta }{\phi }}}$ неофициально означает "Если оба ${\displaystyle \alpha }$ и ${\displaystyle \beta }$ держись, тогда также ${\displaystyle \phi }$ держит "; ${\displaystyle \alpha }$ и ${\displaystyle \beta }$ называются антецедентами правила, ${\displaystyle \phi }$ называется его преемником. Правило без антецедентов называется аксиомой и записывается как ${\displaystyle {\dfrac {}{\quad \phi \quad }}}$.
3. «Завершение» здесь означает в более широком смысле, что вычисление в конечном итоге будет завершено; оно делает нет подразумевают, что никакое нарушение предела (например, нулевое деление) может преждевременно остановить программу.
4. В статье Хоара 1969 года не было правила полной правильности; ср. его обсуждение на стр.579 (вверху слева). Например, учебник Рейнольдса (Джон С. Рейнольдс (2009). Теория языков программирования. Издательство Кембриджского университета.), Раздел 3.4, стр.64 дает следующую версию правила полной корректности: ${\displaystyle {\dfrac {P\wedge B\rightarrow 0\leq t\quad ,\quad [P\wedge B\wedge t=z]S[P\wedge t<z]}{[P]{\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {done}}[P\wedge \neg B]}}}$ когда ${\displaystyle z}$ - целочисленная переменная, которая не встречается бесплатно в ${\displaystyle P}$, ${\displaystyle B}$, ${\displaystyle S}$, или же ${\displaystyle t}$, и ${\displaystyle t}$ является целочисленным выражением (переменные Рейнольдса переименованы, чтобы соответствовать настройкам этой статьи).

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

1. Хоар, К.А.Р. (Октябрь 1969 г.). «Аксиоматическая основа компьютерного программирования» (PDF). Коммуникации ACM. 12 (10): 576–580. Дои:10.1145/363235.363259.
2. Р. В. Флойд. "Придание смысла программам. "Труды симпозиумов Американского математического общества по прикладной математике. Том 19, стр. 19–31. 1967.
3. стр.579 вверху слева
4. Хут, Майкл; Райан, Марк (2004-08-26). Логика в информатике (второе изд.). КРУЖКА. п. 276. ISBN  978-0521543101.

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

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

внешняя ссылка

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