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

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

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

(Р^х_Е} х:=Е{Р} 

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

3. Правило проверки предусловия оператора присваивания

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

If

VP^x_Е

then

{V} x:=E{P} 

Правило вывода А2представляет собой комбинацию правил выводаA1иP1. Из правила выводаP1следует, чтоVявляется предусловием для Рпо отношению к оператору присваивания, если (V=Р^x_Е)and{Р^x_Е} х:=Е{Р}.

Из правила вывода A1следует, что {Р^x_Е} х:=Е{Р}. Поэтому достаточно показать, чтоVР^x_Е, если желательно проверить, что {V} х:=Е{Р}.

При применении правила вывода А2неявно используются два правила вывода (A1иP1). И действительно, правило выводаA1используется для получения предусловия. Затем проверяется, что из заданного предусловия вытекает полученное предусловие, то есть, что гипотеза правила выводаP1удовлетворяется.

4. Правило проверки предусловия условного оператора if

Правило вывода IF1 – «Проверка предусловия условного оператора if»

If

{V and B} OP1 {P} and

{V and not B} OP2 {Р}

then

{V} if В then OP1 else OP2 endif {P} 

Если условие Vистинно перед выполнением условного оператора if, то иV, иВистинны непосредственно перед выполнениемOP1 (если этот оператор выполняется). Поскольку (VandВ) является предусловием для Рпо отношению кOP1, тоРбудет истинным после выполнения OP1. Поступая аналогичным образом, получаем, чтоРбудет истинным после выполненияOP2. Таким образом, из истинностиVперед выполнением условного оператора в обоих случаях следует истинностьРпосле его выполнения. ПоэтомуVявляется предусловием дляРпо отношению к условному оператору целиком.

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

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

If

{V1} OP1 {P} and

{V2} OP2 {Р}

then

((V1 and В) or (V2 and not B)}

if В then OP1 else OP2 endif {P} 

В действительности правило вывода IF2представляет правило вывода IF1сV=[(V1 and В) or (V2 and not В)]. Правило выводаIF2следует из правил выводаIF1иP1. Применяя правило выводаIF2, можно получить предусловие заданного постусловияРпо отношению к заданному условному оператору. Сначала получаем предусловия для Рпо отношению к частям then и else (в выраженияхOP1 иOP2), воспользовавшись подходящими правилами вывода для этих операторов. Затем объединяем два предусловия приведенным выше образом.