Semantique Axiomatique III
Plus precisement, la verification de programmes se fait en deux etapes:
- l’association d’une formule avec chaque etape du calcul significatif.
- La demonstration que la formule finale s’ensuit logiquement de la formule initiale grace aux etapes et formules intermediaires.
Les formules pour l’affectement et les conditions sont les formules de base. L’effet de toutes les autres instructions en decoulent logiquement.