Логика Хоара ( англ. Hoare logic , также Floyd—Hoare logic , или Hoare rules ) — формальная система с набором логических правил, предназначенных для доказательства (англ.) ( компьютерных программ . Была предложена в 1969 году английским учёным в области информатики и математической логики Хоаром , позже развита самим Хоаром и другими исследователями. Первоначальная идея была предложена в работе Флойда , который опубликовал похожую систему в применении к блок-схемам ( англ. flowchart ).

Тройки Хоара

Основной характеристикой логики Хоара является тройка Хоара ( англ. Hoare triple ). Тройка описывает, как выполнение фрагмента кода изменяет состояние вычисления. Тройка Хоара имеет следующий вид:

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

где P и Q являются утверждениями ( англ. assertions ), а C — командой . P называется предусловием ( антецедент ), а Q — постусловием ( консеквент ). Если предусловие выполняется, команда делает верным постусловие. Утверждения являются формулами логики предикатов .

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

Основная идея Хоара — дать для каждой конструкции императивного языка пред- и постусловие , записанное в виде логической формулы. Поэтому и возникает в названии тройка — предусловие , конструкция языка, постусловие .

• Ясно, что для пустого оператора пред- и постусловия совпадают.
• Для оператора присваивания в постусловии кроме предусловия должен учитываться факт, что значение переменной стало другим.
• Для составного оператора (в Python это отступы, в C это {} ) имеем цепочку пред- и постусловий . В результате для составного оператора можно оставить первое предусловие и последнее постусловие .
• Правило вывода говорит, что можно усилить пред и ослабить постусловие , если нам это понадобится. Нет смысла сохранять всю программу какое-то утверждение, которое не помогает решить поставленную задачу.
• Оператор ветвления или просто if . Его условно можно разбить на две ветки: then и else . Если к предусловию добавить истинность логического условия (то, что стоит под if ), то после выполнения ветки then должно следовать постусловие . Аналогично, если к предусловию добавить отрицание логического условия (то, что стоит под if ), то после выполнения ветки else должно следовать постусловие
• Оператор цикла. Это самое нетривиальное и сложное, поскольку цикл может выполняться много раз и даже не закончиться. Чтобы решить проблему возможного многократного повтора тела цикла вводят инвариант цикла . Инвариант цикла — это то, что истинно перед его выполнением, истинно после каждого выполнения тела цикла и, следовательно, истинно и после его окончания. Предусловие для оператора цикла — это просто его инвариант цикла . Если истинно условие продолжения цикла (то, что стоит под while ), то после выполнения тела цикла должна следовать истинность инвариант цикла . В результате, после окончания цикла имеем в качестве постусловия истинность инвариант цикла и отрицание условия продолжения цикла.
• Оператора цикла с полной корректностью. Для этого к предыдущему пункту добавляют ограничивающую функцию, с помощью которой легко доказать, что цикл будет выполняться ограниченное число раз. На неё накладывают условия, что она всегда >=0, строго убывает после каждого выполнения тела цикла и в точности = 0, когда цикл заканчивается.

Правильно работающую программу можно написать очень многими способами, и во многих случаях она будет эффективной. Эта неоднозначность усложняет программирование. Для этого вводят стиль. Но этого оказывается мало. Для многих программ (например, связанных косвенно с жизнью человека) нужно доказать и их корректность. Оказалось, что доказательство корректности делает программу дороже на порядок (примерно в 10 раз). ^{[ источник не указан 2235 дней ]}

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

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

Полная корректность также может быть доказана с использованием расширенной версии правила для оператора While .

Правила

Аксиома пустого оператора

Правило для пустого оператора утверждает, что оператор skip ( пустой оператор ) не меняет состояния программы, поэтому утверждение, верное до skip , остаётся верным после его выполнения.

${\displaystyle {\frac {}{\{P\}\ {\textbf {skip}}\ \{P\}}}}$

Аксиома оператора присваивания

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

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

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

Смысл аксиомы присваивания заключается в том, что истинность ${\displaystyle \{P[E/x]\}}$ эквивалентна ${\displaystyle \{P\}}$ после выполнения присваивания. Таким образом, если ${\displaystyle \{P[E/x]\}}$ имело значение «истина» до присваивания, согласно аксиоме присваивания ${\displaystyle \{P\}}$ будет иметь значение «истина» после присваивания. И наоборот, если ${\displaystyle \{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=3\}\ x:=2\ \{y=3\}}$

является неверным утверждением, если x и y ссылаются на одну и ту же переменную, так как никакое предусловие не может обеспечить, чтобы y было равно 3 после того, как x присвоено 2.

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

Правило композиции Хоара применяется к последовательному выполнению программ S и T , где S выполняется до T , что записывается как S;T .

${\displaystyle {\frac {\{P\}\ S\ \{Q\}\ ,\ \{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 {\frac {\{B\wedge P\}\ S\ \{Q\}\ ,\ \{\neg B\wedge P\}\ T\ \{Q\}}{\{P\}\ {\textbf {if}}\ B\ {\textbf {then}}\ S\ {\textbf {else}}\ T\ {\textbf {endif}}\ \{Q\}}}}$

Правило вывода

${\displaystyle {\frac {P^{\prime }\rightarrow \ P\ ,\ \lbrace P\rbrace \ S\ \lbrace Q\rbrace \ ,\ Q\rightarrow \ Q^{\prime }}{\lbrace P^{\prime }\ \rbrace \ S\ \lbrace Q^{\prime }\rbrace }}}$

Правило оператора цикла

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

Здесь P является инвариантом цикла .

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

${\displaystyle {\frac {<\;{\text{is well-founded,}}\;[P\wedge B\wedge t=z]\ S\ [P\wedge t<z]}{[P]\ {\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {done}}\ [\neg B\wedge P]}}}$

В этом правиле, кроме сохранения инварианта цикла, доказывается цикла при помощи терма , называемого (здесь t ), значение которого строго уменьшается согласно (well-founded relation) " < " с каждой итерацией. При этом условие B должно подразумевать, что t не является минимальным элементом своей области определения, в противном случае посылка данного правила будет ложной. Поскольку отношение " < " является полностью фундированным, каждый шаг цикла определяется уменьшающимися членами конечного линейно упорядоченного множества .

В записи данного правила используются квадратные, а не фигурные скобки, для того чтобы обозначить полную корректность правила. (Это один из вариантов обозначения полной корректности.)

Примеры

Пример 1

${\displaystyle \{x+1=43\}\ y:=x+1\ \{y=43\}}$ — на основании аксиомы присваивания.

Поскольку ${\displaystyle (x+1=43\Leftrightarrow x=42)}$ , на основании правила вывода получаем:

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

Пример 2

${\displaystyle \{x+1\leq N\}\ x:=x+1\ \{x\leq N\}}$ — на основании аксиомы присваивания.

Если x и N целые, то ${\displaystyle (x<N)\implies (x+1\leq N)}$ , и на основании правила вывода получаем:

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

См. также

• Тестирование программного обеспечения
• Контрактное программирование
• Формальная верификация
• Сепарационная логика

Ссылки

Литература

• Гуц А. К. Математическая логика и теория алгоритмов. — М. : Книжный дом "ЛИБРОКОМ", 2009. — 117 с. — ISBN 9785397000567 .