<<
>>

Аксиома присваивания

Эта аксиома «обслуживает», то есть позволяет «доказать» оператор присваивания.

Пусть х := Е — оператор присваивания с постусловием Q. Тогда его предусловие, определяемое по аксиоме

означает, что Р вычисляется как Q, в котором все вхождения переменной х замещаются на Е, то есть на выражение из правой части оператора.

Аксиома записывается в виде следующей тройки:

Повторим, что аксиоматическая семантика разрабатывается для доказательства правильности программ. С этой точки зрения оператор присваивания с предусло

192

Глава 7.
Формальная семантика языков программирования

вием и постусловием может рассматриваться как теорема. Если аксиома присваивания при применении к постусловию и оператору вырабатывает «правильное» предусловие, то теорема доказана.

Применение аксиомы присваивания

Рассмотрим примеры применения аксиомы присваивания, то есть примеры доказательства теорем по поводу операторов присваивания.

Пусть исходные данные для доказательства теоремы имеют вид:

Тогда для заданного оператора а := Ь/2 + 1 слабейшее предусловие вычисляется подстановкой в постусловие {а < 50} вместо а выражения Ь/2 + 1:

Как использовать этот результат? Достаточно проверить соблюдение предусловия и постусловия в ходе реальных вычислений.

Еще один пример. Для заданной пары

слабейшее предусловие равно:

<< | >>

Еще по теме Аксиома присваивания:

  1. Вот общий итог Трёх Аксиом Справедливости.
  2. Введение
  3. Литература
  4. Хирон в VII поле
  5. Сексуальные отношения с возрастом не должны угасать, а наоборот, развиваться и переходить в новое качество
  6. Справедливость на работе
  7. УМЕНИЕ ЛЮБИТЬ и УМЕНИЕ БЫТЬ ЛЮБИМЫМ.
  8. ГИП. Тест-психологема "Такси".
  9. Я ХОРОШИЙ Я ЛЮБИМЫЙ
  10. Современная ситуация