Правило проверки предусловия оператора присваивания
Правило вывода А2 – «Проверка предусловия оператора присваивания»
If
VÞPxЕ
then
{V} x:=E{P} <
Правило вывода А2 представляет собой комбинацию правил вывода A1 и P1. Из правила вывода P1 следует, что V является предусловием для Р по отношению к оператору присваивания, если (V=РxЕ) and {РxЕ} х:=Е{Р}.
Из правила вывода A1 следует, что {РxЕ } х:=Е{Р}. Поэтому достаточно показать, что VÞРxЕ, если желательно проверить, что {V} х:=Е{Р}.
При применении правила вывода А2
неявно используются два правила вывода (A1
и P1). И действительно, правило вывода A1 используется для получения предусловия. Затем проверяется, что из заданного предусловия вытекает полученное предусловие, то есть, что гипотеза правила вывода P1 удовлетворяется.
