Логика Хоара

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

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

Тройки Хоара[править | править вики-текст]

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

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

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

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

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

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

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

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

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

Правила[править | править вики-текст]

Аксиома пустого оператора[править | править вики-текст]

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

Аксиома оператора присваивания[править | править вики-текст]

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

Здесь означает выражение P в котором все вхождения свободной переменной x заменены выражением E.

Смысл аксиомы присваивания заключается в том, что истинность эквивалентна после выполнения присваивания. Таким образом, если имело значение «истина» до присваивания, согласно аксиоме присваивания будет иметь значение «истина» после присваивания. И наоборот, если было равно «ложь» до оператора присваивания, должно быть равно «ложь» после.

Примеры корректных троек:

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

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

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

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

Например, рассмотрим два экземпляра аксиомы присваивания:

и

Согласно правилу композиции, мы получаем:

Правило условного оператора[править | править вики-текст]

Правило вывода[править | править вики-текст]

Правило оператора цикла[править | править вики-текст]

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

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

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

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

Примеры[править | править вики-текст]

Пример 1
— на основании аксиомы присваивания.
Поскольку , на основании правила вывода получаем:
Пример 2
— на основании аксиомы присваивания.
Если x и N целые, то , и на основании правила вывода получаем:

См. также[править | править вики-текст]

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

  1. C. A. R. Hoare. «An axiomatic basis for computer programming». Communications of the ACM, 12(10):576—580,583 October 1969. DOI:10.1145/363235.363259
  2. R. W. Floyd. «Assigning meanings to programs. (недоступная ссылка с 13-05-2013 (1227 дней) — история)» Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19-31. 1967.

Литература[править | править вики-текст]