Simulation des ASMs

Simulation des ASMs

Le but de ce chapitre est de montrer que les programmes impératifs peuvent simuler les ASMs au sens de la définition 2.3.5 p.56. Pour cela nous devons procéder par étapes : 1. Un programme d’ASM Π décrit comment faire une étape de l’algorithme. Ainsi, dans la première section nous présenterons une traduction fidèle de Π en temps que programme impératif capable de simuler une étape de l’ASM : c’est le programme noyau1 PΠ.

2. Pour simuler fidèlement toute une exécution de l’ASM, il faut répéter le programme noyau suffisamment de fois. Pour cela, dans la seconde section, nous utiliserons la complexité cΠ de l’algorithme afin de construire un programme durant assez longtemps : c’est le programme coquille PcΠ .

3. Nous expliquerons ensuite comment « mélanger » le programme noyau PΠ et le programme coquille PcΠ pour obtenir le programme final à la troisième section, et prouverons que les conditions de notre simulation raisonnable sont vérifiées. 4.1 Le programme noyau Soit Π le programme d’ASM à simuler. Le but de cette section est de construire le programme noyau PΠ dont l’exécution pourra simuler correctement une étape de Π

Traduction syntaxique

Dans la mesure où ASM et Imp ont les mêmes commandes pour les mises à jour et les conditionnelles, il est tentant de simplement traduire les programmes d’ASM de cette façon : Définition 4.1.1. (Traduction commande par commande des ASMs) (ft1 …tk := t0)tr =def {ft1 …tk := t0;} (if F then Π1 else Π2 endif)tr =def {if F then Πtr 1 else Πtr 2 ;} (par Π1∥…∥Πn endpar)tr =def Πtr 1 … Πtr n La traduction des commandes par Π1∥…∥Πn

endpar est une composition (voir p.48) de programmes Πtr 1 … Πtr n. Le problème est que pour les ASMs les commandes sont effectuées simultanément, alors que pour les programmes impératifs elles sont effectuées séquentiellement. Ainsi la traduction commande par commande n’est pas fidèle : Exemple 4.1.2. (Traduction non fidèle

Le programme simulant un pas

Il reste cependant deux problèmes : 1. Les variables vt1 ,…,vtr ne sont pas encore initialisées aux valeurs de {t1,…,tr} = Read(Π). 2. Selon la définition 2.3.5 p.56 la dilatation temporelle devrait être constante ce qui nécessiterait que le PΠ désiré fasse le même nombre d’étapes quel que soit l’état considéré.

Le premier problème se pose réellement car comme suggéré à la p.54 les variables temporaires ne devraient pas être initialisées avec des informations portant sur le calcul en cours, typiquement le résultat. En fait nous nous sommes restreints ou bien à des initialisations uniformes (par exemple pour la traduction p.65 bP est vraie et les autres bPj sont faux dans l’état initial) ou bien à la taille des entrées (cas que nous aborderons à la section suivante).

Ainsi, pour régler le premier problème, nous ne donnerons pas de valeur particulière aux vt à l’initialisation mais nous ferons une initialisation explicite en ajoutant le pro gramme ⃗vt := ⃗ t avant le programme Π[⃗vt/⃗ t]tr. Remarque. Dans le programme PΠ désiré les variables ⃗vt ne sont mises à jour que durant l’initialisation, donc elles contiennent la valeur initiale des ⃗ t : vtPΠ(X) = tX