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

Листинг 6.5. Правило вывода IF1 —"Проверка предусловия условного оператора if"

Если условие V истинно перед выполнением условного оператора if, то и У, и В истинны непосредственно перед выполнением ОР1 (если этот оператор выполняется). Поскольку { V and В} является предусловием для Р по отношению к OP 1, то Р будет истинным после выполнения ОР1. Поступая аналогичным образом, получаем, что Р будет истинным после выполнения ОР2. Таким образом, из истинности V перед выполнением условного оператора в обоих случаях следует истинность Р после его выполнения. Поэтому V является предусловием для Р по отношению к условному оператору целиком.

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

Листинг 6.6. Правило вывода IF2—"Получение предусловия условного оператора ifi>

В действительности правило вывода IF2 представляет правило вывода IF1 с.

Правило вывода IF2 следует из правил вывода IF1 и Р1. Применяя правило вывода IF2, можно получить предусловие заданного постусловия Р по отношению к заданному условному оператору. Сначала получаем предусловия для Р по отношению к частям then и else (в выражениях OP 1 и 0Р2), воспользовавшись подходящими правилами вывода для этих операторов. Затем объединяем два предусловия приведенным выше образом.