Semantique Axiomatique IV: l’Affectement

Supposons que x = E soit une instruction d’affectement et que Q soit sa postcondition. Alors, sa precondition est definie par l’axiome P = Q x --> E qui signifie que P est calcule comme Q avec toutes les instances de x remplacees par E.

Comment peut-on prouver l’exactitude de programmes (et en particulier d’une instruction d’affectement) avec de tels outils?

Supposons que x = E soit une instruction d’affectement et que Q soit sa postcondition. Alors, sa precondition est definie par l’axiome P = Q x --> E qui signifie que P est calcule comme Q avec toutes les instances de x remplacees par E.