Semantique Axiomatique I
La semantique axiomatique est definie en conjonction avec une methode de preuve de validite de programmes.
Lorsque le programme est correct, il existe une preuve de validite et dans cette preuve, chaque proposition est precedee et suivie d’une expression logique (pre-condition et post-condition) qui specifie des contraintes sur les variables du programme. Ce sont ces contraintes qui definissent la signification du programme.