RIA
laboria

Institut de Recherche
d'Informatique
et d'Automatique

Domaine de Voluceau
Rocquencourt
B. P. 105 78150 - Le Chesnay
France
Tél.: 954 90 20

laboratoire de recherche
en informatique
et automatique

TECHNIQUE
DE PREUVE PAR ATTRIBUTS
APPLIQUÉE À UN
COMPILATEUR LISP

Pierre DERANSART

Rapport de Recherche N° 271

Janvier 1978
TECHNIQUE DE PREUVE PAR ATTRIBUTS
APPLIQUÉ A UN COMPILATEUR LISP

Pierre Deransart

Résumé :

Ce rapport montre comment on peut utiliser la technique de preuve par attributs afin de prouver la
correction d'un compilateur défini par attributs sémantiques. Le langage choisi est un sous-ensem-
ble compilable de Lisp. Deux définitions en sont fournies : l'une à partir d'un interpréteur, l'autre
constituée par l'implantation dans une machine abstraite. La première est en quelque sorte la réfé-
rence et l'on veut prouver que la traduction dans la machine abstraite est équivalente à la première
définition.

Un des intérêts de cette technique réside dans une décomposition de la preuve, guidée par les défi-
nitions d'attributs.

Abstract :

This report illustrates how to use the attributes-proof-techniques to prove the correctness of a
compiler defined by semantic attributes. The language is a compilable subset of Lisp. Two defini-
tions are proposed : one by interpreter, the other by implementation in terms of an abstract ma-
chine. The first is considered as the reference, and we want to prove that the second is equivalent.
One of the interest of this technique is the modularity of the proof directed by the attribute
definitions.

<footnote>* Mots clés : compilateur, Lisp, attributs sémantiques, preuve de compilateurs, système d’écriture de traducteurs.</footnote>

<footnote>* Keywords : compiler, translator unitting system, semantic attributes, Lisp, interpreter, proof of compiler.</footnote>
TECHNIQUE DE PREUVE PAR ATTRIBUTS

APPLIQUEE A UN COMPILATEUR LISP

# 1. Introduction

La description d'un compilateur par la méthode des attributs est une
technique déjà bien connue [Knuth 71, Lorho 74, Simonet 75, Rochman 76,
Boroviecs 75]. Moins connues sont les possibilités offertes par cette
technique pour établir la preuve d'un compilateur défini par attributs.
Il s'agit d'utiliser la récursivité de la description dirigée par la syntaxe
et la modularité d'une telle définition pour l'établir. La méthode a été
décrite dans [Pair 76].

L'application d'une telle méthode à un compilateur Lisp est due pour une
part à la simplicité du langage et pour une autre au fait que la sémantique
du langage peut être décrite par un interpréteur. La preuve consiste alors
à montrer l'identité du résultat de l'exécution du code généré et du résultat
obtenu en interprétant le texte original.

Le Lisp choisi est un sous-ensemble de Lisp 1.5 [Mc. Carthy 62] défini
dans [Deransart 77.b]. Ce rapport présente donc le langage source et
l'interpréteur associé, puis sa traduction dans un langage objet correspon-
dans à une machine abstraite inspirée de [Lux 75]. Celle-ci permet une
description de l'implantation extrêmement simple et reste proche d'implan-
tation réalisées sur IBM 360 [Hearn] ou DEC systèmes [Maclisp]. Ce rapport
présente enfin la preuve de la traduction qui constitue également une
vérification de l'exactitude de la traduction par attributs.

Une connaissance minimale de Lisp et de la méthode des attributs
sémantiques est requise pour une bonne compréhension de ce rapport.
## 2. Principe de la preuve

La preuve repose sur le fait que l'on dispose de deux définitions du langage.

D'une part, la sémantique (opérationnelle) d'un programme Lisp P est définie par un interprète ($S$) qui, prenant un programme comme paramètre, est une fonction d'états qui modifie un environnement (aliste si le programme est une forme, aliste et liste d'arguments si c'est une fonction). Ceci est illustré par le schéma suivant :

<figure><img src="image_1.png" /></figure>

où les états $S$ peuvent être décrits en termes de structures formelles (aliste, valeurs ...).

D'autre part le compilateur est une autre définition qui consiste à indiquer l'équivalent d'un programme P dans le langage d'une machine définie formellement : la machine abstraite (MA). La description de la MA peut se faire en terme de changement d'états :

<figure><img src="image_2.png" /></figure>

On définit également une fonction d'implantation des états $S$ dans la MA : $S' = I(S)$.

La preuve consiste alors à prouver la commutativité du schéma suivant :

<figure><img src="image_3.png" /></figure>

Soit : $\forall S C(P) (I(S)) = I(S(P)(S))$

C'est ce que nous établirons en écrivant la sémantique du langage de la MA avec des notations inspirées de Hoare :

$$S'_{D} = I(S_{D}) \{C(P)\} S'_{A} = I(S(P) (S_{D}))$$

Une fonction Lisp se présente pour nous sous la forme d'un texte qui, du point de vue de son analyse syntaxique, est un mot terminal de la grammaire fournie en Annexe 1-A, d'axiome <Prog>. Du point de vue de
de l'interpréteur, un tel programme est aussi une S-expression (1),
c'est-à-dire une liste, elle-même combinaison de listes et d'atomes. Ce
programme est le premier argument fourni à l'interpréteur, noté "function"
(cf. Annexe 1-B-b).

Ce double point de vue nous permet d'établir les deux descriptions du
langage : nous qualifierons l'une de fonctionnelle, l'autre de traductive.

Dans le premier cas (fig. 1) trois arguments sont fournis à l'inter-
préteur : la fonction, ses arguments et le contexte. La fonction est une
S-expression, les arguments sont réunis en une liste d'arguments déjà
évalués et le contexte constitue

<figure><img src="image_4.png" /><figcaption>Fig. 1 : définition fonctionnelle de Lisp.</figcaption></figure>

l'environnement (variables et procédures), appelé "aliste", dans lequel
cette fonction doit être évaluée. "apply" produit un résultat qui est
lui-même une S-expression et provoque un nouveau contexte qui peut être
décrit à l'aide d'une autre fonction : transply.

Dans le second cas (fig. 2), on décrit une implantation dans une
machine décrite formellement, appelée machine abstraite (MA).

<S-expr> ::= Ident | (<Contenu de liste>) | (<Paire>)
<Contenu de liste> ::= <S-expr> <Contenu de liste> | empty
<Paire> ::= <S-expr>.<S-expr>

<footnote>(1) La syntaxe des S-expressions est la suivante : (terminal S-expr de la grammaire)</footnote>
<figure><img src="image_5.png" /><figcaption>Fig. 2 : définition traductive de Lisp.</figcaption></figure>

D'une part on décrit donc la machine abstraite par ses instructions élémentaires et les changements d'états qu'elles provoquent, d'autre part on décrit le compilateur du langage (fonction "compile" de fig. 2) ainsi que des implantations des arguments et du contexte (fonctions *I* et *A*).

La preuve consiste alors à prouver la commutativité du schéma de la figure 3. On sait en effet que compilateur et interpréteur analysent le même objet ("fonction") et que les résultats de l'interprétation et de l'activation de la MA doivent coïncider, au sens de l'implémentation (fonction *I* et *A*).
<figure><img src="image_6.png" /><figcaption>Fig. 3 - Schéma de la preuve.</figcaption></figure>

### 3. Description fonctionnelle.

Traditionnellement le contexte est représenté par une "aliste" qui est une liste de doublets "variable, valeur". Ceci revient à définir la aliste par son implantation. La définition fournie à l'Annexe 1-B (structure "alist") ne suppose rien quant à l'implantation et est suffisante pour décrire complètement l'interpréteur. Ainsi, l'objet aliste est formé d'atomes, de valeurs (S-expressions) et d'accès indiquant la liaison d'une variable à sa valeur (pair), la suppression d'une liaison (supp), la modification d'une liaison (affect, qui est une composition des deux précédentes) et la valeur associée à une variable liée (assoc). Un ensemble d'axiomes précise la structure de la aliste. Ainsi par exemple : les axiomes

$$ 
\begin{align*}
\text{assoc}(x, \text{pair}(x,v,a)) &= v \\
\text{assoc}(x, \text{pair}(y,v,a,)) &= \text{assoc}(x,a) \text{ pair } x \neq y \\
\text{assoc}(x, \text{emptalist}) &= \text{novalue}
\end{align*}
$$

indiquent que si x est lié dans la "aliste" sa valeur associée est celle de sa dernière liaison, et "novalue" si x n'est pas lié.
Les autres objets sont les atomes et les valeurs (union des atomes et des cellules). Les accès liant les atomes, cellules et valeurs sont les accès correspondant aux fonctions de base de Lisp et deux accès particuliers définissant les valeurs "nil" et "true" (nil et t).

La structure de l'atome est décrite par une série d'accès modifiables dont la plupart sont habituels en Lisp (apval, expr, subr, fsubr...). Nous avons ajouté deux accès "subrc" et "fsubrc" qui correspondent aux fonctions qui s'exécutent avec un seul argument consituté de la liste des arguments évalués. Notons que les accès "subr." correspondent à des fonctions définies compilées. Il peut paraître surprenant d'introduire à ce niveau des fonctions compilées (type "progadr"), mais ceci permet de réduire la description de l'interpréteur à ses aspects les plus intéressants. On suppose bien sûr que les fonctions compilées sont correctes.

Ces accès sont illustrés par la figure 4.

<figure><img src="image_7.png" /><figcaption>Fig. 4 - Structure de l'atome</figcaption></figure>

Les accès situés sur la même flêche sont exclusifs, c'est-à-dire qu'une fonction peut être expr ou fexpr, par contre elle peut être expr et subr dans cette description. L'interpréteur (Annexe 1-B-b), dans ce dernier cas, choisira la forme compilée.
Les autres accès concernent l'interpréteur qui à une fonction, un
argument composé de la liste des arguments évalués et un contexte fait
correspondre une nouvelle valeur résultat et un nouveau contexte.

La sémantique de l'interpréteur écrit en simili Algol 68 est simple :
son écriture ne comporte que des accès de la structure, la conditionnelle
**if** then else fi habituelle, et de nouveaux accès à la structure du texte
"S-expression" rendant compte de l'analyse syntaxique effectuée dynamiquement
par l'interpréteur.

L'interprète (Annexe 1-B-b) et la grammaire (Annexe 1-A) sont construits
de manière à ce qu'à chaque règle corresponde un cas unique (2) de
l'Interprète donc un accès dans apply et eval [Deransart 77-b] mais non
réciproquement (3). Ainsi, à la règle :

`11 <Formna> = (COND<Listcond>)`

correspond le 6ème cas de "eval" (S-expression dont le CAR est atomique et égal à COND). En effet, le reste de la liste fournie en argument correspond au non terminal <Listcond>. Il suffit pour s'en assurer d'examiner l'accès "evcon" pour lequel les cas correspondent aux règles 24 et 25 de la grammaire.

