Правило условного оператора if № 1

Листинг 6.7. Правило вывода IF3 — «Условный оператор if»

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

Правило условного оператора i/№ 2

Листинг 6.8. Правило вывода IF4 — «Условный оператор if»

Правило вывода IF4 также следует из правил вывода IF1 и Р1. Подобно правилу вывода IF3, оно обладает определенной практической полезностью вследствие простоты формы предусловия { VI and V2}.

Правило последовательности операторов

Листинг 6.9. Правило вывода S1 —"Последовательность операторов".

Правило вывода S1 очевидным образом обобщается на последовательность операторов произвольной длины. Таким образом, для того чтобы отыскать предусловие для заданного постусловия по отношению к последовательности операторов, сначала отыщем предусловие для Р по отношению к последнему оператору последовательности. Затем воспользуемся им в качестве постусловия по отношению к предыдущему, предпоследнему, оператору и так далее, т. е. будем продвигаться от оператора к оператору по последовательности в обратном направлении. Полученное таким образом предусловие по отношению к первому оператору последовательности является также предусловием для Р по отношению ко всей последовательности.