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

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



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