L'accès "exec" (premier cas de apply et transply) mérite une remarque
en ce sens qu'il ne contribue pas à la définition sémantique, il symbolise
l'appel de fonction dans l'interpréteur. Toute fonction ayant une forme
EXPR avant d'être compilée (forme SUBR), c'est la sémantique de la première
forme qui est retenue et dans ce cas on a : exec(function, listvarg, alist) =
apply(EXPR(function),listvarg,alist) transply(function, listvarg,alist) =
transply(EXPR(function),listvarg,alist) par hypothèse et en admettant que
dans ce cas la forme EXPR(respectivement FEXPR, EXPRC, FEXPRC) existe
toujours et est la même.

<footnote>(2) Il peut y avoir un fait plusieurs cas mais ils découlent en fait d'un regroupement visant à abréger l'écriture de l'interpréteur.</footnote>

<footnote>(3) La réciproque serait seulement : si une fonction est interprétée avec certaines conditions (pas de double récursivité par exemple), sa S-expression est syntaxiquement correcte.</footnote>
### 4. Définition traductive.

La définition traductive comporte d'une part la définition de la
Machine Abstraite (MA), d'autre part la définition des fonctions compile,
I et A (Implémentation)

#### a) Définition de la MA.

La MA considérée comporte les éléments suivants (Figure 5) :

<figure><img src="image_8.png" /><figcaption>Fig. 5 - Machine Abstraite.</figcaption></figure>

- Une zone mémoire contenant des cellules en nombre potentiellement infini. Aucune implantation différente des accès élémentaires de la structure source ne sera envisagée ici.

- Une table des atomes, potentiellement non limitée, où chaque identificateur n'est représenté qu'une fois, mais où, du fait de la récursivité de Lisp, chaque atome va pointer (accès assoc) non sur une valeur mais sur une pile de valeurs, dite pile des valeurs associées. L'implantation ne diffère de la structure source que par l'introduction de deux accès supplémentaires "nom" et "recherche" (figure 6).
<figure><img src="image_9.png" /><figcaption>Fig. 6 : accès "nom" et "recherche" de la MA.</figcaption></figure>

Pour simplifier l'écriture de la preuve les accès "nom" et "recherche"
seront par la suite systématiquement omis.

- une zone de piles comportant autant de piles de valeurs associées (PVA) que d'atomes dans la table, une pile servant à stocker les arguments évalués et les résultats (PA), et une pile des adresses de retour,

- une zone de rangement des programmes à laquelle on accède par l'accès "progadr" identique à celui de la structure source,

- un compteur ordinal.

La description complète de la structure correspondant à cette MA
est donnée à l'Annexe 2.B avec les notations. Précisons seulement
l'implantation du contexte :

Define type bstack
    type x : platom, bstackelt, value
    accès (bstack) bstackelt : btop(x)
    accès (bstackelt) value : val
    accès (value) : novalue
    accès (value, bstack) bstack : pushb(x)
    accès (bstack) bstack : popb(x)
    accès (value, bstack) bstack : change(x)

L'objet de type "bstack" est défini à l'aide des types élémentaires
"platom" qui sera confondu avec "atom" dans la suite, "bstackelt" qui
représente un élément de liaison (autant de liaisons effectuées, autant
d'éléments de "bstack") et "value" qui est le même type que celui du
langage source (en confondant "atom" et "platom"). Ce type est paramétré
par le nom des atomes et possède donc autant de chaque accès nommé que
d'atomes.
Les axiomes de l'objet "bstack" sont semblables à ceux de la aliste.

Les instructions de la MA sont décrites à l'Annexe 2-C avec la
notation de Hoare [Hoare 69] où l'état initial de la MA est donné
les préconditions et l'état final résultant de l'effet d'une instruction
par les post-conditions.

Par exemple :

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
ic = a, & ic = a + 1, & \\
stack = b, & \{ \text{PUSHV } x \ i \} & stack = \text{push}(c(\text{top}-i), b), \\
bstack = d, & \text{val}(\text{btop}(x)(d)) = c(\text{top}) &
\end{array}
$$

L'instruction "PUSHV x i" provoque les modifications suivantes de
l'état de la MA :

- le compteur ordinal (ic) est incrémenté

- la pile des arguments (stack) est augmentée d'un élément dont le contenu est celui du i<sup>ième</sup> successeur du sommet (nouveau sommet),

- le contenu du sommet est la valeur associée à l'atome x dans le
contexte bstack. Cette dernière propriété n'est qu'une vérification du
fait que le i<sup>ième</sup> successeur du sommet contient bien la valeur associée à
x dans le contexte bstack.

Il est à noter que l'évolution de la pile (stack) peut s'écrire
également :

$$
\text{top} = e \quad \left\{ \text{PUSHV } x \ i \right\} \quad \begin{array}{l} \text{top} = e + 1, \\ c(\text{top}) = c(\text{top}-i) \end{array}
$$

La définition des instructions ne pose pas de problème particulier
sinon pour l'appel de fonction. Comme nous l'avons souligné nous sommes
obligés de supposer que la sémantique en est connue et que de plus - ceci
dans le cadre de l'axiomatique de Hoare - l'appel se termine. Il est
enfin nécessaire d'indiquer le mode de passage des paramètres dans la MA.

Toute fonction trouve, par définition, ses paramètres en sommet de
pile des arguments. Si une fonction a n paramètres, par hypothèse, nous
admettrons que ses n arguments sont bien en sommet de pile. Ceci pourrait
d'ailleurs être vérifié à la compilation.
Dans ce cas l'appel de l'instruction "LINK n f" est le suivant :

```
ic = a                      ic = a+1,
top = b                      top = b+1
list(c(b-n+1)...c(b)) =     c(top) =
                          I(lvg)      LINK n f      I(exec(f,lvg,a))
si f est SUBR ou FSUBR       bstack =
c(b) = I(lvg)                A(transply(f,lvg,a))
si f est SUBRC ou FSUBRC
```

Ce qui revient à supposer que pour une fonction compilée la preuve est faite. En effet, les pré et post-conditions expriment la commutativité du schéma de la figure 1.

Notons cependant que l'implantation de la liste des n arguments fournie à "apply" dans le cas d'une fonction SUBR ou FSUBR est identique (cf. infra la définition de I) à la liste constituée dans l'espace des valeurs de la MA avec les n éléments localisés en sommet de pile des arguments. Dans le cas des fonctions SUBRC et FSUBRC il n'y a qu'un argument en sommet de pile qui est précisément la liste des arguments évalués fournie à la fonction.

L'activation de la MA est extrêmement simple : l'instruction dont le numéro se trouve dans le compteur est exécutée et ainsi de suite tant qu'une instruction "stop" n'est pas rencontrée.

b) Définition de compile, I et A.

La définition du compilateur a été longuement détaillée dans [Deransart 77-b] et reproduite in extenso en Annexe 3 - A et B. Nous ne rappellerons ici que les grandes lignes du compilateur.

Le compilateur comporte différents groupes d'attributs :

- les attributs servant à la génération de code (CEVAL, POBOUND, PUBOUND). Ces définitions de ces attributs utilisent ce que l'on pourrait appeler une syntaxe abstraite du langage en ce sens que leur combinaison ne comporte que la composition et le saut. Il faut noter que le langage compilé ne comporte que des expressions (les formes "prog" ont été exclues puisqu'elles reviennent à traiter le cas de langages itératifs usuels sensiblement plus complexes à traiter).

- Les attributs de comptage des instructions (LAB, LAB1, LAB2) qui permettent de générer les sauts et, éventuellement, de générer dans le désordre les instructions.

- L'attribut TOP qui simule l'évolution de la pile des arguments.

- Les attributs NARG qui comptent les arguments d'une fonction.
- Les attributs NVAR qui comptent le nombre de variables d'une fonction (il doit normalement y en avoir autant que d'arguments).

- L'attribut TAB qui simule l'évolution de la aliste en indiquant les variables liées et la localisation dans la pile des arguments des valeurs de ces variables. Cette localisation est constante pour toute la durée de la liaison (portée de la variable dans le λ-expression où elle est définie). La preuve en est faite à l'Annexe 3-A-c (cas de H.TAB).

- L'attribut TEXT enfin qui reproduit le texte correspondant à un terminal de la grammaire.

La signification de ces attributs apparaît plus clairement si l'on se réfère au tableau de l'Annexe 3-A-b qui indique les non-terminaux auxquels sont définis les attributs. Ainsi l'attribut S.NARG est défini aux non-terminaux <listarg> et <listexpr> et relève donc le nombre d'arguments existants sous ces non-terminaux. Par contre l'attribut H.NARG est défini aux non-terminaux <function> et <F-function> et sert à transmettre le nombre d'arguments de la fonction définie sous ces non-terminaux.

La traduction proprement dite est donnée à l'Annexe 3-B (règles R1 à R33) pour chaque règle de la grammaire.

Les définitions de *I* et *A* sont données récursivement pour chaque accès de la structure source (Annexe 2-D). La fonction d'implémentation *I* est définie comme "pratiquement" une identité puisque l'espace des valeurs est formellement le même dans les deux représentations. *I* est donc une application des valeurs dans les valeurs. Ceci est obtenu au prix de deux abus :

- confusion déjà signalée entre atomes et places d'atomes dans la structure de la MA.

- L'implémentation d'une liste de n arguments est l'implémentation de chacun des arguments en sommet de pile des arguments, sachant que le plus à gauche de la liste est le plus profond dans la pile. Ceci est résumé par la notation :

$$I((a_1... a_n)) = \text{list } (c(top-n+1)..c(top))$$

où $c(top-n+i) = I(a_i)$ est implicite.

La définition de *A* s'écrit par exemple :

$$A(pair(x : atom, v : value, α : alist)) = \text{pushb}(x)(I(v), A(α))$$
qui signifie que l'implémentation de l'ajout d'une liaison à la aliste se traduit par l'accès pushb du même atome x avec pour arguments l'implantation de la valeur (identité) et l'implémentation de la aliste initiale.

## 5. Mise en place de la preuve.

La commutativité du schéma de la figure 3 s'exprime par une propriété du code généré qui est : pour toute fonction définie par la règle :

$$ \langle \text{Prog} \rangle = (\text{LAMBDA}(\langle \text{Listvar} \rangle) \langle \text{Form} \rangle) $$

```
ic = 1,
list(c(1-na)..c(o)) = I(la),
stack = b,
bstack = A(a)
ic = cr(returntop),
stack=push(I(apply(prog,la,a),b),
{CEVAL(Prog)})
bstack=A(transply(prog,la,a))
```

et pour toute fonction définie par la règle :

$$ \text{Prog} = (\text{LAMBDA} \ \text{Ident} \ \text{Form}) $$

```
ic = 1,
c(top) = I(la),
top = b,
bstack = A(a)
ic = cr(returntop),
c(top) = I(apply(prog,la,a)),
top = b + 1,
bstack = A(transply(prog,la,a))
```

en supposant la terminaison du programme généré.

Ces deux assertions expriment d'une part qu'une fonction trouvant ses n arguments en sommet de pile des arguments met son résultat en sommet de pile et que l'exécution du code généré produit le même résultat que l'interprétation du texte source de cette fonction.

La technique de preuve par attributs, décrite dans [Pair 76], consiste à traduire les propriétés que l'on veut démontrer par des assertions liant les attributs d'un même symbole non-terminal de la grammaire, puis à associer à chaque assertion l'un des attributs du symbole non-terminal considéré. La base de la preuve est un raisonnement par récurrence, l'ordre de récurrence étant l'ordre d'évaluation des attributs ainsi associés.

