Semantique Axiomatique VI: la Regle de Consequence (retrecissement ou elargissement)

• Parfois, la pre-condition obtenue par la procedure ne correspond pas a la pre-condition attendue.

• Dans ce cas, on peut se servir de la regle de consequence qui est la regle d’inference suivante:

{P} S {Q}, P’ => P, Q => Q’

{P’} S {Q’}

Previous slide

Next slide

Back to first slide

View graphic version