Semantique Axiomatique VII: Sequences d’instructions

Etant donne deux instructions adjacentes avec les pre- et post- conditions suivantes:

{P1} S1 {P2}

{P2} S2 {P3}

La regle d’inference pour une telle sequence est:

{P1} S1 {P2}, {P2} S2 {P3}

{P1} S1 ; S2 {P3}

Previous slide

Next slide

Back to first slide

View graphic version