Дополнения о правилах вывода для условного оператора

Лекция 5

0. Дополнения о правилах вывода для условного оператора

14.04.2015

О схемах программ

10.03.2015

Условный оператор

{P & B} S1 {Q} , {P & !B} S2 {Q}
_____________________________________________________
{P}  if (B)  S1; else S2;  {Q}.

Верификация программ

10.03.2015

Доказательство

P

P & !B

P & B

Q

{P & B} S1 {Q} , {P & !B} S2 {Q}
_______________________________________________
{P} if (B) S1; else S2; {Q}

Верификация программ

10.03.2015

Правило 5.2.

(P1&B) ∨(P2&!B)

P2

P1

Q

{P1} S1 {Q} , {P2} S2 {Q}
_______________________________________________
{(P1&B)∨(P2&!B)} if (B) S1; else S2; {Q}

Верификация программ

10.03.2015

Правило 5.3.

P1&P2

P2&!B

P1&B

Q

{P1&B} S1 {Q} , {P2&!B} S2 {Q}
_______________________________________________
{P1&P2} if (B) S1; else S2; {Q}

Верификация программ