Sémantique opérationnelle à grands pas

Approche naïve

Essayez tout d'abord de compléter la théorie suivante, qui tente naïvement de définir la sémantique opérationnelle de Niklaus à l'aide d'une fonction.

Utilisation d'un prédicat inductif

Exercice

Corrigé

Propriétés de la sémantique (et du langage)

Il est possible de définir la notion d'instructions équivalentes, qui peut être utile par exemple pour prouver la correction d'un optimiseur de code.

On démontre également que le langage Niklaus est déterministe : lorsqu'on exécute une instruction à partir d'un état de la machine, on arrive toujours dans un seul état.

Sémantique à petits pas

Pour ceux qui sont intéressés, voici une version à petits pas de la sémantique opérationnelle de Niklaus, qui ne sera pas abordée en cours.