Dans le cas présent la preuve est simplifiée par le fait que la propriété à démontrer est quasi unique et attachée à l'attribut de génération de code qui est synthétisé. La preuve synthétisée qui en découle se fait donc de la manière suivante :
- établir les assertions à démontrer pour chaque non-terminal où sont définis les attributs de génération de code (CEVAL, PUBOUND, POBOUND),

- en admettant comme hypothèse les assertions associées aux attributs définis aux non-terminaux du membre droit d'une règle, prouver l'assertion associée au non-terminal de gauche de la règle et ceci pour toutes les règles de la grammaire.

La liste des assertions pour chaque non-terminal où l'attribut code est défini est donnée à l'Annexe 4-A et comporte 11 assertions du type des deux ci-dessus.

Les règles de déduction utilisées pour la preuve reposent sur les règles de l'axiomatique de Hoare, adaptées pour la circonstance. La règle concernant le saut est décrite avec les instructions BR et BRN, qui ne modifient que le compteur ordinal. Elles conservent toutes les autres propriétés :

$$ \mathit{co} = a, P \{\mathit{go} \ \mathit{to} \ \mathit{lab}\} \ \mathit{co} = \mathit{lab}, P $$

La règle principale de déduction s'exprime de la manière suivante :
(composition) :

$$ \begin{array}{l} P1 \{S1\} Q1, P2 \{S2\} Q2, P \supset P1, Q1 \supset P2, Q2 \supset Q \\ \\ P \{S1; S2\} Q \end{array} $$

La propriété à démontrer concerne une séquence de code (S1 et S2), la preuve consiste alors à montrer que connaissant P, on a P1 (P>P2), que Q1>P2 (en général il suffit d'identifier Q1=P2) et que la post-condition finale implique la post-condition recherchée.

Cette procédure s'itère, et, comme en général les implications sont des identités, la forme générale de la preuve est la suivante :

$$ \begin{array}{l} P1 \{S1\} Q1, P2 \{S2\} Q2, P3 \{S3\} Q3 \\ \\ P \{S1; S2; S3\} Q \end{array} $$

Preuve :

$$ P = P_1 $$

$$ Q_1 = P_2 $$

$$ Q_2 = P_3 $$

$$ Q_3 = Q \qquad \mathbf{CQFD} $$
La preuve consiste donc, pour chaque règle à vérifier de proche
en proche l'égalité des prédicats en utilisant les identités des
définitions d'attributs (les affectations peuvent être utilisées en
fait dans un sens ou dans l'autre).

6. Un exemple de preuve.

La preuve complète est fournie à l'Annexe 4-C pour chaque règle R1 à
R33. Pour chaque règle on indique :

- la définition du code (composition) : définition S1.

- la suite des états (pré et post-conditions) pour chaque instruction en groupe d'instructions et leur unification avec les hypothèses ou les définitions utilisées pour les réaliser.

A titre d'explication nous donnons ici un exemple commenté :
R14 <Formna> = (<Function> <Listarg>)

S1 S.CEVAL (Formna) := S.CEVAL (Listarg)
S.CEVAL (Function)

S.LAB(Function : POP S.NARG(Listarg) ;

donc composition de 3 éléments de code.

Les autres définitions d'attributs sont (cf. Annexe 3-B, R14) :

S2 H.LAB(Listarg) := H.LAB(Formna)
S3 H.LAB(Function) := S.LAB(Listarg)
S4 S.LAB(Formna) := S.LAB(Function) + 1

S5 H.TOP(Listarg) := H.TOP(Formna)
S6 H.TOP(Function) := H.TOP(Formna) + S.NARG(Listarg)

S7 H.TAB(Function) := H.TAB(Formna)
S8 H.TAB(Listarg) := H.TAB(Formna)
S9 H.NARG(Function) := S.NARG(Listarg)

La pré-condition de départ est donnée par l'assertion A2 :

ic = H.LAB(Formna),                      ic = S.LAB(Formna),
stack = b,                               {CEVAL(Formna)} stack = push(I.eval(formna,α),b),
bstack = A(α)                             bstack = A(transval(formna,α))

On a donc :

P = ic = H.LAB(Formna),
top = H.TOP(Formna),
bstack = A(α)
immédiatement identifié avec P1 de l'assertion A3 appliquée au non terminal <listarg>

P1 ≡ ic = H.LAB(Listarg) = H.LAB(Formna) (S2)

top = H.TOP(Listarg) = H.TOP(Formna) (S5)

bstack = A(α) (identité)

Q1 découle de l'assertion A4 :

Q1 ≡ ic = S.LAB(Listarg), top = H.TOP(Listarg) + S.NARG(Listarg)

list(c(H.TOP(Listarg)+1)..c(H.TOP(Listarg)+S.NARG(Listarg)))/I(evlis(listarg,α))

bstack = A(translis(listarg,α))

P2 est la pré-condition de A1 appliquée au non-terminal <Function>

P2 ≡ ic = H.LAB(Function) = S.LAB(Listarg) (S3), top = H.TOP(Function)

list(c(H.TOP(Function-H.NARG(Function)+1)..c(H.TOP(Function)))/I(la)

bstack = A(translis(listarg,α)) (identité)

Sachant que H.TOP(Function) = H.TOP(Formna) + H.NARG(Function) (S6), (S7) et que H.TOP(Listarg) = H.TOP(Formna) (S5), l'identification du membre gauche est immédiate ; celle du membre droit également avec la = evlis(listarg,α)

Q2 découle de A1 appliquée à <Function> :

Q2 ≡ ic = S.LAB(Function)

top = H.TOP(Function) + 1

c(top) = I(apply(function, evlis(listarg,α), translis(listarg,α)))

bstack = A(transply(function, evlis(listarg,α), translis(listarg,α)))

Il reste à exécuter l'instruction POP S.NARG(Listarg) en identifiant
aparavant sa pré-condition avec Q2 (Arbre 2-c)

P3 ≡ ic = S.LAB(Function)

top = H.TOP(Function) + 1 (unification de a et b)

D'où l'état après exécution :

Q3 ≡ ic = S.LAB(Function) + 1

top = H.TOP(Function) + 1

c(top) = c(H.TOP(Function) + 1) = I(apply(..)) (selon Q2 et P3)

bstack = A(transply(...))

Il reste à identifier Q3 avec Q, c'est-à-dire :

Q ≡ ic = S.LAB(Formna)

top = H.TOP(Formna) + 1

c(top) = I.eval(formna,α)

bstack = A(transval(formna,α))
ici est identifié par S4, top par S6. Pour c(top) et bstack, il est nécessaire de rechercher à quels cas dans eval et transval correspond la règle 14 (<Function>) correspond soit à une fonction atomique SUBR, soit à une LAMBDA expression - règles 18 et 19) et dans les deux cas on a :

`eval(formna,α) = apply(car(formna),evlis(cdr(formna),α), translis(cdr(formna),α))`

et idem pour transval.

où car et cdr sont des accès aux éléments du texte qui répond à la syntaxe de la règle 14. On peut donc unifier puisque l'on a, par définition :

```
car(formna) = function
et cdr(formna) = listarg
```

## 7. Conclusion.

Nous avons montré ainsi la correction du compilateur décrit par attributs, c'est-à-dire que l'exécution du code généré d'une fonction produit le même résultat que l'interpréteur et que ce résultat est cohérent avec le fonctionnement de la machine abstraite.

La méthode utilisée, la preuve synthétisée, est une technique assez générale dans la mesure où une telle preuve peut se ramener à une propriété liée à un seul attribut synthétisé (ici le code généré). Dans le cas contraire, il faudrait établir des preuves concernant d'autres propriétés liées à des attributs ayant un sens quelconque de circulation. L'attribut "code généré" jouant cependant un rôle privilégié lorsque l'on définit un compilateur, il semble naturel de considérer que la propriété qui peut lui être associée soit l'une des propriétés essentielles à vérifier. Or la méthode pratique de preuve mise en oeuvre, s'appuyant sur la représentation développée dans l'axiomatique de Hoare, laisse apparaître une possibilité d'automatisation, au moins partielle de celle-ci.

On peut de plus se demander si le processus de preuve n'est pas réversible ; à savoir s'il n'est pas possible de déduire les définitions d'attributs de la seule définition des propriétés à prouver. La résolution de ce problème aboutirait à synthétiser le traducteur (par attributs) d'un langage dont seuls seraient connus la syntaxe, les propriétés à vérifier aux non-terminaux, les attributs et sens de variation, l'axiomatice du domaine de calcul des attributs et la définition du code généré et de certaines définitions d'attributs.
## Remerciements.

Je tiens à remercier MM PAIR, CUTTAG et Mme GAUDEL pour les
fructueuses discussions qui ont conduit à la mise en forme de cette
preuve.

## BIBLIOGRAPHIE.

G.V. BOCHMANN, M. MARCOTTY, H.F. LEDGARD.

A Sampler of Formal Definitions. Computing Survey, Vol 8, N° 2,
Juin 1976.

J. BOROWIEC.

Pragmatics in a compiler producing system - MERA - Warsaw - July 1975.
Communication.

P. DERANSART.

a. Définition par attributs sémantiques de Lisp pur et preuve de
l'équivalence de la définition traductive et de l'évaluateur.
Rapport Laboria n° 220. Février 1977.

b. Définition et implantation de Lisp à l'aide d'un compilateur décrit
par la méthode des attributs sémantiques. Rapport Laboria n° 224.
Mars 1977.

c. Définition and implementation of a Lisp System using semantic
attributes. Colloque III. May 16.19.1977. Guidel (France).

A.C. HEARN.

Compilateur Lisp IBM 360.

C.A.R. HOARE.

An axiomatic basis for computer programming CACM vol 12, n° 10
p. 576)581. 1969.

D.E. KNUTH Semantics of context free languages

a. Math. Systems Theory V2, N2 p. 127-145. 1968

b. Math. Systems Theory V5, N1, p. 95-96. 1971.

B. LORHO.

De la définition à la traduction des langages de programmation :
méthode des attributs sémantiques. Thèses n° 637. Faculté Paul Sabatier
de Toulouse. 29 Nov. 1974.

R.L. LONDON.

Correctness of two compilers for a Lisp Subset. CSP report n° CS240
Stanford University, October 1971.

A. LUX.

Etude d'un modèle abstrait pour une machine Lisp et de son implémenta-
tion. Thèse. Université Scientifique et Médicale de Grenoble,
19 mars 1975.

MACLISP.

référence manuel. 17 Décembre 1975.

J.MC. CARTHY & al.

LISP 1.5 Programmer Manual, The MIT Press, Cambridge Mass. 1962.

C. PAIR, M. AMIRCHAHY, D. NEEL,

Preuve de descriptions de traitement de textes par attributs.

IRIA-Laboria. Avril 1976.

M. SIMONET, P.Y. CUNIN, J. VOIRON.

Méthodologie d'écriture de compilateur. Thèse de l'Université
Scientifique et Médicale de Grenoble. 22 avril 1976.
## Table

### A1 Langage Source (structures),

A - Syntaxe

B - Sémantique

a - Structure des données (cellules et aliste)

b - Interprète (apply, transply)

### A2 Langage Objet (structures),

A - Machine abstraite

B - Structure de la machine abstraite

C - Code objet et exemples

D - Fonctions *I* et *A* (représentation des structures sources)

### A3 Traduction (compile)

A - Définition des attributs

a) Nom, type et signification

