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

       

В then OP1 else OP2


Правило вывода IFЗ – «Условный оператор if»

If

{V1} OP1 {P} and

{V2} OP2 {Р}

then

{V1 and V2} if В then OP1 else OP2 endif {P} <

Правило вывода IF3

представляет собой слабую теорему, которая следует из правил вывода IF1 и P1. Благодаря простой форме образующих ее выражений, на практике иногда она оказывается удобной для применения.


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