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

       

Правило проверки предусловия условного оператора 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 (если этот оператор выполняется). Поскольку (V and В) является предусловием для Р

по отношению к OP1, то Р будет истинным после выполнения OP1. Поступая аналогичным образом, получаем, что Р

будет истинным после выполнения OP2. Таким образом, из истинности V

перед выполнением условного оператора в обоих случаях следует истинность Р после его выполнения. Поэтому V является предусловием для Р по отношению к условному оператору целиком.



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