Правила вывода для операторов ветвления.
Для выполнения P/\B после выполнения оператора S1 постусловием было бы Q, и если бы выполнилось P/\¬B, то после выполнения оператора S2 постусловием было бы Q.
|
\/
___ B ___
P/\B
| | P/\¬B
S1 S2
|___________|
| Q
\/
Полный условный оператор
{P/\B}S1{Q}, {P/\¬B}S2{Q}
{P} if (B) S1, else S2 {Q}
Если оператор неполный:
{P/\B}S1{Q}, P/\¬B -> Q
{P} if (B) S1 {Q}
Правила вывода циклов с предусловием и посусловием.
Оператор цикла с предусловием:
{ P /\ B } S { P }
{P} while (B) {P/\¬B} P – инвариант цикла
| P
----- \/
|
| B нет
| |
P | да | P/\B | P/\¬B
| \/ |
| S
|______|
Цикл с постусловием
{P} S {Q}, Q/\B -> P
{P} do S while (B) {Q/\¬B}
----- | P
| \/
| S
| | Q
| \/
|
| B нет
| | Q/\¬B
| Q/\B | |