b) Nom-terminaux auxquels ils sont définis

c) Cas de *H.TAB*

B - Traduction

### A4 Preuve

A - Assertions aux non-terminaux

B - Organisation de la preuve

C - Preuve par règles.
# ANNEXE 1.

## Langage Source

### A - Syntaxe : (Forme BNF simplifiée)

1. `<Prog>` = (LAMBDA (<Listvar>) <Form>)

2. = (LAMBDA Ident <Form>)

3. `<Listvar>` = <Listvar> Ident

4. = empty

5. `<Form>` = number

6. = ( )

7. = Constant

8. = Ident

9. = <Formna>

10. `<Formna>` = (QUOTE Sexpr)

11. = (COND <Listcond>)

12. = (SETQ Ident <Form>)

13. = (NEXTL Ident)

14. = (<Function> <Listarg>)

15. = (<Functionc> <Listargc>)

16. = (<F-Function> <Listexpr>)

17. = (<F-Functionc> <Listexprc>)

18. `<Function>` = (LAMBDA (<Listvar>) <Form>)

19. = Subr

20. `<Functionc>` = (LAMBDA Ident <Form>)

21. = Subrc

22. `<F-Function>` = F-Subr

23. `<F-Functionc>` = F.Subrc

24. `<Listcond>` = (<Form> <Form>) <Listcond>

25. = empty

26. `<Listarg>` = <Listarg> <Form>

27. = empty

28. `<Listexpr>` = <Listexpr> S-expr

29. = empty

30. `<Listargc>` = <Form> <Listargc>

31. = empty

32. `<Listexprc>` = S-expr <Listexprc>

33. = empty
# B - Sémantique

## a. Structure des données (cellules et aliste)

### Schéma de la structure d'un atome :

<figure><img src="image_10.png" /></figure>

<table><tr><td>valeur d'une</td><td>fonction associée</td><td>adresse du</td><td>accès à l'élément</td></tr><tr><td>constante</td><td>(λ - expression ou<br/>nom de fonction)</td><td>programme<br/>correspondant</td><td>de la aliste<br/>contenant la</td></tr><tr><td></td><td></td><td>(fonction compilée)</td><td>valeur associée.</td></tr></table>

### Définition de la structure "alist" :

**Define type alist**

**type** atom, value

**accès** alist : emptalist

**accès** value : novalue

**accès** (atom, value, alist) alist : pair

**accès** (atom, alist) alist : supp

**accès** (atom, value, alist) alist : affect

**accès** (atom, alist) value : assoc

### Axiomes définissant la structure "alist" : (quantificateur implicite)

* supp (x, emptalist) = emptalist

* supp (x, pair (x, v, a)) = a

* supp (x, pair (y, v, a)) = pair (y, v, supp (x, a)) x ≠ y

* affect (x, v, a) = pair (x, v, supp (x, a))

* assoc (x, emptalist) = novalue
`assoc (x, pair (x, v, a)) = v`

`assoc (x, pair (y, v, a)) = assoc (x, a) x ≠ y`

`assoc (x, supp (y, a)) = assoc (x, a)`

Définition des autres accès :

`type atom, cell, progadr, alist`

`type value = union (atom, cell)`

`accès (atom) value : apval, expr, fexpr`

`accès (atom) progadr : subr, fsubr, subrc, fsubrc`

`accès progadr : noprog`

`accès value : novalue`

`accès (value) value : atom`

`accès (cell) value : car, cdr`

`accès (value, value) cell : cons`

`accès value : nil`

`accès atom : t`

`accès (value, value, alist) value : apply`

`accès (value, value, alist) alist : transply`

et tous les accès associés (eval, evlis, evcon... transval, translis...)

b. Interprète :

- écrit en simili Algol 68

- les accès élémentaires sont écrits en majuscules

- la structure du texte est décrite sous forme d'accès car et cdr à une
liste, après éventuel test atomique. Exemples :

`car ((a b c)) = a`

`cdr ((a b c)) = (b c)`

`cdr ((a)) = ( )`

`atom (a) = t`

`atom (...)) = nil`

`list (a, b, c) = (a b c)`

`cons (a,(b c)) = (a b c)`

- les arguments sont passés par valeur.
`proc` apply (function, listvarg, alist)

`if` atom (function) = t

`then` if `SUBR` or `SUBRC` (function) or `FSUBR` or `FSUBRC` (function) ≠ `noprog`

`then` exec (function, listvarg, alist)

`elif` `EXPR` (function) ≠ `novalue`

`then` apply (`EXPR`(function), listvarg, alist)

`elif` `FEXPR` (function) ≠ `novalue`

`then` apply (`FEXPR`(function), listvarg, alist)

`else` apply (`ASSOC`(function, alist), listvarg, alist) `fi`

`elif` car (function) = `LAMBDA`

`then` if `atom` (cadr(function)) = t

`then` `eval` (caddr(function), pair (cadr(function), listvarg, alist))

`else` `eval` (caddr(function), pairlis(cadr(function), listvarg, alist)) `fi`

`else` apply (`eval`(function, alist), listvarg, transval (function, alist))

`fi`

`proc` transpy (function, listvarg, alist)

`if` atom (function) = t

`then` if `SUBR` (function) or `SUBRC` (function) or `FSUBR`(function) or `FSUBRC`

(function) ≠ `noprog`

`then` transpy (function, listvarg alist)

`co` dans ce cas transpy est connu, function ayant été compilée `co`

`elif` `EXPR` (function) ≠ `novalue`

`then` transpy (`EXPR`(function), listvarg, alist)

`elif` `FEXPR` (function) ≠ `novalue`

`then` transpy (`FEXPR` (function), listvarg, alist)

`else` transpy (`ASSOC` (function, alist), listvarg, alist) `fi`

