Правило получения предусловия условного оператора 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), воспользовавшись подходящими правилами вывода для этих операторов. Затем объединяем два предусловия приведенным выше образом.
