Интернет магазин китайских планшетных компьютеров



Компьютеры - Логика Хоара

23 января 2011


Оглавление:
1. Логика Хоара
2. Частичная и полная корректность
3. Примеры



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

Тройки Хоара

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

\{P\}\;C\;\{Q\}

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

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



Просмотров: 2174


<<< Логика в информатике
Лямбда-исчисление >>>