Simulation des programmes impératifs

Simulation des programmes impératifs

Graphes d’exécution

Le but de ce chapitre est de prouver que les ASMs peuvent simuler les programmes impératifs, au sens de la définition 2.3.5 p.56. Je rappelle que dans le système de transition p.47 définissant la sémantique opérationnelle de nos programmes impératifs les états sont de la forme P ⋆X. Les deux systèmes utilisent les mêmes commandes de mise à jour, donc la simulation revient en grande partie à simuler la partie « programme » de P ⋆ X.

Notre but est donc de construire à partir de P un programme d’ASM ΠP (voir la traduction 3.2.1 p.65) contenant non seulement les mêmes mises à jour, mais aussi capable de déterminer où en est l’exécution de ΠP par rapport au programme impératif d’origine P. Lignes d’un programme

L’idée intuitive pour traduire un programme impératif en une ASM est de traduire séparément chaque commande, en ajoutant une sorte de pointeur d’instruction1 pour passer d’une commande à l’autre tout en respectant la sémantique opérationnelle Remarque. Le numéro d’une ligne est la longueur du programme (voir p.127) avant la commande actuelle, donc les numéros de ligne sont tous entre 0 et length(P), et line = length(P) est la fin du programme.

Comme le nombre de valeurs est borné, à la place d’un compteur d’instruction dont la valeur va changer, un nombre fini de boo léens b0,b1,…blength(P) peuvent être utilisés. Cette approche a été suggérée dans [GV12], et est adaptée pour un langage de pro grammation basé sur des numéros de ligne (par exemple utilisant des commandes goto) mais pas pour un langage de programmation structuré comme Imp.

En effet, le numéro de ligne peut faire la distinction entre deux commandes qui sont pourtant identiques du point de vue de la sémantique opérationnelle : Exemple 3.1.2. Nous distinguons à la table 3.2 p.61 les commandes x := x+1 et x := x+1 par un marquage extérieur. Du point de vue de la sémantique opérationnelle ces commandes sont identiques. Ainsi, les programmes P2 et P4 ne sont distingués que par le marquage alors que leur opérationnalité est la même :

nous aurions pu remplacer P2 par P4 sans changer la suite de l’exécution. Toutefois en affirmant que x := x+1 et x := x+1 sont des lignes différentes du programme, c’est bien une telle distinction que nous sommes en train de faire, qui n’a donc aucun fondement du point de vue de la sémantique opérationnelle. De même que pour les boucles, cette distinction sans fondement concerne également les conditionnelles (voir la table 3.3 p.61)

Ainsi, une traduction basée sur les numéros de ligne pourrait être définie, mais pour être distinguées les commandes devraient être marquées par leur profondeur (pour des boucles imbriquées) et le chemin de conditionnelles fait pour les atteindre. En plus d’être pénible cette approche serait inutile car ces commandes seraient de toute façon identiques pour la sémantique opérationnelle.