Аксиома присваивания
Пусть х := Е — оператор присваивания с постусловием Q. Тогда его предусловие, определяемое по аксиоме
означает, что Р вычисляется как Q, в котором все вхождения переменной х замещаются на Е, то есть на выражение из правой части оператора.
Аксиома записывается в виде следующей тройки:
Повторим, что аксиоматическая семантика разрабатывается для доказательства правильности программ. С этой точки зрения оператор присваивания с предусло
192 |
Глава 7. Формальная семантика языков программирования |
вием и постусловием может рассматриваться как теорема. Если аксиома присваивания при применении к постусловию и оператору вырабатывает «правильное» предусловие, то теорема доказана. |
Применение аксиомы присваивания Рассмотрим примеры применения аксиомы присваивания, то есть примеры доказательства теорем по поводу операторов присваивания. Пусть исходные данные для доказательства теоремы имеют вид:
Тогда для заданного оператора а := Ь/2 + 1 слабейшее предусловие вычисляется подстановкой в постусловие {а < 50} вместо а выражения Ь/2 + 1:
Как использовать этот результат? Достаточно проверить соблюдение предусловия и постусловия в ходе реальных вычислений. Еще один пример. Для заданной пары |
слабейшее предусловие равно: |