Semantique Axiomatique VIII: les Instructions de Selection

• If-then-else:

{B and P} S1 {Q}, {(not B) and P} S2 {Q}

{P} if B then S1 else S2 {Q}

• If-then:

{B and P} S1 {Q}, {(not B) and P} => Q

{P} if B then S1 {Q}

Previous slide

Next slide

Back to first slide

View graphic version