Semantique Axiomatique II
La pre-condition la plus faible represente la pre-condition la moins restrictive qui garantie la validite de la post-condition associee a l’instruction du programme.
Si la pre-condition la plus faible peut etre calculee a partir de la post-condition definie pour chaque instruction du language, preuves de validite peuvent etre construites pour les programmes de ce language.
Les preuves sont construites en partant de la fin d’un programme et en remontant vers son debut.
La semantique axiomatique n’est pas tres utile pour decrire la signification des languages de programmation a cause de sa comlexite. Neanmoins, elle est utile pour la recherche et pour le raisonnement sur les programmes.