2015-03-27
852
Язык алгоритмических логик сочетает язык описания программ и логический язык, что дает возможность выражать разнообразные свойства программ. Это программная или динамическая логика.
Применяется для описания свойств частичной корректности программ. Использует выражения:
(исходное состояние памяти) (программа заканчивает работу) (заключительное состояние памяти)
где P, Q – логические формулы, а A – программа.
Такая формула имеет следующий смысл: Если исходное состояние памяти (исходное значение переменных 
удовлетворяет условию P и программа A завершает работу над 
, то заключительное значение переменных удовлетворяет условию Q.
Верификация – доказательство правильности программ. Алгоритмическая логика позволяет доказать правильность (неправильность) программ без перебора всевозможных вариантов их реализации на различных сочетаниях переменных.
В [1] приводятся примеры языков алгоритмических логик, использующих высказывания вида:
{U}S{В} – «Если до исполнения оператора S будет выполнено U, то после него будет В». Здесь U – предусловие, а В – постусловие. При анализе условных операторов программы, если ни при каких вариантах не реализуется один из его выходов – фиксируется ошибка. При описании циклов, что является наиболее трудным, анализируются возможности выходов из них. Каждое состояние памяти, возникающее в ходе исполнения программы, – «возможный мир». Пути исполнения программы – переходы между «мирами». В случае тотальной корректности программа обязательно завершается: ^B. Частичная корректность: 
|
|
|
Автоматическое доказательство правильности программ – задача до сих пор нерешенная.