`elif` car (car (function) = `LAMBDA`

`then` if `atom` (cadr (function)) = t

`then` `supp` (cadr (function), transval (caddr (function), pair (cadr (function), listvarg, alist)))

`else` `supplis` (cadr (function), transval (caddr (function), pairlis (cadr (function), listvarg, alist))) `fi`

`else` transpy (`eval` (function, alist), listvarg, transval (function, alist))

`proc` `eval` (form, alist)

`if` `atom` (form) = t

`then` if `form` = number
then APVAL (number)
elif form = constant
then APVAL (form)
else ASSOC (form, alist) fi
elif form = ( )
then NIL
elif car (form) = QUOTE
then CADR (form) (1)
elif car (form) = COND
then evcon (cdr(form))
elif car (form) = SETQ
then CADR (form) (1)
elif car (form) = NEXTL
then CAR (ASSOC (cadr (form), alist)
elif atom (car (form)) = t
then if SUBR (car (form)) or SUBRC (car(form)) ≠ noprog or EXPR (car(form)) ≠ novalue
then apply (car(form), evlis (cdr(form),alist), translis (cdr(form),alist))
elif FSUBR (car(form)) or FSUBRC (car(form)), ≠ noprog or FEXPR (car(form)) ≠ novalue
then apply (car(form), cdr(form),alist)
else apply (car(form), evlis (cdr(form),alist), translis (cdr(form),alist)) fi
else apply (car(form), evlis (cdr(form),alist), translis (cdr(form),alist))
fi
proc transval (form, alist)
if atom (form) = t
then alist
elif form = ( ) or car (form) = QUOTE
then alist
elif car (form) = COND
then transcon (cdr(form), alist)
elif car (form) = SETQ
Then affect (cadr(form), eval(caddr(form),alist), transval(caddr(form),alist))
elif car (form) = NEXTL
then affect (cadr(form), CDR (ASSOC (cadr (form))), alist)

<footnote>(1) Le résultat est un élément de texte.</footnote>
elif atom (car (form)) = t

then if SUBR or SUBRC (car(form)) ≠ noprog or EXPR (car(form)) ≠ novalue
then transply (car(form), evlis (cdr(form), alist), translis (cdr(form), alist))
elif FSUBR or FSUBRC (car(form)) ≠ noprog or FEXPR (car(form)) ≠ novalue
then transply (car(form), cdr(form), alist)

fi

else transply (car(form), evlis (cdr(form), alist), translis (cdr(form), alist))

fi

proc evcon (listcond, alist)

if listcond = ( )

then NIL

elif eval (caar (listcond), alist) ≠ NIL

then eval (cadar (listcond), transval (caar (listcond), alist))

else evcon (cdr (listcond), transval (caar (listcond), alist))

fi

proc transcon (listcond, alist)

if listcond = ( )

then alist

elif eval (caar (listcond), alist) ≠ NIL

then transval (cadar (listcond), transval (caar (listcond, alist)))

else transcon (cdr (listcond), transval (caar (listcond, alist)))

fi

proc evlis (listarg, alist)

if listarg = ( )

then NIL

else CONS (eval (car (listarg), alist), evlis (cdr (listarg), transval (car (listarg), alist)))

fi

proc translis (listarg, alist)

if listarg = ( )

then alist

else translis (cdr (listarg), transval (car (listarg), alist))

fi
proc pairlis(listvar, listvarg, alist)

if listvar = ( )

then alist)

elif listvarg = ( )

then pairlis(cdr(listvar), NIL, pair(car(listvar), NIL, alist))

else pairlis(cdr(listvar), cdr(listvarg), pair(car(listvar), car(listvarg), alist))

fi

proc supplis(listvar,alist)

if listvar = ( )

then alist

else supplis(cdr(listvar), supp(car(listvar), alist))

fi

Simplification de transply :

Transply utilise les accès élémentaires supp et pair. On remarque que
supp a toujours lieu après un pair et que seul transply utilise ces accès,
transval ne faisant que des modifications (affect). Il est donc possible de
simplifier transply en supprimant les appels à supp, pair, supplis et
pairlis :

elif car(function) = LAMBDA

then transval(caddr(function,alist)

else transply(...)

fi

On voit de cette manière que la aliste initiale est conservée aux
modifications près de transval seulement.

Traitement des variables :

Une variable peut être :

- liée dans une fonction compilée : (LAMBDA(X)(CAP X))

- libre dans une fonction compilée : (LAMBDA(X)(CONS X Y))
  auquel cas elle peut être :

- une constante (LAMBDA(X)(PLUS X 1))

- une fonction (LAMBDA(X)(F X))

- une variable partagée avec l'interpréteur ou avec d'autres fonctions compilées.

D'une manière générale toutes les variables sont partagées et ont
donc leur valeur liée dans la aliste.
Structure de la place d'atome identique à celle de l'atome (A1-B-a-1)
avec les accès apval, expr, fexpr, subr et fsubr (assoc est remplacé par
btop).

Définition de la structure bstack :

Define type bstack

type x : platom, bstackelt, value

accès (bstack) bstackelt : btop(x)

accès (bstackelt) value : val

accès value : novalue

accès (value, bstack) bstack : pushb(x)

accès (bstack) bstack : popb(x)

accès (value, bstack) bstack : change(x)

Les axiomes de bstack comportent :

- les axiomes des piles correspondant aux accès paramètres : btop(x),
pushb(x), popb(x), change(x) et val,

- les axiomes d'indépendance entre piles paramétrées,

- et : btop(x) (emptbstack) = emptbstack(x)
  val(emptbstack(x)) = novalue

Comme pour la alist, on admet que l'accès popb est toujours défini.

Définition de la structure stack :

Define type stack

type stackelt, value

accès stackelt : top

accès (stackelt) stackelt : s, s⁻¹

accès (stackelt) value : c

accès stack : emptstack

accès (value, stack) stack : push

accès (stack) stack : pop

Les axiomes sont ceux de la pile.

De plus, on adopte la notation :

$$
s^n(y : stackelt) \equiv y-n
$$

$$
s^{-n}(y : stackelt) \equiv y+n
$$
# ANNEXE 2.

## Langage Objet

### A - Machine Abstraite

(a) Zone mémoire avec un nombre potentiellement infini de cellules (liste libre et ramasse-miettes ne sont pas traités ici).

(b) Table d'atomes potentiellement infinie contenant les noms d'atomes et leurs emplacements avec les accès search et name = search⁻¹.

(c) Pile des arguments dénotée par son sommet st et le contenu d'un élément de rang r = c(r).

(d) Piles d'associations dénotées pour chaque place d'atome x par l'accès à son sommet (btop) et le contenu de celui-ci qui est un pointeur sur un élément de la pile des arguments (accès r). L'ensemble des piles d'associations forme l'objet "bstach".

(e) Pile des adresses de retour (non décrite ici).

(f) Zone des programmes.

(g) Compteur ordinal (ci).

(h) Accès au nombre d'arguments de la fonction appelée (na)

Cycle : exécuter l'instruction d'adresse ic jusqu'à rencontrer une instruction d'arrêt.

### B - Structure de la machine abstraite :

Schéma de la structure décrite :

<figure><img src="image_11.png" /></figure>
C - Code objet :

ic=a, stack=b {PUSHQ S-expr} ic=a+1, stack = push(S-expr, b)

ic=a, stack=b {PUSHV x i} ic=a+1, stack = push(c(top-i), b), val(btop(x)(d))=c(top)

ic=a, stack=b, {PUSHV x} ic=a+1, stack=push(val(btop(x)(d)), b)

ic=a, bstack = b {PUSHB x i} ic=a+1, bstack=pushb(x), (c(top-i),b)

ic=a, bstack=b {POPB x} ic=a+1, bstack=popb(x)(b)

ic=a, bstack=b {SET x i} ic=a+1, bstack=change(x)(c(top),b), c(top-i)=c(top)

ic=a, bstack=b {SET x} ic=a+1, bstack=change(x)(c(top),b)

ic=a, top=b {POP n} ic=a+1, top=b-n, c(top)=c(b)

ic=a, top=b {POP} ic=a+1, top=b-1

ic=a, stack=b {PUSHA x} ic=a+1, stack=push(apval(x),b)

{ BR lab } ic=lab

ic=a { BRN lab } ic=if c(top)=nil then lab else a+1 fi
ic=a,top=b { LINK n f } ic=a+1, top=b+1
bstack=A(α) { } bstack=A(transply(f,1vg,α))

list(c(b)...c(b-n+1))=I(lvg) c(top)=I(exec(f,1vg,α))

si f est SUBR ou FSUBR

c(b)=I(lvg) et n=1

si f est SUBRC ou FSUBRC

Cette définition suppose la terminaison de la fonction f.

ic=a { RETURN } ic=cr returntop la structure de la pile des
         } adresses retour n'est pas décrite ici

ic=a { CAR } ic=a+1
top=b { } c(top)=car(c(b))

idem pour { CDR } 
top=a { SWAP } top=a
c(top)=d
c(top-1)=b

top=a { CONS } top=a+1
c(top)=b c(top)=cons(d,b)
c(top-1)=d

Exemple :

FACT : (LAMBDA(N)(COND((ZEROP N)1)
             (T(TIMES N
               (FACT(SUB1 N)) )) ))

1 : PUSHB N 0 ;

2 : PUSHV N 0 ;

3 : LINK 1 ZEROP ;

4 : POP 1 ;

5 : BRN 9 ;

6 : POP ;

7 : PUSHA 1 ;

8 : BR 20 ;

9 : PUSHA T ;

10 : BRN 20 ;

11 : POP ;

12 : PUSHV N 0 ;

13 : PUSHV N 1 ;
14 : LINK 1 SUB1 ;

15 : POP 1 ;

16 : LINK 1 FACT ;

17 : POP 1 ;

18 : LINK 2 TIMES ;

19 : POPE2 ;

20 : PORB N ;

21 : RETURN ;

D - Fonctions $\mathcal{I}$ et $\mathcal{A}$

$\mathcal{I}$ : fonction d'implantation des S-expressions, cellules et atomes. On a :

$\mathcal{I}(u : \text{value}) = u : \text{value}$ (le même type a été utilisé mais :

$\mathcal{I}(x : \text{atom}) = \text{search}(x) : \text{platom}$

$\mathcal{I}(\text{liste de n arguments}) = \text{list}(c(top-n+1)..c(top))$

$\mathcal{I}(\text{car}(v)) = \text{car}(\mathcal{I}(v)) \text{ id cons}$

$\mathcal{A}$ : fonction d'implantation du contexte (cf A1-B-a-1)

$\mathcal{A}(x : \text{atom}) = \text{search}(x) : \text{platom}$

$\mathcal{A}(u : \text{value}) = u : \text{value}$ (même type utilisé)

$\mathcal{A}(\alpha : \text{alist}) = \beta : \text{bstack}$

$\mathcal{A}(\text{emptalist}) = \text{emptbstack}$

$\mathcal{A}(\text{pair}(x : \text{atom}, v : \text{value}, \alpha : \text{alist})) = \text{pushb}(\text{search}(x))(\mathcal{I}(v), \mathcal{A}(\alpha))$

$\mathcal{A}(\text{supp}(x:\text{atom},\alpha:\text{alist})) = \text{popb}(\text{search}(x),\mathcal{A}(\alpha))$

$\mathcal{A}(\text{affect}(x,v,\alpha)) = \text{change}(\text{search}(x))(\mathcal{I}(v),\mathcal{A}(\alpha))$

$\mathcal{I}(\text{assoc}(x,\alpha)) = \text{val}(\text{btop}(\text{search}(x))(\mathcal{A}(\alpha)))$

**Nota** : dans les définitions on a confondu $x$ et $\text{search}(x)$. Cette confusion sera maintenue par la suite, sachant que dans la machine abstraite toute référence à un atome $x$ désigne en fait une place d'atome.
# ANNEXE 3

## A - Définition des attributs. (S = synthétisé, H = hérité)

<table><thead><tr><th>a) Nom</th><th>Type</th><th>Signification</th></tr></thead><tbody><tr><td>S. CEVAL</td><td>Ensemble</td><td>Ensemble ordonné des instructions générées en langage machine. Chaque instruction est précédée de son label.</td></tr><tr><td>H. LAB</td><td>Entier</td><td>Label de la première instruction exécutable de l'ensemble correspondant.</td></tr><tr><td>S. LAB</td><td>"</td><td>Label de la prochaine instruction exécutable après exécution de l'ensemble correspondant.</td></tr><tr><td>S. POBOUND</td><td>Ensemble</td><td>Ensemble ordonné des instructions générées liant les variables.</td></tr><tr><td>S. PUBOUND</td><td>"</td><td>id. déliant les variables.</td></tr><tr><td>H. LAB1</td><td>Entier</td><td>Label de la prochaine instruction PUSHB de l'ensemble correspondant.</td></tr><tr><td>H. LAB2</td><td>"</td><td>id. pour POPB</td></tr><tr><td>H. TOP</td><td>"</td><td>Entier n représentant s<sup>n</sup>(top) où top est l'état initial du sommet de la pile des arguments au moment de l'exécution de l'expression compilée.</td></tr><tr><td>S. NARG, H. NARG</td><td>"</td><td>Nombre d'arguments.</td></tr><tr><td>H. NVAR</td><td>"</td><td>Nombre total de variables de la LAMBDA expression considérée.</td></tr><tr><td>S. NVAR</td><td>"</td><td>Nombre de variables sous le non terminal considéré.</td></tr><tr><td>H. TAB</td><td>Tableau(chaine,Entier)</td><td>Tableau de la correspondance nom de variable - emplacement dans la pile des arguments.</td></tr><tr><td>TEXT</td><td>Texte</td><td>Attribut standard.</td></tr></tbody></table>
b) Non-terminaux auxquels sont définis les attributs :

S.CEVAL : tous sauf listvar

H.LAB : id. sauf prog

S.LAB : id.

S.POBOUND : listvar

S.PUBOUND : id.

H.LAB1 : id.

H.LAB2 : id.

H.NVAR : id.

S.NVAR : id.

H.TOP : tous sauf prog

S.NARG : listarg, listexpr

H.NARG : function, f-function

H.TAB : tous sauf listvar, prog.

Nota : TEXT est utilisé aux terminaux : number, constant, Ident, S-expr.

c) Cas de H.TAB :

Traitement des variables liées d'une fonction compilée :

A l'entrée d'une fonction, la pile des arguments a une certaine hauteur $h_0$ avec $h_0-n+1, \dots, h_0-1, h_0$ les n arguments de la fonction.

A un instant donné du calcul de cette fonction, on a donc la configuration suivante (fig. 1).
Chaque fois que l'on génère une instruction PUSHV X i ou SET X i, on sait que la valeur recherchée se trouve à l'emplacement décalé de i par rapport au sommet, soit :

$$i = h - h_{0} + n - p$$

La valeur $h_0+n-p$ est donc immuable au cours de la durée de vie de la variable liée. Pour la préserver, il suffit d'hériter cette valeur, associée à X dans les sous-expressions où X est susceptible d'être liée. Ceci est fait par la table H.TAB comportant le nom de la variable et le rang de sa dernière déclaration soit :

$$h_{0} - n + p$$

où $H.TOP-H.NVAR+S.NVAR^{(1)}$ (on suppose qu'il y a toujours le même nombre d'arguments que de variables à lier).

Dans la génération de code, il sera donc possible d'utiliser indifferemment la valeur associée située en sommet de pile des liens - val(btop(x)) - ou la valeur située dans la pile des arguments (pour une variable liée) située à :

$i = H.TOP-ind(x.H.TAB)^{(2)}$ du sommet courant (H.TOP).

Il est aisé de vérifier que $c(i)$ et $val(btop(x))$ sont constamment égaux quels que soient H.TAB et H.TOP. Ils le sont en effet au moment de la liaison (par construction) et pour la suite $c(i)$ et $val(btop(x))$ sont modifiés conjointement par la seule instruction SET.

A l'intérieur d'un bloc où H.TAB est héritée (donc pour la portée des variables définies dans les LAMBDA expressions) ces indices ni leur contenu ne sont jamais modifiés puisque la pile des arguments ne fait que croître. Ceci peut être directement vérifié sur les assertions (A4-A) où top est soit inchangé, auquel cas les contenus sont préservés, soit croît avec des contenus pour les nouveaux éléments seulement.

<footnote>(1) cf. A3-A.</footnote>

<footnote>(2) notation : x sélectionne l'élément x de la table et ind est l'indice associé à x dans la table.</footnote>
B - Traducteur

R1 <Prog> = (LAMBDA (<Listvar>) <Form>)
S1 S. CEVAL(Prog) := S.PUBOUND(Listvar)
                 S.CEVAL(Form)
                 S.POBOUND(Listvar)
                 S.LAB(Form) + S.NVAR(Listvar) : RETURN;
