• conçue dans le même esprit que la sémantique fonctionnelle mais en utilisant une relation ternaire ;
• chaque instruction est vue comme une transformation entre – un état initial (avant l'exécution de l'instruction) ; – un état final (après l'exécution).

• Encore une relation inductive pilotée par l'instruction à exécuter.
• Mais ici, on décrit une relation entre l'état courant et l'état suivant après exécution d'une étape élémentaire dite aussi petit pas par ex. une affectation) de l'instruction courante.
• À l'issue d'un petit pas, on aboutit à une nouvelle configuration composée : – du nouvel état – du reste du programme à exécuter ; ce dernier est représenté par un AST, amis on peut le penser comme un compteur ordinal (program counter).
• Autrement dit, une transition (petit pas) transforme une configuration en une nouvelle configuration.
• L'exécution complète d'un programme consiste à répéter des petits pas (fermeture transitive de SOS₁)
• On a ainsi accès à l'état mémoire obtenu après 1, 2,… n petits pas.

Deux possibilités en fait :

• configuration intermédiaire Inter = "en cours de calcul"
• configuration Final "calcul terminé"

Pas de calcul partant de Final, pas même de petit pas. Petit pas : état -> AST -> configuration

coq_chap_08_SOS.v

P1 = "while not (i=0) do {i := i-1; x := 1+x}".