Являясь формализованым аналогом обычной логики, логика первого порядка дает возможность строго рассуждать об истинности и ложности утверждений и об их взаимосвязи, в частности, о логическом следовании одного утверждения из другого, или, например, об их эквивалентности. Рассмотрим классический пример формализации утвержденийестественного языка в логике первого порядка.
Возьмем рассуждение «Каждый человек смертен. Конфуций — человек. Следовательно, Конфуций смертен». Обозначим «x есть человек» через ЧЕЛОВЕК (x) и «x смертен» через СМЕРТЕН (x). Тогда утверждение «каждый человек смертен» может быть представлено формулой: x(ЧЕЛОВЕК (x) → СМЕРТЕН (x)) утверждение «Конфуций — человек» формулой ЧЕЛОВЕК (Конфуций), и «Конфуций смертен» формулой СМЕРТЕН (Конфуций). Утверждение в целом теперь может быть записано формулой
( x(ЧЕЛОВЕК (x) → СМЕРТЕН (x)) ЧЕЛОВЕК (Конфуций)) → СМЕРТЕН (Конфуций)
3)
Логика Хоара (англ. Hoarelogic, также Floyd—Hoarelogic, или Hoarerules) — формальная система с набором логических правил, предназначенных для доказательства корректности компьютерных программ.
|
|
Основной характеристикой логики Хоара является тройка Хоара (англ. Hoaretriple). Тройка описывает, как выполнение фрагмента кода изменяет состояние вычисления. Тройка Хоара имеет следующий вид:
где P и Q являются утверждениями (англ. assertions), а C — командой. P называется предусловием, а Q — постусловием. Если предусловие выполняется, команда делает верным постусловие. Утверждения являются формулами логики предикатов.
В логике Хоара есть аксиомы и правила вывода для всех конструкций простого императивного языка программирования. В дополнение к этим конструкциям, описанным в оригинальной работе Хоара, Хоаром и другими исследователями были разработаны правила и для остальных конструкций:одновременного выполнения, вызова процедуры, перехода и указателя.
В стандартной логике Хоара может быть доказана только частичная корректность, так как завершение программы нужно доказывать отдельно. Таким образом, «интуитивное» понимание тройки Хоара можно выразить так: если P имеет место до выполнения C, то либо имеет место Q, либо C никогда не завершится. Действительно, если C не завершается, никакого «после» нет, поэтому Q может быть любым утверждением. Более того, мы можем выбрать Q со значением «ложь», чтобы показать, что C никогда не завершится.
Полная корректность также может быть доказана с использованием расширенной версии правила для оператора While.