S2 H.LAB1(Listvar) := 1
S3 H.LAB2(Listvar) := S.LAB(Form)
S4 H.LAB(Form)     := H.LAB1(Listvar) + S.NVAR(Listvar)
S5 H.TOP(Listvar)  := 0
S6 H.TOP(Form)     := 0
S7 H.NVAR(Listvar) := S.NVAR(Listvar)
S8 H.TAB(Form)     := S.TAB(Listvar)

R2 <Prog> = (LAMBDA Ident <Form>)
S1 S.CEVAL(Prog) := 1 : PUSHB TEXT(Ident) 0;
                CEVAL(Form)
                S.LAB(Form) : POPB TEXT(Ident) ;
                S.LAB(Form) + 1 : RETURN;
S2 H.LAB(Form) := 2
S3 H.TOP(Form) := 0
S4 H.TAB(Form) := insert emptytab, TEXT(Ident), 0)

R3 <Listvar> = <Listvar> Ident
S1 S.PUBOUND(Listvar) := S.PUBOUND(Listvar')
                  H.LAB1(Listvar') + S.NVAR(Listvar') : PUSHB TEXT(Ident)
                  H.NVAR(Listvar) - S.NVAR(Listvar) ;
S2 H.LAB1(Listvar') := H.LAB1(Listvar)
S3 H.TOP(Listvar') := H.TOP(Listvar)
S4 H.NVAR(Listvar') := H.NVAR(Listvar)
S5 S.NVAR(Listvar) := S.NVAR(Listvar') + 1
S6 S.TAB(Listvar) := insert(S.TAB(Listvar'), TEXT(Ident),
                           H.TOP(Listvar) - N.NVAR(Listvar) + S.NVAR(Listvar))
S7 S.POBOUND(Listvar) := S.POBOUND(Listvar')
                  H.LAB2(Listvar') + S.NVAR(Listvar') : POPB TEXT(Ident) ;
S8 H.LAB2(Listvar') := H.LAB2(Listvar)
R4 `<Listvar>` = empty

S1 S.PUBOUND(Listvar) := emptyset

S2 S.NVAR(Listvar) := 0

S3 S.TAB(Listvar) := emptytab

S4 S.POBOUND(Listvar) := emptyset

R5 `<Form>` = number

S1 S.CEVAL(Form) := H.LAB(Form) : PUSHA TEXT(number ;

S2 S.LAB(Form) := H.LAB(Form) + 1

R6 `<Form>` = ( )

S1 S.CEVAL(Form) := H.LAB(Form) : PUSHQ NIL ;

S2 id

R7 `<Form>` = constant

id R5

R8 `<Form>` = Ident

S1 S.CEVAL(Form) :=
    if TEXT(Ident) ∈ name(H.TAB(Form))
    then H.LAB(Form) : PUSHV TEXT(Ident) H.TOP(FORM) -
        ind(TEXT(Ident).H.TAB(Form)) ;
    else H.LAB(Form) : PUSHV TEXT(Ident) ;
fi
S2 S.LAB(Form) := H.LAB(Form) + 1

R9 `<Form>` = `<Formna>`

S1 S.CEVAL(Form) := S.CEVAL(Formna)

S2 H.LAB(Formna) := H.LAB(Form)

S3 S.LAB(Form) := S.LAB(Formna)

S4 H.TOP(Formna) := H.TOP(Formn)

S5 H.TAB(Formna) := H.TAB(Form)

R10 `<Formna>` = (QUOTE S-expr)

S1 S.CEVAL(Form) := H.LAB(Form) : PUSHQ TEXT(S-expr) ;

S2 S.LAB(Formna) := H.LAB(Formna) + 1
R11 `<Formna> = (COND <Listcond>)`
S1 S.CEVAL(Formna) := S.CEVAL(Listcond)
S2 H.LAB(Listcond) := H.LAB(Formna)
S3 S.LAB(Formna) := S.LAB(Listcond)
S4 H.TOP(Listcond) := H.TOP(Form)
S5 H.TAB(Listcond) := H.TAB(Form)

R12 `<Formna> = (SETQ Ident <Form>)`
S1 S.CEVAL(Formna) := S.CEVAL(Form)
    if TEXT(Ident) ∈ name (H.TAB(Form))
    then S.LAB(Form) := SET(Ident) H.TOP(Form)+1-ind TEXT(Ident).
        H.TAB(Form)) ;
    else S.LAB(Form) := SET TEXT(Ident) ;
    fi
S.LAB(Form) +1 : PUSHQ TEXT(Ident) ;
S.LAB(Form) +2 : POP 1 ;
S2 H.LAB(Form) := H.LAB(Formna)
S3 S.LAB(Formna) := S.LAB(Form) + 3
S4 H.TOP(Form) := H.TOP(Formna)
S5 H.TAB(Form) := H.TAB(Formna)

R13 `<Formna> = (NEXTL Ident)`
S1 S.CEVAL(Formna) :=
    if TEXT(Ident) ∈ name (H.TAB(Formna))
    then H.LAB(Formna) := PUSHV TEXT(Ident) H.TOP(Formna)-ind TEXT(Ident).
        H.TAB(Formna)) ;
    H.LAB(Formna)+1 : CAR ;
    H.LAB(Formna)+2 : PUSHV TEXT(Ident) H.TOP(Formna)+1-ind TEXT(Ident) . H.TAB(Formna)) ;
    H.LAB(Formna)+3 : CDR ;
    H.LAB(Formna)+4 : SET TEXT(Ident) H.TOP(Formna)+2-ind TEXT(Ident) . H.TAB(Formna)) ;
    H.LAB(Formna)+5 : POP ;
    else H.LAB(Formna) := PUSHV TEXT(Ident) ;
    H.LAB(Formna)+1 : CAR ;
    H.LAB(Formna)+2 : PUSHV TEXT(Ident) ;
    H.LAB(Formna)+3 : CDR ;
    H.LAB(Formna)+4 : SET TEXT(Ident) ;
    H.LAB(Formna)+5 : POP ;
S2 S.LAB(Formna) := H.LAB(Formna)+6
R14 <Formna> = (<Function> <Listarg>)
S1 S.CEVAL(formna) := S.CEVAL(Listarg)
S.CEVAL(Function)
S.LAB(Function) : POP S. NARG(listarg) ;
S2 H.LAB(Listarg) := H.LAB(formna)
S3 H.LAB(function) := S.LAB(Listarg)
S4 S.LAB(formna) := S.LAB(function)
S5 H.TOP(Listarg) := H.TOP(formna)
S6 H.TOP(function) := H.TOP(formna)+S.NARG(Listarg)
S7 H.TAB(function) := H.TAB(formna)
S8 H.TAB(Listarg) := H.TAB(formna)
S9 H.NARG(function):= S.NARG(Listarg)

R15 <Formna> = (<Functionc> <Listargc>)
Définitions identiques en remplaçant S.NARG(Listarg) par 1 dans R14.

R16 <Formna> = (<F-Functionc> <Listexprc>)
Définitions identiques à R14

R17 <Formna> = (<F-Functionc> <Listexprc>)
Définitions identiques à R15

R18 <Function> = (LAMBDA(<Listvar>) <Form>)
S1 S.CEVAL(Prog) := S.PUBOUND(Listvar)
S.CEVAL(Form)
S.POLROUND(Listvar)
S2 H.LAB1(Listvar) := H.LAB(function)
S3 H.LAB2(Listvar) := S.LAB(Form)
S4 H.LAB(Form) := H.LAB1(Listvar)+S.NVAR(Listvar)
S5 S.LAB(function) := H.LAB2(Listvar)+S.NVAR(Listvar)
S6 H.TOP(Listvar) := H.TOP(function)
S7 H.TOP(Form) := H.TOP(function)
S8 H.NVAR(Listvar) := S.NVAR(Listvar)
S9 H.TAB(Form) := union(1) (H.TAB(function), S.TAB(Listvar))

(1) L'union modifie les indices des variables de même nom, en remplaçant les
les anciens (hérités dans H.TAB(Function)) par les nouveaux (construits
dans S.TAB(Listvar)).
R19 `<Function>` = Subr

S1 S.CEVAL(Function) := H.LAB(Function) : LINK H.NARG(Function) TEXT(Subr) ;

S2 S.LAB(Function) := S.LAB(Function) + 1

R20 `<Functionc>` = (LAMBDA Ident `<Form>`)

S1 S.CEVAL(Functionc) := H.LAB(Functionc) : PUSHB TEXT(Ident) 0 ;
CEVAL(Form)

S.LAB(Form) : POP TEXT(Ident) ;

S2 H.LAB(Form) := H.LAB(Functionc) + 1

S3 S.LAB(Functionc) := S.LAB(Form) + 1

S4 H.TOP(Form) := H.TOP(Functionc)

S5 H.TAB(Form) := insert(H.TAB(Functionc), TEXT(Ident), 0)

R21 `<Functionc>` = Subrc

S1 S.CEVAL(Function) := H.LAB(Function) : LINK 1 TEXT(Subrc) ;

S2 S.LAB(Function) := H.LAB(Function) + 1

R22 `<F-Function>` = F-Subr

S1 S.CEVAL(F-Function) := H.LAB(F-Function) : LINK H.NARG(F-Function) TEXT(F-Subr) ;

S2 S.LAB(F-Function) := H.LAB(F-Function) + 1

R23 `<F-Functionc>` = F-Subr

S1 S.CEVAL(F-Functionc) := H.LAB(F-Function) : LINK 1 TEXT(F-Subrc) ;

S2 S.LAB(F-Functionc) := H.LAB(F-Functionc) + 1

R24 `<Listcond>` = `<Form> <Form>`

S1 S.CEVAL(Listcond) := S.CEVAL(Form)

S.LAB(Form) : BRN S.LAB(Listcond) ;

S.LAB(Form)+1 : POP ;

S.CEVAL(Form')

S2 H.LAB(Form) := H.LAB(Listcond)

S3 H.LAB(Form') := S.LAB(Form)+2

S4 S.LAB(Listcond) := S.LAB(Form)

S5 H.TOP(Form) := H.TOP(Listcond)

S6 H.TOP(Form') := H.TOP(Listcond)

S7 H.TAB(Form) := H.TAB(Listcond)

S8 H.TAB(Form') := H.TAB(Listcond)
R25 <Listcond> = empty
S.CEVAL(Listcond) := H.LAB(Listcond) : <PUSHQ NIL;
S.LAB(Listcond) := H.LAB(Listcond)+1

R26 <Listarg> = <Listarg> <Form>
S1 S.CEVAL(Listarg) := S.CEVAL(Listarg)
S.CEVAL(Form)
S2 H.LAB(Listarg') := H.LAB(Listarg)
S3 H.LAB(Form) := S.LAB(Listarg')
S4 S.LAB(Listarg) := S.LAB(Form)
S5 H.TOP(Listarg') := H.TOP(Listarg)
S6 H.TOP(Form) := H.TOP(Listarg')+S.NARG(Listarg')
S7 S.NARG(Listarg) := S.NARG(Listarg')+1
S8 H.TAB(Listarg') := H.TAB(Listarg)
S9 H.TAB(Form) := H.TAB(Listarg)

R27 <Listarg> = empty
S1 S.CEVAL(Listarg) := emptyset
S2 S.LAB(Listarg) := H.LAB(Listarg)
S3 S.NARG(Listarg) := 0

R28 <Listexpr> = <Listexpr> S-expr
S1 S.CEVAL(Listexpr) := S.CEVAL(Listexpr')
S.LAB(Listexpr) : <PUSHQ TEXT(S)expr> ;
S2 H.LAB(Listexpr') := H.LAB(Listexpr)
S3 S.LAB(Listexpr) := S.LAB(Listexpr')+1
S4 H.TOP(Listexpr') := H.TOP(Listexpr)
S5 H.TAB(Listexpr') := H.TAB(Listexpr)
S6 S.NARG(Listexpr) := S.NARG(Listexpr')

R29 <Listexpr> = empty
Idem R27 avec Listexpr au lieu de Listarg

R30 <Listargc> = <Form> <Listargc>
S1 S.CEVAL(Listargc) := S.CEVAL(Form)
S.CEVAL(Listargc')
S.LAB(Listargc') : <CONS ;
S.LAB(Listargc')+1 : <POP 2 ;
S2 H.LAB(Form) := H.LAB(Listargc)
S3 H.LAB(Listargc') := S.LAB(Form)
S4 S.LAB(Listargc) := S.LAB(Listargc')+2
S5 H.TOP(Form) := H.TOP(Listargc)
S6 H.TOP(Listargc) := H.TOP(Listargc)+1

S7 H.TAB(Form) := H.TAB(Listargc)

S8 H.TAB(Listargc) := H.TAB(Listargc)

R.31 <Listargc> = empty

S1 S.CEVAL(Listargc) := H.LAB(Listargc) : PUSHQ nil ;

S2 H.LAB(Listargc) := S.LAB(Listargc)+1

R32 <Listexprc> = S-expr <Listexprc>

S1 S.CEVAL(Listexprc) := H.LAB(Listexprc) : PUSHQ TEXT(S-expr) ;
S.CEVAL(Listexprc')

S.LAB(Listexprc') : CONS ;

S.LAB(Listexprc')+1 : POP 2 ;

S2 H.LAB(Listexprc') := H.LAB(Listexprc)+1

S3 S.LAB(Listexprc) := S.LAB(Listexorc')+2

S4 H.TOP(Listexprc') := H.TOP(Listexprc)+1

S5 H.TAB(Listexprc') := H.TAB(Listexprc)

R33 <Listexprc> = empty

S1 S.CEVAL(Listexpr) := H.LAB(Listexpr) : PUSHQ nil ;

S2 S.LAB(Listexpr) := H.LAB(Listexpr)+1
# ANNEXE 4

## A - Assertions aux non-terminaux

Pour chaque groupe de non-terminaux on indique les états de la machine abstraite correspondant à avant et après exécution de l'ensemble d'instructions générées à chaque non-terminal.

Les attributs décrivant l'évolution de l'état de la NA apparaissent. De plus, l'accès push peut être remplacé par une description équivalente utilisant les attributs. Ainsi :

(A4)

```
stack = b      { } stack = push (I(evlis(lf,α)),b)

devient :

top = H.TOP   { } top = H.TOP + 1
              c(top) = I(evlis(lf,α))
```

C'est la seconde forme qui sera utilisée pour la preuve. De plus, le nom du non-terminal (lf ici) est confondu avec son texte qui serait TEXT(lf). Pour simplifier l'écriture, on se contentera d'écrire toujours le nom du non-terminal correspondant au texte évalué.

```
A1 à A''

ic = H.LAB,                      ic = S.LAB,

bstack = A(α),                   {CEVAL(f_n)} bstack = A (transply(f_n,la,α))

list(c(H.TOP-H.NARG+1).c(H.TOP)) = I(la) stack=push(I(apply(f_n,la,α)),b)

stack = b

pour : f_n = Prog, (1) Function, Functionc, (2) F-Function, F-Functionc (2)
```

<footnote>(1) Dans ce cas $H.LAB=1$, $H.TOP=0$, $H.NARG = \text{na par convention}(\text{ASS}.A'_1)$, de même que $S.LAB$ n'est pas définie (cf. RETURN(A2-C-1). Notons que $na=1$ dans le cas d'une liste de variables réduites à un atome (assertion $A''_1$)</footnote>

<footnote>(2) Dans ce cas il y a un seul argument et l'on a simplement

$A''_1 : c(H.TOP) = I(la)$.</footnote>
A2 :

ic = H.LAB,

bstack = A(α)

{CEVAL(f)}

stack = b

pour : f = Form, Formna

ic = S.LAB

bstack = A(transval(f,α))

stack = push(I(eval(f,α)),b)

A3 et A'₃

ic = H.LAB

bstack = A(α)

{CEVAL(lf)}

top = H.TOP

ic = S.LAB

bstack = A(translis(lf,α))

top = H.TOP + S.NARG

list(c(H.TOP+1)..c(H.TOP+S.NARG)) =
I(evlis(lf,α))

pour : lf = listarg, listexpr (3)

A4 et A'₄

ic = H.LAB

bstack = A(α)

{CEVAL(lf)}

stack = b

pour : lf = listargc, listexprc (3)

ic = S.LAB

bstack = A(translis(lf,α))

stack =

I(evlis(lf,α))

A5

ic = H.LAB

bstack = A(α)

{CEVAL(lc)}

stack = b

pour : lc = listcond

ic = S.LAB

bstack = A(transcon(lc,α))

stack = push(I(evcon(lc,α)), b)

A6

ic = H.LAB!

bstack = A(α)

{PUBOUND(lv)}

list(c(H.TOP-N.NVAR+1)..

c(H.TOP-N.NVAR+S.NVAR)) = I(S.NVAR(la))

ic = H.LAB + S.NVAR

bstack = A(pairlis

(S.NVAR(lv), S.NVAR(la),α))

où n(1)=liste des n premiers éléments de la liste 1

<footnote>(3) Dans ce cas, il n'y a pas évaluation des arguments, bstack n'est donc pas modifié et I(evlis(lf,α)) devient simplement I(lf) (A'₃ et A'₄)</footnote>
ic = 1 = H.LAB1(Listvar)
bstack = A(α) identité
list(c(-na+1)..c(c0))=I(1a) identité(S5,S7) et si même nb. de var. que
top = 0 d'arg. ts

PUBOUND(A6)
ic = H.LAB1 → ic = H.LAB1+N.VAR(Hyp.)=H.LAB(Form) (S4)
bstack = A(α) → bstack=A(pairlis(S.NVAR(Listvar), S.NVAR(1a),α)) (Hyp)
list(c(H.TOP-H.NVAR+1)..(c(H.TOP-H.NVAR+S.NVAR))=I(S.NVAR(1a)))

CEVAL(A2)
ic = H.LAB(Form) → ic = S.LAB(Form) = H.LAB2(Form) (S3)
bstack = cf. ci-dessus → bstack = A(transval(form, pairlis(listvar, la, α)))
top = 0 (inchangé) → top = 1
c(top) = I.eval(form, pairlis(listvar, la, α)))

POBOUND(A7)
ic = H.LAB2(Form) → ic = H.LAB2(Listvar)+S.NVAR(Listvar) id. selon S3
bstack = cf ci-dessus → A(supplis(listvar, transval(form, pairlis(listvar, la, α))))

RETURN(Définition)
ne modifie que ic.

L'identification avec A' est immédiate puisque c(top) et bstack sont les
termes exacts de la définition de apply et transpy dans ce cas.

R2 <Prog> = (LAMBDA Ident<Form>)
S1 : S.CEVAL(Prog) := 1 : PUSHB TEXT(Ident) 0 ;
CEVAL(Form)
S.LAB(Form) : POPB TEXT(Ident)
S.LAB(Form)+1 : RETURN ;

ic = 1
bstack = A(α)
c(0) = I(1a)
top = 0

PUSHB(Définition de PUSHB x i)
ic = 2 = H.LAB(Form) (S2)
bstack=pushb(TEXT(Ident))(c(0),A(α)) = A(pair(TEXT(Ident), la,α)définition de A
CEVAL(A2)

ic = S.LAB(Form)

bstack = A(transval(form,pair(TEXT(Ident),la,α)))
top = 1 (S3 et A2)
c(top) = I.eval(form,transval(form,pair(TEXT(Ident),la,α))))

POPB(Définition de POPB x)

ic = S.LAB(Form)+1

bstack = popb(TEXT(Ident)) (A(transval(...)))

RETURN

ic = crarfurnertop)
bstack = A(supp(TEXT(Ident),transval(form,pair(TEXT(Ident),la,α))))
top = 1
c(top) = I.eval(form,transval(form,pair(TEXT(Ident),la,α))))

La comparaison avec A''_1, compte tenu des définitions de apply et transply
dans ce cas, confirme le résultat.

R3 Listvar = Listvar Ident
S1. S.PUBOUND(Listvar) := S.PUBOUND(Listvar')
    H.LAB1(Listvar')+S.NVAR(Listvar') : PUSHB TEXT(Ident)
    H.TOP(Listvar)-H.NVAR(Listvar)+S.NVAR(Listvar)_;

(A6)

ic = H.LAB1(Listvar)
bstack = A(α)

list(c(H.TOP(Listvar)-H.NVAR(Listvar)+1)..c(H.TOP(Listvar)-H.NVAR(Listvar)+S.NVAR(Listvar))))

= I(S.NVAR(Listvar)(1a))
implique :
    ic = H.LAB1(Listvar') (S2)
bstack = A(α)

list(c(H.TOP(Listvar')-N.NVAR(Listvar')+1..c(H.TOP(Listvar')-H.NVAR(Listvar)+S.NVAR(Listvar))))

= I(S.NVAR(Listvar')(1a)) (S3, S4, S5)

PUBOUND (A6)

ic = H.LAB1(Listvar')+S.NVAR(Listvar')
bstack = A(pairlis(S.NVAR(Listvar')(listvar),S.NVAR(Listvar')(la),α)))
PUSHB(Définition)

ic = H.LAB1(Listvar')+S.NVAR(Listvar')+1

bstack = pushb(TEXT(Ident))(c(H.TOP(Listvar)-H.NVAR(Listvar)+S.NVAR(Listvar)),
A(pairlis(...)))

identifié à la conclusion cherchée par S5, S3 bt la définition de A, sachant
que c(H.TOP(Listvar)-H.NVAR(Listvar)+S.NVAR(Listvar)) est le dernier élément
de I(S.NVAR(Listvar)(1a)) selon l'hypothèse de A6.

S7.S.POBOUND(Listvar) := S.POBOUND(Listvar')

H.LAB2(Listvar') + S.NVAR(Listvar') : POPB TEXT(Ident) ;

La démonstration est analogue à la précédente. Il faut remarquer de plus que
l'ordre dans lequel sont générées les instructions POPB est indifférent (Dans
ce cas, on dépile dans le même ordre que l'on a empilé, comme supplis par
rapport à pairlis).

R4 <Listvar> = empty

Immédiat, A6 et 17 s'appliquent en assimilant list(c(H.TOP+1)..C(H.TOP))
à I(nil) et O(1a) à nil, ic et bstack étant inchangés pour un ensemble
vide d'instructions (S1, S2, S4).

R5 <Form> = number

S1 S.CEVAL(Form) := H.LAB(Form) : <PUSHA TEXT(number) ;>
Immédiat d'après A2 et S2.

R6 <Form> = ( )

Immédiat

R7 <Form> = constant

Immédiat

R8 <Form> = Ident

S1 S.CEVAL(Form) :=
  if TEXT(Ident) ∈ name(H.TAB(Form))
  then H.LAB(Form) : <PUSHV TEXT(Ident) H.TOP(Form)-ind(TEXT(Ident)).
  else H.LAB(Form) : <PUSHV TEXT(Ident) ;
  name(H.TAB(Form)) représente l'ensemble des variables liées dans la
  fonction compilée. Selon que l'identificateur représente une variable
  liée ou non, on génère l'instruction PUSHV x i ou PUSHV x.
Le résultat est immédiat selon A2 et S2 puisque val(btop(TEXT(Ident))(A(α))) = I(assoc(TEXT(Ident),α), donc :
=I.eval(TEXT(Ident),α))

R9 <Form> = <Formna>

Immédiat par identification

R10 <Formna> = (QUOTE S-expr)

S1 S.CEVAL(Formna) := H.LAB(Form) : PUSHQ TEXT(S-expr) ;

Immédiat selon la définition de CADR dans éval et sachant que S-expr n'est
par définition jamais vide.

R11 <Formna> = (COND <listcond>)

Immadiat par identification et définition de eval.

R12 <Formna> = (SETQ Ident <Form>)

S1 S.CEVAL(Formna) := S.CEVAL (Form)

if TEXT(Ident) ∈ name (H.TAB(Form))

then S.LAB(Form) : SET TEXT(Ident) H.TOP(Formna)+1 - ind(TEXT(Ident).
H.TAB(Formna)) ;

else S.LAB(Form) : SET TEXT(Ident) ;

fi

S.LAB(Form)+1 : PUSHQ TEXT(Ident) ;
S.LAB(Form)+2 : POP 1 ;

L'identification de l'état initial de A2 au non terminaux Formna et Form
est immédiate.

ic = H.LAB(Form)

bstack = A(α)

top = H.TOP(Form)

S.CEVAL(Form) produit :

ic = S.LAB(Form)

bstack = A(transval(form,α))

top = H.TOP(Form)+1

c(top) = I.eval(form,α))

Le raisonnement pour la clause if-then-else-fi est identique à celui pour
la règle R8 et l'état résultant, d'après la définition de SET est :

ic = S.LAB(form)+1

bstack = change(TEXT(Ident))(c(H.TOP(Form)+1),A(transval(form,α)))
en vérifiant que :

c(H.TOP(Form)+1-H.TOP(Formna)-1+ind(TEXT(Ident).H.TAB(Formna)))=c(H.TOP(Form)+1)

soit :

c(ind(TEXT(Ident).H.TAB(Formna)))=c(H.TOP(Form)+1), c'est à dire l'élément comportant la valeur associée de TEXT(Ident) dans la pile a bien été modifié.

Les effets de PUSHQ TEXT(Ident) et POP1 sont évidents et l'on obtient :

ic = S.LAB(Form')+3

bstack = change(TEXT(Ident))(I.eval(form',α)),A(transval(form',α)))

top = H.TOP(Form')+1

c(top) = TEXT(Ident) = I.eval(formma,α))

Cet état s'identifie à l'état résultat de A2 au non terminal Formna grâce à S3, S4 et la définition de A(affect...) et celle de transval dans ce cas.

R13 <Formna> = (NEXTL Ident)

S1 cf A3-B-R13

Pour vérifier la propriété A2 au non terminal Formna il suffit d'appliquer les instructions décrites dans S.CEVAL(Formna) à partir de l'état :

ic = H.LAB(Formna)

bstack = A(α)

top = H.TOP(Formna)

pour obtenir l'état :

ic = H.LAB(Formna)+6

bstack = change(TEXT(Ident))(cdr(val(btop(TEXT(Ident))(A(α))), A(α)))

top = H.TOP (Formna)+1

c(top) = car (val(btop(TEXT(Ident))(A(α)))))

ce qui est le résultat cherché puisque :

I(car(assoc(x, )))=car(val(btop(x)(A(α))))

A(affect(x, cdr(assoc(x,α))))) =
change(x) (cdr(val(btop(x)(A(α)))) ,A(α))

R14 <Formna> = (<Function> <Listarg>)

S1 S.CEVAL(Formna) := S.CEVAL(Listarg)

S.CEVAL(Function)

S.LAB(Function) : POP S.NARG(Listarg) ;
(A2)

ic = H.LAB(Formna)

bstack = A(α)

top = H.TOP(Formna)

Il est aisé de vérifier que, A1 et A2 étant admis, on obtient avec S2, S3, S5, S6, S9, l'état final :

ic = S.LAB(Function)

bstack = A(transply(function, evlis(listarg, α), translis(listarg, α)))

top = H.TOP(Formna)+1

c(top) = A(apply(function, evlis(listarg, α), translis(listarg, α)))

L'identification est immédiate du fait que function est soit un atome SUBR, soit une LAMBDA expression, soit une forme quelconque non atomique qui traitent le texte correspondant à <Formna> de la même manière (appel de apply avec évaluation des arguments)

R15 <Formna> = (<Functionc> <Listargc>)

La démonstration est identique à celle de R14 en appliquant $A_1''$ au lieu de A1, la fonction étant soit une EXPR, soit une LAMBDA expression qui traitent le texte correspondant à <Formna> de la même manière.

R16 <Formna> = (<F-Function> <Listexpr>)

Démonstration identique à R14 avec $A_3'$

R17 <Formna> = (<F-Functionc> <Listexprc>)

Démonstration identique à R15 avec $A_4'$

R18 <Function> = (LAMBDA(<Listvar>) <Form>)

La démonstration est analogue à celle de R1, avec une instruction de moins (RETURN) et des pré et post-conditions différentes caractérisées par les nouvelles règles S2, S5 et S6. On suppose de plus qu'il y a le même nombre d'arguments que de variables (condition H.NARG(Function) = S.NVAR(Listvar)).

R19 <Function> = Subr

S1 S.CEVAL(Function) := H.LAB(Function) : LINK H.NARG(Function)

TEXT(Subr) :

Immédiat d'après la définition de LINK.
R20 <Functionc> = (LAMBDA Ident <Form>)

La démonstration est analogue à celle de R2 avec une instruction en
moins (RETURN) et des pré et post-conditions différentes caractérisées par les
nouvelles règles S2, S3 et S4.

R21 <Functionc> = Subrc
S1 S.CEVAL(Functionc) := H.LAB(Functionc) : LINK 1 TEXT(Subrc) :
Immédiat d'après la définition de LINK et A''_1.

R22 <F.-Function> = F-Subr
idem R19

R23 <F-Function> = F-Subrc
idem R21

R24 <Listcond> = (<Form> <Form>) <Listcond>
S1 S.CEVAL(Listcond) := S.CEVAL(Form)
S.LAB(Form) : BRN S.LAB(Form')+1 ;
S.LAB(Form)+1 : POP ;
S.CEVAL(Form')
S.LAB(Form') : BR S.LAB(Listcond) ;
S.LAB(Form')+1 : POP ;
S.CEVAL(Listcond')

Préconditions A5 = Préconditions A2

ic = H.LAB(Listcond) = H.LAB(Form) (S2)

bstack = A(α)

top = H.TOP Listcond) = H.TOP(Form) (S6)

S.CEVAL

ic = S.LAB(Form)

bstack = A(transval(form,α))

top = H.TOP(Form)+1, c(top) = I.eval(form,α))

BRN deux cas sont à examiner

1) c(top)=nil alors ic = S.LAB(Form')+1, on exécute :

POP

ic = S.LAB(Form')+2 = H.LAB(Listcond') (S4)

top = H.TOP(Form) = H.TOP(Listcond) (S8)

bstack = A(transval(form,α))
A5

ic = S.LAB(Listcond') = S.LAB(Listcond) (S5)
top = H.TOP(Listcond')+1 = H.TOP(Listcond)+1 (S8)
bstack = A(transcon(listcond', transval(form,α)))
c(top) = I(evcon(listcond', transval(form,α)))
identifié d'après la définition de evcon et transcon.

POP

2) c(top) ≠ nol alors ic = S.LAB(Form)+1, on exécute
ic = S.LAB(Form)+2 = H.LAB(Form') (S3)
top = H.TOP(Form) = H.TOP(Form') (S6,S7)
bstack = A(transval(form,α))

A2

ic = S.LAB(Form')
top = H.TOP(Form')+1 = H.TOP(Listcond)+1 (S7)
c(top) = I.eval(form', transval(form,α)))
bstack = A(transval(form', transval(form,α)))

BR

ic = S.LAB(Listcond)
identifié selon evcon et transcon

R25

<Listcond> =
la démonstration est immédiate

R26

<Listarg> = <Listarg> <Form>
S1 S.CEVAL(Listarg) := S. CEVAL(Listarg')
S. CEVAL(Form)

A3 précondition

ic = H.LAB(Listarg) = H.LAB(Listarg') (S2)
bstack = A(α)
top = H.TOP(Listarg) = H.TOP(Listarg') (S5)
A3 (Listarg')
ic = S.LAB(Listarg') = H.LAB(Form) (S3)
bstack = A(translis(listarg', α))
top = H.TOP(Listarg')+S.NARG(Listarg')=H.TOP(Form) (S6)
list(c(H.TOP(Listarg')+1)..c(H.TOP+S.NARG(Listarg')))= (evlis(listarg', α))

A2
ic = S.LAB(Form) = S.LAB(Listarg) (S4)
bstack = A(transval(form, translis(listarg', α)))
top = H.TOP(Form)+1 = H.TOP(listarg)+ S.NARG(listarg) (S6,S7,S5)
c(top) = I.eval(form, translis(listarg', α))

L'identification est immédiate à l'aide des propriétés suivantes de
evlis et translis :

evlis(append(l₁, l₂), α) = append(evlis(l₁, α), evlis(l₂, translis(l₁, α)))
translis(append(l₁, l₂, α) = translis(l₂, translis(l₁, α))

R27
<Listarg> = empty
Immédiat en assimilant list(H.TOP+1.. H.TOP+0) à I(nil).

R28
<Listexpr> = <Listexpr> S-expr
Immédiat compte tenu de A'₄

R29
<Listexpr> = empty
idem R27

R30

<Listargc> = <Form> <Listarg>
S1 S.CEVAL(Listarg) := S.CEVAL(Form)
                  S.CEVAL(Listargc)
S.LAB(Listargc') : CONS ;
S.LAB(Listargc')+1 : POP 2 ;

L'identification des pré et post-conditions de A4 est immédiate si l'on
suit la séquence A2, A4, CONS, POP. Le résultat obtenu correspond directement
à la définition de evlis et translis.
R31

<Listargc> = empty

S1 S.CEVAL(LListargc) := H.LAB(LListargc) : PUSHQ nil :
Immédiat sachant que I(nil) = nil.

R32

<Listexpr> = S-expr <Listexprc>

L'identification des pré et post-conditions est immédiate si l'on suit
la séquence PUSHQ, A'₄, CONS, POP. Le résultat est direct si l'on note que
cons(S-expr, listexprc') = listexprc

R33

<Listexprc> = empty

Immédiat sachant que I(nil) = nil.