Теория и практика защиты программ

Правило получения предусловия оператора присваивания


Чтобы получить предусловие для заданного постусловия Р

по отношению к заданному оператору присваивания х:=Е, подставим выражение Е вместо переменной с именем х всюду, где это имя встречается в постусловии Р. Либо, используя введенные ранее обозначения, запишем то же в следующем виде.

Правило вывода А1 – «Получение предусловия оператора присваивания»

(РхЕ} х:=Е{Р} <

 

Значение х после выполнения оператора присваивания х:=Е будет таким же, как и значение Е перед его выполнением. Значение у будет неизменным (на основании допущения, что не должно появляться «побочных эффектов»). Здесь переменная у обозначает все те переменные программы, которые отличны от х. Таким образом, значение Р(х,у) после выполнения оператора присваивания будет равно значению Р(Е,у) до его выполнения. Следовательно, из истинности Р(Е,у) до выполнения следует истинность Р(х,у) после выполнения, то есть Р(Е,у) является предусловием для Р(х,у) по отношению к оператору присваивания х:=Е.



Содержание раздела