Понятие об алгоритмической логике Ч. Хоара

Язык алгоритмических логик сочетает язык описания программ и логический язык, что дает возможность выражать разнообразные свойства программ. Это программная или динамическая логика.

Применяется для описания свойств частичной корректности программ. Использует выражения:

(исходное состояние памяти) (программа заканчивает работу) (заключительное состояние памяти)

где P, Q – логические формулы, а A – программа.

Такая формула имеет следующий смысл: Если исходное состояние памяти (исходное значение переменных удовлетворяет условию P и программа A завершает работу над , то заключительное значение переменных удовлетворяет условию Q.

Верификация – доказательство правильности программ. Алгоритмическая логика позволяет доказать правильность (неправильность) программ без перебора всевозможных вариантов их реализации на различных сочетаниях переменных.

В [1] приводятся примеры языков алгоритмических логик, использующих высказывания вида:

{U}S{В} – «Если до исполнения оператора S будет выполнено U, то после него будет В». Здесь U – предусловие, а В – постусловие. При анализе условных операторов программы, если ни при каких вариантах не реализуется один из его выходов – фиксируется ошибка. При описании циклов, что является наиболее трудным, анализируются возможности выходов из них. Каждое состояние памяти, возникающее в ходе исполнения программы, – «возможный мир». Пути исполнения программы – переходы между «мирами». В случае тотальной корректности программа обязательно завершается: ^B. Частичная корректность:

Автоматическое доказательство правильности программ – задача до сих пор нерешенная.