Specification de la Semantique Dynamique (ou, simplement, Semantique)
Il y a trois methodes de specification semantique:
- Description Operationnelle: la signification d’un programme est determinee par l’execution de ses enonces sur une machine virtuelle.
- Description Denotationelle: la signification d’un programme est decrite a l’aide de fonctions montrant l’effet de l’application d’un enonce sur l’etat de la machine.
- Description Axiomatique: la signification d’un programme est decrite a l’aide d’assertions specifiant les contraintes et relations qu’imposent un enonce.