Semantique Axiomatique V: Justification de la procedure
Une instruction d’affectement avec sa precondition et sa postcondition peuvent etre consideres comme des theoremes.
Si l’axiome d’affectement, lorsqu’applique a la postcondition et a l’instruction d’affectement, produit la precondition donnee, alors on peut dire que le theoreme est prouve, et donc, le programme est exact ou correcte.