# Preuve et génération d'attributs sémantiques

Pierre Deransart

► To cite this version:

Pierre Deransart. Preuve et génération d'attributs sémantiques. [Rapport de recherche] IRIA-RR-302, IRIA. 1978, pp.29. hal-04716569

HAL Id: hal-04716569

https://inria.hal.science/hal-04716569v1

Submitted on 1 Oct 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons Attribution 4.0 International License
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

PREUVE ET GÉNÉRATION
D'ATTRIBUTS SÉMANTIQUES

Pierre DERANSART

Rapport de Recherche N° 302

Mai 1978
PREUVE ET GÉNÉRATION D'ATTRIBUTS SÉMANTIQUES

Pierre Deransart

Résumé :

L'objet de ce rapport est de présenter une méthode de génération automatique de certaines définitions d'attributs sémantiques, inspirée d'une technique de preuve.

Les attributs sémantiques ont été introduits par Knuth dans le but de définir une sémantique des langages de programmation déduite de l'arbre de dérivation syntaxique. L'un des principaux domaines d'utilisation des attributs sémantiques est la définition de compilateurs.

L'un des inconvénients de la méthode est le volume des définitions ainsi que les répétitions qu'elles contiennent. Cet article étudie une technique visant à améliorer cette méthode en diminuant ses lourdeurs.

La technique de génération présentée repose sur la méthode de preuve exposée par Amirchahy, Néel et Pair et qui a été utilisée pour prouver des parties de compilateurs écrits avec des attributs. Ce rapport expose quelques exemples où l'on peut envisager d'automatiser tant la preuve que la génération des attributs.

Mots-clés : Attributs sémantiques, sémantique déclarative, constructeurs de compilateur, preuve, génération des attributs, synthèse de programme.

Abstract :

This report presents a method of automatic semantic attributes generation, derived from a proof technique.

The semantic attributes have been introduced by Knuth to define Semantics for programming languages driven by the syntactical tree. The principal use of semantic attributes is compiler definition. One of the drowbacks of the method is the size of the definitions and the repetitions that occure in it. This report describes an approach to improve this technique by decreasing the redundancies of the description.

The generation technique presented derives from the proof method described by Amirchahy, Néel and Pair and used to prove parts of compilers written by attributes.

This report shows some examples which are possible to prove and generate automatically.

Key-words : Semantic attributes, declarativ semantic, compiler-compiler, proof of correctness, program synthesis, attributes generation.
# PREUVE ET CENERATION D'ATTRIBUTS SEMANTIQUES

## Introduction

L'objet de ce rapport est de présenter une méthode de synthèse (1) automatique de certaines définitions d'attributs sémantiques, inspirée d'une technique de preuve.

Les attributs sémantiques ont été introduits par Knuth [Kn 68, 69, 71a,b] dans le but de définir une sémantique des langages de programmation déduite de l'arbre de dérivation syntaxique. De tels systèmes ont été successivement appelés dans la littérature K-système, sémantique déclarative [Fa 72, W 71] et grammaires d'attributs [Bo 76, JP 77] ou, plus simplement, attributs sémantiques [Lo 75, Ne 75]. L'un des domaines principaux d'utilisation des attributs sémantiques est la définition de compilateurs [Fa 72, Lo 75, Bor 75, Bo 76, GRW 77]. Bien que de tels constructeurs imposent en général des limitations importantes aux attributs - le système Delta [Lo 75], est à notre connaissance, le seul fonctionnant sans aucune restriction sur les définitions d'attributs - il s'avère dans la pratique que de tels systèmes comportent un très grand nombre de définitions et de nombreuses redondances. En effet, les définitions d'attributs se limitent souvent à de simples affectations ou reprennent des éléments d'autres définitions dans la même règle. Deux cas se rencontrent fréquemment : les identités, c'est-à-dire que les valeurs d'attributs sont simplement transmises d'un noeud à un autre de l'arbre de dérivation syntaxique ; et l'évolution en parallèle de différents attributs. Le cas des identités est traité assez simplement dans le système Delta (lkeéliorations récentes). Le traitement de l'autre cas et - plus généralement d'autres cas - correspond à la génération de définitions d'attributs.

<footnote>(1) Le terme "synthèse" inspiré de "synthèse de programme" ne sera pas utilisé par la suite afin d'éviter la confusion avec "attribut synthétisé". On utilisera donc le terme "génération".</footnote>
L'idée de faire des preuves dans les grammaires d'attributs est relativement récente [Wi 74, NA 74]. Amirchahy, Néel et Pair ont exposé dans [ANP 77] une technique de preuve par attributs qui découle des preuves par assertions. Cette technique peut servir à des fins diverses : correction des définitions d'attributs, mais il faut ajouter donner une seconde définition du langage source également dérivée de l'arbre d'analyse syntaxique [ANP 76], équivalence de codes générés [NA 74, ANP 76] et preuve de la traduction comme par exemple dans [De 78] où une sémantique (opérationnelle) du code généré est montrée équivalente à une sémantique (également opérationnelle et dérivant de la même syntaxe) du langage source. La technique de preuves doit pouvoir être enrichie par l'apport de travaux plus théoriques tels que [GT 74, CM 77]. Notre idée de génération des définitions d'attributs se fondera sur la technique de preuve telle que décrite dans [ANP 76] et dont nous donnons un rappel dans la section 1.

Preuve et génération d'attributs sont loin de pouvoir être automatisées, tout au moins complètement. Notre propos est de montrer que dans des cas limités, une génération automatique des définitions d'attributs peut être envisagée, en s'inspirant de techniques telles que celles mises en oeuvre par [BD 77] ou [MW 77].

La section 1 constitue un rappel succint de la définition de systèmes d'attributs d'après [Kn 71] et de la technique de preuves telle que décrite dans [ANP 76].

La section 2 expose la technique générale de génération sur un exemple simple, dérivée de la technique de preuve.

La section 3 enfin traite un exemple non trivial de génération - inspiré d'un exemple développé dans [ANP 76] avec l'objectif de montrer l'équivalence de deux codes générés, l'un optimisé, l'autre non dans lequel nous générons une partie des définitions d'attributs conduisant à enendrer directement du code optimisé. Cet exemple relève d'une démarche opposée à celle de la technique générale.
# Section 1 Attributs sémantiques et preuve par attributs, introduction à la génération

Dans [Kn 68, 71] Knuth a proposé de représenter la sémantique d'un langage indépendant du contexte par un système d'équations sémantiques associées aux productions de la grammaire. Ainsi, une description par attributs sémantiques comprend :

a) Une grammaire indépendante du contexte (GCF) définie par le quadruplet $(V_N, V_T, P, A)$ où

- $V_N$ est un ensemble de symboles dits **non terminaux**

- $V_T$ est un ensemble de symboles dits **terminaux** disjoint du précédent.

On note $V = V_N \cup V_T$ le vocabulaire de la GCF.

- P un ensemble de **productions** du type $V_N \to V^*$.

- A un symbole de $V_N$ dit **axiome** de la grammaire.

b) Deux ensembles disjoints d'objets associés à chaque non terminal de G dits ensemble des **attributs hérités** et ensemble des **attributs synthétisés**. On notera $H_X$ et $S_X$ ces deux ensembles associés au non-terminal X et $H_X$, $S_X$ des éléments de l'ensemble des parties de $H_X$ et $S_X$.

A chaque attribut est associé son domaine de valeurs auquel il faut ajouter pour des raisons que nous ne détaillerons pas ici mais signalées dans [Lo 74 et CM 77] un élément **indéfini** dont nous ne parlerons plus par la suite par soucis de simplicité.

c) Un ensemble d'équations sémantiques dits "définitions d'attributs" associé à chaque règle de grammaire correspondant d'une part aux définitions des attributs synthétisés de la racine de la règle en fonction de ses attributs hérités et des attributs synthétisés des non-terminaux de la partie membre droite, d'autre part aux définitions des attributs hérités des non-terminaux de la partie droite en fonction des attributs hérités de la partie gauche et des attributs synthétisés des non-terminaux de la partie droite. Le schéma de la figure 1 résume ces contraintes :
<figure><img src="image_2.png" /><figcaption>**Figure 1.** Illustration des contraintes de définitions d'attributs pour une règle du type $X_0 \to \alpha_1 X_1 \alpha_2 X_2 \alpha_3 X_3 \alpha_4$ où $\alpha_i \in V_T^*$, sur les non-terminaux $X_0$ et $X_2$.</figcaption></figure>

Ces contraintes [CM 77, Wi 74] n'affectent pas la puissance de la description par attribut et sont implicitement admises dans la plupart des applications réelles. Elles ont pour nous l'avantage de simplifier sensiblement l'exposé de la technique de préuve et de génération.

Ainsi à chaque règle de grammaire :

$$X_0 \to \alpha_1 X_1 \alpha_2 X_2 \dots \alpha_k X_k \dots \alpha_n X_n \alpha_{n+1}$$

où $k>0$, $\alpha_k \in V_T^*$, $X_k \in V_N$, est associé le système d'équations :

$$S_{X_0} = F_0 (H_{X_0}, S_{X_1}, S_{X_2}, \dots, S_{X_n})$$

$$H_{X_1} = F_1 (H_{X_0}, S_{X_1}, S_{X_2}, \dots, S_{X_n})$$

......

$$H_{X_n} = F_n (H_{X_0}, S_{X_1}, S_{X_2}, \dots, S_{X_n})$$

où chaque équation résume l'ensemble des définitions concernant les attributs synthétisés (de $X_0$) et les attributs hérités (de $X_k$) et où chaque fonction de $F_0, F_1, \dots, F_n$ dépend de la règle considérée.
Dans le cas d'une règle terminale le système se réduit à la première équation ci-dessus.

L'ensemble des attributs hérités de l'axiome est vide par définition :

$$H_A = \emptyset.$$

L' exemple 1 illustre ces définitions sur une définition simplifiée de Knuth [Kn 68] que nous donnons sous une forme purement synthétisée (l'ensemble des attributs hérités est vide).

$$1. A \to L \qquad v_A = v_L \qquad (1)$$

$$2. A \to L \cdot L \qquad v_A = v_L + v_{L'} + 2 \uparrow - \ell_{L'}$$

$$3. L \to L \cdot B \qquad v_L = 2 * v_{L'} + v_B ; \ell_L = \ell_{L'} + 1$$

$$4. L \to B \qquad v_L = v_B ; \ell_L = 1$$

$$5. B \to 0 \qquad v_B = 0$$

$$6. B \to 1 \qquad v_B = 1$$

**Figure 2.** Exemple 1. GCF et définition d'attributs pour des nombres rationnels binaires positifs ou nuls.

Deux attributs sont utilisés ici : $v$, défini à tous les non-terminaux qui est la valeur de la chaîne terminale de bits dérivée du non-terminal correspondant. La valeur recherchée est évidemment $v_A$ l'attribut synthétisé de l'axiome. Le second attribut est $\ell$, la longueur d'une sous-chaîne de bits à gauche ou à droite du point. Il est défini au seul non-terminal L.

Les domaines de définition de $v$ et $\ell$ sont :

$D_v = \text{Q nombres rationnels positifs ou nuls aux non-terminaux A, L, B et}$

$D = \text{N, entiers naturels, au non-terminal L.}$

Les définitions sémantiques dans le cas de la règle 3 sont de la forme :

$$v_L = f_{\phi v} (v_{L'}, v_b)$$

$$\ell_L = f_{\phi 1} (\ell_{L'})$$

<footnote>(1) L' sert à désigner la deuxième occurrence de L dans la règle.</footnote>
L'idée principale de Knuth [Kn 68], complètement développée dans
[Lo 74, LP 75], a été de définir un algorithme testant la non-circularité
des définitions de telle manière que tous les attributs puissent être
calculés à tous les noeuds où ils sont définis de tout arbre de dérivation,
quelle que soit la phrase analysée. Ainsi, à chaque arbre de dérivation, il
est possible d'associer un ordre d'évaluation des attributs.

C'est cet ordre que Amirchahy, Néel et Pair ont proposé d'utiliser
[ANP 76] afin de réaliser des preuves. La technique est la suivante :

L'objectif de la preuve est de prouver des assertions liant les
attributs d'un même non-terminal. A chaque assertion on associe un attribut
dit *attribut guide*⁽¹⁾. La preuve se fait de la manière suivante :

Pour chaque règle et pour chaque définition portant sur un attribut guide *a* :

$a_{X_o} = f_{\phi a_o} (H_{X_o}, S_{X_1}, ..., S_{X_n})$ si *a* est synthétisé (¥ k tel que $a_{X_k}$ est défini :

$a_{X_k} = f_{ka} (H_{X_o}, S_{X_1}, ..., S_{X_n})$ si *a* est hérité) et sachant que des occurrences
de *a* peuvent apparaître dans les arguments des $f, déduire$ l'assertion associée
à $a_{X_o}$ (respectivement les assertions associées à $a_{X_k}$) à partir :

- des assertions portant sur les non-terminaux $X_i$, oïsïn (respectivement idem) et dont les attributs guides occurrent dans l'équation de définition,

- des définitions d'attributs,

- d'axiomes portant sur les fonctions utilisées dans les définitions et les assertions.

Cette technique utilise la dépendance locale des attributs définis dans
le contexte d'une règle. Elle garantit la stabilité de la relation de
dépendance - et donc l'exactitude de la preuve - quel que soit l'arbre de
dérivation. Par contre rien ne garanti qu'en suivant cette technique l'on
pourra effectivement faire une telle preuve. Il se peut en effet qu'un
nombre insuffisant d'assertions ait un attribut guide occurrant dans une
définition. De plus la réalisation de la preuve peut dépendre du choix de
l'attribut guide - a priori quelconque. Il n'entre pas dans notre propos de
discuter de cette question. On supposera que l'on est capable de choisir un
ensemble d'attributs guides associés à un ensemble d'assertions permettant
de mener à bien une telle preuve.

<footnote>(1) L'attribut guide sera souligné par la suite.</footnote>
La technique présentée ne précise pas non plus la nature des assertions susceptibles de lier les attributs d'un même non-terminal. Il est clair cependant que les attributs peuvent être des fonctions d'un ordre quelconque, définis d'une manière algorithmique sans restriction particulière, que les assertions peuvent avoir un nombre quelconque d'attributs et qu'en conséquence les assertions sont d'un ordre quelconque (au sens de la logique) et que les preuves associées sont particulièrement complexes et loin - a priori - d'être automatisables. Là encore, il ne renferre pas dans cet article de discuter de la nature des assertions susceptibles de lier les attributs d'un même non-terminal, mais on peut noter que deux cas reviennent fréquemment dans les exemples :

1) Une assertion consiste à définir un attribut en fonction d'autres attributs. Par exemple :

$$A_X : a_X = f_X(b_X, c_X)$$

signifie que la valeur de $a_X$ se calcule à partir de celles de $b_X$ et $c_X$ au non-terminal X par la fonction $f_X$.

C'est par exemple le cas où l'on définit le numéro de la dernière instruction générée comme la longueur de la suite correspondant au code généré.

Dans ce cas $A_X$ est une définition d'attribut. Mais il peut se faire que, $f_X$ étant une fonction complexe à calculer, on souhaite utiliser la récursivité des règles de grammaire pour obtenir une définition récursive de $a_X$ en fonction d'autres occurrences de $a$ aux autres non-terminaux ou d'autres attributs. Il s'agit alors de générer une nouvelle définition de $a$.

On peut noter que dans ce cas, $a$ et les autres attributs sont soit hérités, soit synthétisés et que de plus la définition recherchée ne dépend pas des autres attributs (dans le cas contraire, la définition est toute trouvée !). Par contre, les autres attributs ($b$ et/ou $c$ dans cet exemple) peuvent dépendre de $a$. C'est par exemple le cas pour le numéro de dernière instruction du code généré qui sera utilisé pour générer le code lui-même (cf. section 3).

2) Une assertion exprime une relation entre attributs, par exemple :

$$A_X : R_X(a_X, b_X, c_X)$$

où $b_X$, $c_X$ apparaissent comme des variables intermédiaires ou des paramètres pour le calcul de $a_X$.

Les attributs ainsi liés n'ont pas nécessairement la même orientation. L'objectif général d'une description par attributs est d'obtenir la valeur
des attributs synthétisés de l'axiome, privilégiant en quelques sortes le rôle des attributs synthétisés par rapport aux attributs hérités. Le cas le plus fréquent semble donc devoir être celui où $a_X$ est synthétisé et où la relation $R_X$ lie $a_X$ à des attributs hérités (1). Il arrive cependant que le cas contraire se produise - c'est alors normalement pour apporter l'information nécessaire au calcul d'un autre attribut synthétisé - auquel cas $a_X$ est hérité et les autres attributs sont synthétisés.

Il existe ainsi une relation de dépendance entre $a_X$ et les autres attributs ($b_X$, $c_X$). Ce cas apparaît comme opposé au précédent où la relation de dépendance, si elle existait, était nécessairement inverse.

Une illustration de ce cas est celui où un attribut synthétisé se déduit d'un attribut hérité, par exemple : $s_X = f_X(h_X)$ et où $f_X$ étant une fonction complexe, on souhaite remplacer ce calcul par une suite de pas de calculs déduits de la récursivité des règles. Le but de la génération est donc cette fois, dans la mesure du possible, de retarder l'apparition de h dans la définition de s.

Il est cependant certain, qu'à un moment ou à un autre, h interviendra dans cette définition (règle terminale).

En général cependant, comme les attributs n'ont pas la même orientation et comme $a_X$ dépend des autres, l'objectif de la génération est soit de rechercher la définition de $a_X$ connaissant celle de $h_X$ et $c_X$, soit de rechercher celles de $b_X$ et $c_X$ - ou de l'un d'entre eux - connaissant celle de $a_X$. Si donc on cherche à générer $a_X$, le but de la génération est de retarder l'apparition des éléments dont il dépend et si l'on cherche à générer $h_X$ en $c_X$, le but est de trouver une définition sans $a_X$.

On voit ainsi que l'idée de la génération est qu'étant donnée une définition ou une relation - que nous appellerons spécification - liant les attributs d'un même non terminal, il doit être possible de remplacer cette spécification par des définitions liant les occurrences de ces attributs à des non-terminaux différents d'une même règle, faisant intervenir moins d'attributs - en tous cas pas ceux qui dépendent d'eux - et utilisant la récursivité induite par les règles.

Une telle définition n'utilise plus nécessairement les mêmes attributs que la spécification mais conserve les dépendances contenues dans celle-ci.

<footnote>(1) Notons qu'il pourrait y avoir plusieurs attributs synthétisés dépendant des hérités et intervenant dans l'assertion.</footnote>
Par la suite, chaque assertion sera écrite dans un langage de spécifications d'attributs que nous définirons au fur et à mesure de son utilisation. Ce langage inclut comme on l'a vu le langage de définition d'attributs.

## Section 2 Preuve et génération : technique générale

Il semble que dans les deux cas exposés précédemment la technique de génération, bien que découlant du même principe, doive-t-être sensiblement différente. Dans le premier cas en effet on connaît la définition d'un attribut par une fonction $f_X$ et la définition recherchée correspond au calcul partiel de cette fonction dans le contexte de chaque règle. Des techniques particulières reposant sur l'évaluation partielle des fonctions peuvent alors être employées. Le second cas est plus général. Les définitions cherchées doivent être obtenues à partir des spécifications sans que l'on dispose d'autres informations que des contraintes sur les occurrences d'attributs susceptibles d'y figurer. Il s'agit alors de trouver une hypothèse manquante liant ces occurrences, permettant d'achever la preuve et dont on puisse extraire une définition.

Cette section expose sur un exemple simple la technique générale.

Nous noterons $A_{a_x}$ où $A_{a,x}$ une assertion attachée au non terminal $v$, liant les attributs $v_i$ y sont définis et ayant a comme attribut guide.

La définition de l'attribut guide a est une équation :

$$ a_x = f(b_1, ..., b_i, 1 \le i \le n) \text{ où } b_i \text{ est le i-ème attribut} $$

intervenant dans la définition de $a$.

La preuve consiste donc à prouver $A_{a_x}$ à l'aide des assertions attachées aux non-terminaux dont les attributs guide occurrent dans la définition de $a_x$ soit :

$$ A_i \quad A_{b_i} \text{, où tel que } \left\{ \begin{array}{l} - \text{bi attribut guide} \\ - \text{bi occurre dans la définition } A_{a_x} \end{array} \right. \Rightarrow A_{a_x} $$

La technique consiste à remplacer dans les expressions de $A_{b_i}$ et $A_{a,x}$ les occurrences des attributs synthétisés de la partie gauche et des attributs hérités des non-terminaux de la partie droite par leur définition. On obtient alors de part et d'autre de l'implication deux expressions contenant les mêmes variables ; à savoir des occurrences des attributs hérités de la racine de la règle et des occurrences des attributs synthétisés des non-terminaux de la partie droite.
Il reste à prouver l'implication, c'est-à-dire que la formule obtenue est une tautologie.

La génération consiste à rechercher les définitions manquantes qui permettent d'établir l'implication.

En effet, dans ce cas, l'opération de remplacement des occurrences d'attributs définis dans une règle par leur définition ne peut se faire complètement. L'expression obtenue après remplacement comporte donc des occurrences des attributs dont on cherche la définition à différents non-terminaux. Les définitions recherchées apparaissent alors comme des hypothèses manquantes consistant en des relations liant les occurrences des attributs définis et éventuellement d'autres attributs. De ces hypothèses restituées, on tente d'extraire les définitions sous la forme d'égalités avec comme membre gauche l'occurrence d'un attribut défini et en partie droite des occurrences des autres attributs, hérités de la racine ou synthétisés des non-terminaux de partie droite, sauf de ceux que l'on veut éliminer.

Un problème apparaît cependant : on ignore a priori le nombre d'assertions que l'on est en droit d'utiliser pour prouver l'implication puisque l'on ne connaît pas a priori les attributs guides qui vont apparaître dans la définition. Ce problème est limité si l'on évite de rechercher les définitions d'attributs servant d'attribut guide. Cette restriction ne semble pas devoir limiter les possibilités de génération, dans la mesure où les attributs guides sont en général ceux à partir desquels sont bâties les assertions et par là même les plus complexes donc les moins susceptibles d'être générés.

L'exemple 2 qui suit illustre cette démarche.

On considère un langage, tel Algol 68, dont la grammaire possède une règle du type LI → LI I où LI est une liste d'instructions et I une instruction quelconque (éventuellement étiquetée) ou une déclaration de mode.

Pour compiler chaque instruction, on a besoin de connaître l'ensemble des déclarations de mode qui interviennent dans l'ensemble des instructions d'un bloc contenant cette liste d'instructions. On introduit donc deux attributs :

* ms : l'ensemble des modes synthétisés à partir de chaque déclaration,

* mh : l'ensemble de tous les modes déclarés dans le bloc, hérité à toutes les instructions.
On associe donc à la règle LI → LI I les équations sémantiques suivantes :

$$ms_{LI} = \text{union}(ms_{LI'}, ms_{I})$$

$$mh_{LI'} = mh_{LI}$$

$$mh_{I} = mh_{LI}$$

La figure 2 schématise les dépendances existant entre ces attributs dans cette règle :

<figure><img src="image_3.png" /><figcaption>Figure 2. dépendances des attributs ms et mh</figcaption></figure>

mh et ms sont définis aux mêmes non-terminaux. Il existe également une règle du type Bloc → LI où mh est initialisé par l'équation : mh$_{LI}$ = ms$_{LI}$'.

On veut alors prouver l'assertion

$A_{mh,N}$ : $ms_N \subseteq mh_N$ pour N = LI, I qui traduit que mh contient tous les modes déclarés dans la liste d'instructions qui contient I et celles de LI.

On a le choix de l'attribut guide, mais compte-tenu du fait que mh est défini à partir de ms, et que nous chercherons une définition de ms, nous choisissons mh comme attribut guide.

La preuve s'écrit donc :

$$A_{mh,LI} \Rightarrow A_{mh,LI'} \quad (a)$$

$$A_{mh,LI} \Rightarrow A_{mh,I} \quad (b)$$

Preuve de (a) : on remplace $ms_{LI}$ à gauche par sa définition et $mh_{LI'}$ à droite également, (a) devient :
$$ \text{union}(\text{ms}_{LI'}, \text{ms}_I) \subseteq \text{mh}_{LI} \Rightarrow \text{ms}_{LI'} \subseteq \text{mh}_{LI} $$

L'implication est immédiate, vu les propriétés de l'inclusion. La démonstration pour (b) est identique.

Pour la génération de ms, la même technique de remplacement, impossible bien sûr en ce qui concerne ms, conduit à :

$$ \text{ms}_{LI} \subseteq \text{mh}_{LI} \Rightarrow \text{ms}_{LI'} \subseteq \text{mh}_{LI} \quad (a') $$

$$ \text{ms}_{LI} \subseteq \text{mh}_{LI} \Rightarrow \text{ms}_{I} \subseteq \text{mh}_{LI} \quad (b') $$

Considérant l'expression (a'), l'hypothèse manquante s'obtient à partir de l'axiome de transitivité de l'inclusion, soit :

$$ \text{ms}_{LI'} \subseteq \text{ms}_{LI} \quad (a'') $$

de (b') on extrait une hypothèse analogue

$$ \text{ms}_I \subseteq \text{ms}_{LI} \quad (b'') $$

Si l'on n'utilisait que (a') ou (b'), la génération fournirait une définition erronée car on ne pourrait obtenir qu'une identité. Il est nécessaire en fait d'utiliser à la fois (a') et (b') pour générer la définition de ms car la preuve issue de l'attribut guide h comporte les deux assertions (a) et (b).

(a'') et (b'') sont équivalents à :

$$ \text{union}(\text{ms}_{LI'}, \text{ms}_I) \subseteq \text{ms}_{LI} $$

Une définition est donc :

$$ \text{ms}_{LI} = \text{union}(\text{ms}_{LI'}, \text{ms}_I) $$

Il existe en fait une infinité de solutions dues au fait que la propriété donnée est trop lâche pour donner une seule solution. Il est possible de préciser la nature de mh et ms par plusieurs assertions, mais nous avons voulu nous limiter à une propriété simple afin de mieux mettre en évidence le mécanisme de génération dans le cas général.

## Section 3 : Exemple de génération (code optimisé).

La méthode générale, illustrée précédemment, consiste à générer des définitions d'attributs en cherchant à reconstituer une preuve qui partant des équations sémantiques retrouve les assertions. Cette démarche est analogue à celle des preuves de programme.

Le cas examiné ici correspond au cas où l'assertion est une définition d'attribut, c'est-à-dire que par exemple

$$ a_X = f_X(b_X) $$
où $a_X$ est l'attribut défini, $b_X$ le (ou les) attribut(s) servant à la définition et $f_X$ une fonction dépendant de la règle et du non-terminal considéré.

Ce que l'on recherche est une nouvelle définition de $a_X$ sans occurrence de $b_X$ (mais éventuellement avec des occurrences de $a$ à d'autres non-terminaux) et qui ne remette pas en cause la cohérence des définitions. Ce dernier point sera laissé de coté ici ; rappelons seulement que $a_X$ et le (ou les) $b_X$ sont ensemble synthétisés ou hérités. Dans ce cas la démarche est inverse de la méthode générale. En effet, on est en mesure de déduire logiquement la définition cherchée des assertions. Les assertions étant données comme vraies (on peut alors utiliser toutes celles dont on a besoin), la définition s'obtient en transformant le membre droit de la première définition. Ces transformations doivent viser à simplifier celui-ci, en termes de calculs tout au moins, ce qui revient en général à faire apparaître des occurrences de l'attribut défini ($a_X$) à d'autres non-terminaux.

L'exemple traité ici porte sur un langage simple constitué d'affectations et d'expressions limitées à la somme d'un nombre quelconque de variables. L'intérêt de ce langage est de refléter en la simplifiant une situation courante dans les langages de programmation et de mettre en évidence le cas d'optimisation que nous voulons traiter, à savoir l'élimination des triplets redondants. Nous donnons en annexe 1 un bref rappel de l'algorithme classique d'optimisation du code généré.

### Grammaire :

1. $A = L.$ (Notations [Wir 77])

2. $L = L";"I.$

3. $L = I.$

4. $I = \text{Ident":

5. $E = \text{Ident.}$

6. $E = E"+"\text{Ident.}$

### Attribut type

(1)

$\uparrow\downarrow C_N$ suite de triplets correspondant à : (2)
pour $\downarrow C$ : Code généré de la chaîne terminale précédant $N$
$\uparrow C$ : idem mais en incluant $N$

attributs définis aux nt : $L,I,E$ pour $\uparrow C_N$, idem plus $P$ pour $\uparrow C_N$.

<footnote>(1) les flèches indiquent : $\uparrow$ synthétisé, $\downarrow$ : hérité, $\uparrow\downarrow$ deux attributs l'un hérité l'autre synthétisé.</footnote>

<footnote>(2) Le code généré ne comprend que des triplets d'affectation (= a b) où a est une variable, b une variable ou un triplet, et des triplets d'addition (+ b a).</footnote>
↑↑nt<sub>N</sub> entier nombre de triplets de ↑↑C<sub>N</sub>, définis aux mêmes non-terminaux.

↑x<sub>N</sub> XUT où X est l'ensemble des variables des programmes et T
l'ensemble des mémoires auxiliaires.

↑x_N n'est défini que pour une expression (N=E) et représente le nom de la variable ou le numéro de triplet (variable auxiliaire) contenant la valeur de l'expression.

↑↑nd<sub>N</sub> XUT→N nombre de dépendance des variables ou des triplets +, défini aux mêmes non-terminaux que ↑↑C.

Nota : on associe à chaque triplet + une variable auxiliaire représentée par le numéro de ce triplet dans le code généré.
Définitions d'attributs

L'ensemble des définitions est donné en annexe 2. La règle 6 étant la
plus complexe nous nous contenterons de traiter preuve et génération dans le
cadre de cette règle que nous donnons ci-dessous.

6. E = E"+"Ident (cf. explications sur les notations plus bas)

$$
\begin{align*}
+ C'_{E'} = + C_{E'} \quad & \uparrow C_{E'} = \underline{\text{si Cond}} \\
& \underline{\text{alors}} \quad \uparrow C'_{E'} \\
& \underline{\text{sinon}} \quad \uparrow C'_{E'} \\
& \quad [\uparrow \text{nt}_{E',+1}] + \uparrow x_{E'} \text{Ident} \\
& \underline{\text{fsi}}
\end{align*}
$$

$$
\begin{align*}
*+nt'_{E'} = -nt_{E'} \quad & *+nt_{E'} = \underline{\text{si Cond}} \\
& \underline{\text{alors}} \quad \uparrow nt'_{E'} \\
& \underline{\text{sinon}} \quad [\uparrow nt'_{E'} + 1] \\
& \underline{\text{fsi}}
\end{align*}
$$

$$
\begin{align*}
*+nd_{E'} = -nd_{E'} \quad & *+nd_{E'} = \underline{\text{si Cond}} \\
& \underline{\text{alors}} \quad \uparrow nd_{E'} \\
& \underline{\text{sinon}} \quad (\lambda x. \ \underline{\text{if}} \ x = [\uparrow nt_{E'} + 1] \\
& \qquad \underline{\text{then}} \ 1+\max(\uparrow nd_{E'} \ \uparrow x_{E'} \ \uparrow nd_{E'} \ \text{Ident}) \\
& \qquad \underline{\text{else}} \ \uparrow nd_{E'} \ x \ \underline{\text{fi}} \ \underline{\text{fsi}} \\
& \underline{\text{↑}x_{E'}} = \underline{\text{si Cond}} \\
& \underline{\text{alors}} \quad i \\
& \underline{\text{sinon}} \quad [\uparrow nt_{E'} + 1] \\
& \underline{\text{fsi}}
\end{align*}
$$

(1)

$$
\begin{align*}
\text{où Cond s'écrit} \\
& [(\exists i)(i < [\uparrow \text{nt}_E', +1] \land i. \uparrow C_E' = ' + \uparrow x_E', \text{Ident}') \\
& \qquad \land 1+\max(\uparrow \text{nd}_E', \uparrow x_E', \uparrow \text{nd}_E', \text{Ident}) = \uparrow \text{nd}_E', i)]
\end{align*}
$$

Cette condition exprime qu'il existe un triplet déjà généré dans $\uparrow C_E'$

<footnote>(1) L'écriture de Cond dans chacune des définitions n'est évidemment pas élégante ni efficace. L'optimisation qui consisterait à introduire une seule fois le test et un test plus simple dans les autres définitions mais avec un attribut de synchronisation (cf Lo 74) ne rentre pas dans le cadre de cet article.</footnote>
de rang i (opération 'point' de sélection du ième élément dans la suite) de
la forme "+ +x<sub>E</sub>, Ident" (semblable à celui que l'on devrait générer) et
ayant le même numéro de dépendance que celui que l'on devrait générer.

Pour bien comprendre ces notations, il faut distinguer ce qui dénote
le calcul d'attributs (langage de définitions sémantiques - LDS) de ce qui
dénote la valeur finale d'un attribut. Ainsi la structure de contrôle _si_
<u>alors sinon fsi</u> fait partie du LDS alors que _if then else fii_ intervient
dans la valeur finale de nd. La syntaxe informelle du LDS que nous utilisons
est la suivante :

<Définition> = attribut "=" <Expression LDS>,

<E LDS> = "si" <E LDS> "alors" <E LDS> "sinon" <E LDS> "fsi"
<E LDS> = Attribut | "["Calcul de valeur"]".

Ainsi, outre les opérations utilisées pour décrire le calcul des attributs
(1'ajout d'un triplet en fin de code est implicite ainsi que la construction
de chaîne), le LDS ne comporte comme mots clés que si .. fsi et les crochets. (1)
Le reste représente le calcul des valeurs d'attributs.

Enfin, pour ne pas alourdir l'écriture, l'argument d'une fonction à
un seul argument est noté sans parenthèses.

Ainsi : nd<sub>E</sub>, x<sub>E</sub>, représente nd<sub>E</sub>, appliquée à x<sub>E</sub>.

Dans cet exemple deux attributs ont une définition qui se déduit du
code généré. Ce sont ↑↑nt et ↑↑nd. Compte-tenu du fait que ↑↑nd, ↑↑nt et ↑↑C
evoluent parallèlement, nous négligerons par la suite, dans la mesure
où il n'y a pas ambiguïté, de noter les flèches. Nous traiterons donc
successivement les preuves et génération de nt puis de nd.

3.1 Génération de nt.

La définition de nt est donnée par l'assertion :

$A_{C,N} : nt_N = lg(C_N)$ pour N = P,L,I,F

où lg(C) correspond à la longueur de la suite C,i.e. au nombre de triplets
de C. La définition de nt<sub>E</sub> est donc donnée par A<sub>C,F</sub>.

On remplace c<sub>E</sub> par sa définition qui, comportant une conditionnelle,
introduit deux cas :

<footnote>(1) Ceux-ci sont omis s'il n'y a pas ambiguïté.</footnote>
$$ \text{Cond} \wedge \text{nt}_E = \lg(C_E) $$

non $\text{Cond} \wedge \text{nt}_E = [\lg(C_E) + 1]$ après transformation.

Sachant que $A_{C,E'}$ est vérifiée au non-terminal $E'$, soit que $\text{nt}_{E'} = \lg(C_{E'})$, on obtient la nouvelle définition par cas :

$$ \text{Cond} \wedge \text{nt}_E = \text{nt}_{E'} $$

non $\text{Cond} \wedge \text{nt}_E = [\text{nt}_E, +1]$

Il reste à reconstruire une définition d'attributs à partir des deux clauses. Cette reconstruction est semblable à la reconstruction par cas décrite par Manna et Waldinger [MW 77] : pour obtenir la définition :

$$ \text{nt}_E = \underline{\text{si Cond alors } \text{nt}_E, \text{sinon } [\text{nt}_E, +1] \text{ fsi}} $$

où $\text{Cond}$ ne fait intervenir que des attributs synthétisés du non-terminal $E'$.

### 3.2. Génération de nd

$nd_E$ est défini à partir de $C_E$ par la propriété :

$$ A_{C,E}^1 : \text{nd}_E X = $$

$$ x \in X_E \rightarrow \max k \underline{ds} \quad \{k / k. C_E = ' = x u'\} ; $$

$$ x \in T_E \rightarrow \underline{\text{soit}} a,b \underline{\text{tq}} x \cdot C_E = ' + ab' \underline{\text{ds}} $$

$$ 1+\max(\text{nd}_E a, \text{nd}_E b) ; $$

$$ \underline{\text{sinon}} 0 $$

Dans cette notation qui fait partie du langage de spécification d'attributs la flèche dénote une conditionnelle, "$\max$ i $ds$ N ;" dénote le maximum de i dans l'ensemble N d'entiers et "$\underline{soit}$ $v_1$, $v_2$, ..., $v_n$ $\underline{\text{tq}}$ $P(v_1$, $v_2$, ..., $v_n$) $\underline{\text{ds}}$ expression ;" dénote un bloc d'affectation où $P(v_1$, $v_2$, ..., $v_n$) définit les valeurs de $v_1$, $v_2$, ..., $v_n$ qui sont reportées dans l'expression. Le résultat du "$\underline{soit}...;$" est la valeur de l'expression ainsi calculée.

La définition de $\text{nd}_E$ est donc récursive et du type :

$$ x \in D_1 \rightarrow f_1 x $$

$$ x \in D_2 \rightarrow f_2 x $$

$$ \underline{\text{sinon}} f_3 x $$

$A_{C,E}$ fait intervenir deux attributs "fantômes" $X_E$ et $T_E$ que l'on définit par les propriétés $A^2$ et $A^3$ :

$$ A_{C,E}^2 : X_E = \{x / k. C_E = ' = x u'\} $$

$$ A_{C,E}^3 : T_E = \{k / k. C_E = '+ ab'\} $$
$X_E$ est donc l'ensemble des variables ayant été affectées au moins une fois dans $C_E$, et $T_E$ l'ensemble des rangs des triplets addition dans $C_E$.

Notons que $X$ et $T$ sont des attributs qui "suivent" $C$, ainsi que nd.

Il n'y a donc pas de problème de définition de l'assertion puisque quand $C_E$ est vide, $X$ et $T$ sont vides et nd (d'après $A^1$) est réduite à la fonction constante nulle (*)

On opérera en deux temps : génération de $X$ et $T$ puis de nd.

### 3.2.1. Génération de $X$ et $T$ :

Pour $X$ c'est évident puisqu'il n'y a que des identités (tout au moins pour la règle 6).

Pour $T$, la définition de $T_E$ correspond à :

$$A_{C,E}^3 : T_E = \{k/k. C_E = '+ab\}$$

Remplaçant $C_E$ par sa définition et utilisant les propriétés de l'opérateur de sélection "." sur les suites ainsi que celles des propriétés caractéristiques des ensembles, qui sont :

$$P(k.C_1C_2) = P(k.C_1) \lor P(k.c_2)$$

$$\{x/P_1(x) \lor P_2(x)\} = \{x/P_1(x)\} \cup \{x/P_2(x)\}$$

on obtient, toujours en opérant par cas :

$$\text{Cond} \land T_E = T_E'$$

$$\text{non } \text{Cond} \land T_E = T_F, \text{ u } \{ \text{nt}_E, +1 \}$$

Les définitions reconstruites sont donc :

$$X_E = X_E'$$

$$T_E = \text{si } \text{Cond } \text{alors } T_E, \text{ sinon } T_F, \text{ u } \{[\text{nt}_E, +1]\} \text{ fsi}$$

<footnote>(*) qui peut s'écrire $(\lambda x.o)$</footnote>
### 3.2.2. Génération de nd à partir de $A_{C,E}^1$

nd est une application de l'ensemble $X_E \cup T_E \circ VNA_E^{(1)}$ dans les entiers.

Des règles comme $E = E^+ + E^-$ Ident. ou $I = \text{Ident}^- := \text{Ident}^+$ ont pour but d'exprimer des extentions du domaine de nd. Il est légitime dans ce cas de considérer que si dans l'expression d'une valeur nouvelle, apparaissent des occurrences du nouvel attribut mais avec des paramètres dont la valeur n'appartiennent pas à l'extension du domaine, alors on peut substituer ces occurrences par celles de l'ancien attribut.

Nous exprimerons ceci par un axiome "d'extension du domaine" :

$$ 
\begin{array}{l@{\qquad}l}
\text{sif } x = x \in D_1 \rightarrow f_1 x & \\
\phantom{\text{sif }} x \in D_2 \rightarrow f_2 x & D_2 \cap D_1 = \emptyset, D_2 \text{ extension} \\
\text{i.e. } x \in D_2 \rightarrow fx = f'x &
\end{array}
$$

et que dans $f_1 x$ et $f_2 x$ apparaissent des occurrences $fy$, alors on peut remplacer ces occurrences par $f'y$, à condition toutefois que $y \notin D_2^{(2)}$.

Cet axiome découle du fait que la valeur obtenue pour un tel attribut est la réalisation d'une fonction définie récursivement (à partir d'une grammaire récursive) $f'$ apparaît comme une fonction moins définie (sur $D_1$) que $f$ (sur $D_1 \cup D_2$) et l'on cherche une définition de $f$ en fonction de $f'$ à partir d'une définition récursive de $f$ pour laquelle on montre que ses occurrences intervenant dans sa définition ont des paramètres définis sur $D_1$ et non sur le domaine étendu ($D_1 \cup D_2$).

Deux cas se présentent (Cond et non Cond) qui entraineront une reconstruction. Le premier cas est évident (Identité), le second conduit à l'expression suivante :

$$ 
\begin{array}{l}
\text{non Cond} \wedge \text{nd}_E x = \\
\phantom{\text{non Cond} \wedge \text{nd}_E x =} x \in X_E \rightarrow \underset{\underline{\hspace{2.5cm}}}{\max} k \ ds \ \{k/k.C_E, [nt_E, +1] + x_E, \text{Ident} = ' = x \ u\} ; \\
\phantom{\text{non Cond} \wedge \text{nd}_E x =} x \in T_E \cup \{[nt_E, +1]\} \rightarrow \underset{\underline{\hspace{2.5cm}}}{\text{soit}} a, b \ \underline{\hspace{1cm}} x. \ C_E, [nt_E, +1] + x_E, \text{Ident} = ' + ab \\
\phantom{\text{non Cond} \wedge \text{nd}_E x =} \qquad \underline{\hspace{1cm}} 1 + \max(\text{nd}_E a, \text{nd}_E b) ; \\
\phantom{\text{non Cond} \wedge \text{nd}_E x =} \text{sinon } 0.
\end{array}
$$

<footnote>(1) VNA : ensemble de variables non affectées.</footnote>

<footnote>(2) En fait l'axiome traduit l'hypothèse que si la variable n'appartient pas à l'extension du domaine, elle appartient à l'ancien domaine.</footnote>
Il faut examiner alors ensemble par ensemble :

$x \in X_E$ : il y a identité qui conduit à $nd_E x = nd_E x = nd_E, x$

$x \in T_E$ : conduit à

soit $a, b : x \cdot C_E, [nt_E, +1] + x_E, \text{Ident} = ' + a b$

$\underline{ds} 1 + \max(\underline{nd}_E a, \underline{nd}_E b)$ ;

si $x \in T_E$, on peut montrer, que le sélecteur $x$ ne

prend jamais la valeur $[nt_E, +1]$ et que par suite l'expression s'écrit :

soit $a, b : x \cdot C_E, = ' + a b \underline{ds} 1 + \max(\underline{nd}_E a, \underline{nd}_E b)$ ;

faisant alors jouer l'axiome d'extension, on peut substituer $nd_E, a$ et $\underline{nd}_E, b$ à $nd_E, a$ et $nd_E, b$ puisque $a$ et $b$ sont différents de $[nt_E, +1]$.

Il reste à traiter le cas :

$x \in ([nt_E, +1])$ qui conduit, après simplification de soit, à :

$$1 + \max(\underline{nd}_E x_E', \underline{nd}_E \text{Ident})$$

comme il s'agit du cas d'extension du domaine, on peut substituer les occurrences de $nd_E$ par $nd_E$, à condition de montrer que

(a) $x_E' \neq [nt_E, +1]$ et (b) $\text{Ident} \neq [nt_E' + 1]$.

(a) se vérifie du fait que si $x_E' \in T_E$, $x_E'$ est inférieur ou égal à $nt_E'$, par contre si $x_E' \in X_E'$, ($x_E'$ est une variable) il ne peut être un nombre. Il en est de même pour $\text{Ident}$ qui est une variable.

Reconstruisant le résultat par cas, on obtient l'expression finale :

$nd_E = \underline{si} \ \underline{Cond} \ \underline{alors} \ nd_E,$

$\underline{sinon} \ (\lambda x, \underline{if} \ x = [nt_E, +1] \ \underline{then} \ 1 + \max(\underline{nd}_E x_E', \underline{nd}_E \text{Ident}) \ \underline{else} \ \underline{nd}_E, x \ \underline{fi}) \ \underline{fsi}$
## Conclusion.

La technique de preuve par attributs telles que décrite par [ANP 76]. nous a permis d'établir une méthode pour générer certaines définitions d'attributs.

Cette méthode relève des techniques de synthèse de programmes inspirées des techniques de preuve de programmes. Logiquement on ne devrait pas pouvoir espérer traiter ainsi de gros systèmes d'attributs. Ce qui tempère cette impression et le contexte dans lequel les définitions d'attributs doivent être générées. Très guidée par les règles de grammaire, la génération dans de nombreux cas non triviaux devrait être possible. De plus, le cas examiné (section 3) - qui se rencontre fréquemment au niveau de la génération du code - relève de techniques de transformations de programmes qui permettent de traiter des programmes plus importants [BD 77].

Toutes ces techniques sont au moins partiellement automatisables. On devrait pouvoir espérer d'une telle démarche une simplification sensible de la définition de compilateurs par attributs sémantiques. Une telle approche rejoint celle des langages de programmation où de plus en plus de place est réservée aux déclarations des objets que l'on va manipuler. Ainsi une définition par attribut sémantique se réduirait aux équations définissant les attributs essentiels et ferait une plus large place aux spécifications d'attributs déduite des premiers.

Il va de soi que ceci nécessite de mettre au point d'une part un langage de spécification d'attributs et d'autre part, un langage sémantique dans lequel les preuves puissent être facilement étudiées et par suite la génération se faire.

Notons enfin que plusieurs aspects n'ont pas été développés ici le type des assertions, l'introduction d'axiomes supplémentaire, le rôle des dépendances entre attributs et leur respect lors des générations, le choix des assertions pour retrouver une preuve. Toutes ces questions doivent être précisées pour pouvoir traiter effectivement la méthode générale d'une manière automatique.

## Remerciements.

Je tiens à remercier M.C. Gaudel et G. Terrine et tout particulièrement C. Pair qui ont permis les fructueuses discussions aux cours desquelles ces développements ont pu apparaître.
# ANNEXE 1 Génération de code optimisé pour un langage simple.

## Rappel de l'algorithme de Gries.

$$ 
\begin{array}{l}
\textbf{Exemple :} \\
D = D + C * B \\
A = D + C * B \\
C = D + C * B \\
A = C
\end{array}
 $$

Pour chaque triplet et variable, on calcule un numéro de dépendance :

$$ \text{nd}(+ a b) = 1 + \max(\text{nd}(a), \text{nd}(b)) $$

$$ \text{nd}(x) = \text{si } x \text{ non affectée alors } \text{nd}(x) = 0 $$

$$ \begin{array}{l} \text{sinon } \text{nd}(x) = \text{numéro du triplet de la dernière affectation} \\ \text{(dernier triplet "= x b)} \end{array} $$

**Exemple ci-dessus :**

<table><thead><tr><th>Code non optimisé</th><th>Code optimisé :</th></tr></thead><tbody><tr><td>(1) * C B nd(1) = 1 nd(C)=0, nd(B)=0</td><td>(1) * C B</td></tr><tr><td>(2) + D(1) 2 nd(D)=0</td><td>(2) + D(1)</td></tr><tr><td>(3) = D(2) 3 nd(D)=3</td><td>(3) = D(2)</td></tr><tr><td>(4) * C B 1</td><td></td></tr><tr><td>(5) + D(4) 4</td><td>(4) + D(1)</td></tr><tr><td>(6) = A(5) 5 nd(A)=6</td><td>(5) = A(4)</td></tr><tr><td>(7) * C B 1</td><td></td></tr><tr><td>(8) + D(7) 4</td><td></td></tr><tr><td>(9) = C(8) 5 nd(C)=9</td><td>(6) = C(4)</td></tr><tr><td>(10) = A C 10</td><td>(7) = A C</td></tr></tbody></table>

**Optimisation :**

Si deux triplets sont égaux et ont leurs numéros de dépendance égaux le dernier est redondant. Il peut être supprimé. La définition d'attributs vise à générer du code optimisé.
# ANNEXE 2

## Description des attributs (exemple de la section 3)

1. A = L.

$$ 
\begin{array}{l@{\hspace{2em}}c@{\hspace{2em}}l@{\hspace{2em}}c@{\hspace{2em}}l}
\downarrow C_L & = & \text{suitevide} & \uparrow C_A & = & \uparrow C_L \\
* \downarrow nt(L) & = & 0 & * \uparrow nt_A & = & \uparrow nt_L^* \\
* \downarrow nd(L) & = & (\lambda x.O)
\end{array}
$$

2. L = L";"I

$$ 
\begin{array}{l@{\hspace{2em}}c@{\hspace{2em}}l@{\hspace{2em}}c@{\hspace{2em}}l}
\downarrow C_L' & = & \downarrow C_L & \uparrow C_L & = & \uparrow C_L \\
\downarrow C_I & = & \uparrow C_L' & & & \\
* \downarrow nt_L' & = & \downarrow nt_L & * \uparrow nt_L & = & \uparrow nt_L \\
* \downarrow nt_I & = & \uparrow nt_L' & & & \\
* \downarrow nd_L' & = & \downarrow nd_L & * \uparrow nd_I & = & \uparrow nd_I \\
* \downarrow nd_I & = & \uparrow nd_L' & & & \\
\end{array}
$$

3. L = I.

$$ 
\begin{array}{l@{\hspace{2em}}c@{\hspace{2em}}l@{\hspace{2em}}c@{\hspace{2em}}l}
\downarrow C_I & = & \downarrow C_L & \uparrow C_L & = & \uparrow C_I \\
* \downarrow nt_I & = & \downarrow nt_L & * \uparrow nt_L & = & \uparrow nt_I \\
* \downarrow nd_I & = & \downarrow nd_L & * \uparrow nd_L & = & \uparrow nd_I \\
\end{array}
$$

4. I = Ident ":"E.

$$ 
\begin{array}{l@{\hspace{2em}}c@{\hspace{2em}}l@{\hspace{2em}}c@{\hspace{2em}}l}
\downarrow C_E & = & \downarrow C_I & \uparrow C_I & = & \uparrow C_E \\
* \downarrow nt_E & = & \downarrow nt_I & * \uparrow nt_I & = & \uparrow nt_E + 1 \\
* \downarrow nd_E & = & \downarrow nd_I & * \uparrow nd_I & = & (\lambda x. \text{if } x = \text{Ident} \\
& & & & & \text{then } \uparrow nt_E + 1 \\
& & & & & \text{else } \uparrow nd_E x \text{ fsi})
\end{array}
$$

5. E = Ident.

$$ 
\begin{array}{l@{\hspace{2em}}c@{\hspace{2em}}l@{\hspace{2em}}c@{\hspace{2em}}l}
\uparrow x_E & = & \text{Ident} & \uparrow C_E & = & \downarrow C_E \\
* \uparrow nt_E & = & \downarrow nt_E & * \uparrow nt_E & = & \downarrow nt_E \\
* \uparrow nd_E & = & \downarrow nd_E & * \uparrow nd_E & = & \downarrow nd_E
\end{array}
$$

6. E = E"+"Ident.

Les définitions sémantiques sont données dans le texte (section 3).

**Nota** : les flèches $\uparrow\downarrow$ correspondent aux attributs synthétisés en hérités. L'astérisque indique les définitions générées.
BIBLIOGRAPHIE

[ANP 76] C. PAIR, M. AMIRCHAHY, D. NEEL, "Preuve de descriptions de traitements de textes par attributs. Rapport de recherche n° 163. Mars 1976. 25 p.

[BD 77] R.M. BURSTALL, J. DARLINGTON, "A transformation system for developing recursive programs". JACM. V 24 - N1 - pp 44.67, 1977.

[BM 75] R.J. BOYER, J.S. MOORE, "Proving Theorems about Lisp functions", JACM, V22, N1, pp. 129.144, 1975.

[Bo 74] G.V. BOCHMANN "Attribute grammars and compilation : program evaluation in several phases". Document de travail. Département d'Informatique. U. de Montréal. Août 1974.

[Bo 76] G.V. BOCHMANN "Semantic evaluation form left to right", CACM 19(2), pp. 55.62, Fev. 1972.

[Bor 75] J. BOROWIEC, "Programatics in a compiler producing system", Institute of Mathematical Machine. PERA. Warsaw, July 1975.

[CM 77] L.M. CHIRICA, D.F. MARTIN. "An algebraic formulation of Knuthian Semantics". University of California, Los Angeles. CSD, 1977.

[De 77] P. DERANSART "Proof by semantic attributes of a Lisp compiler". Second Hungarian Computer Science Conference. Budapest 77. June 27 July 2. 1977.

[De 78] P. DERANSART, "Technique de preuve par attributs appliquée à un compilateur LISP". Rapport de recherche n° 271. IRIA LABORIA, Janv. 1978.

[Fa 72] I. FANG, "FOLDS, a declarative Formal Language Definition System", CSD Stanfort Univ., Palo Alto, California, STAN - CS - 329 - Decem. 1972.

[G. 71] D. GRIES. Compiler Constructions for Digital Computers. John Wiley & Sons, Inc, New York 1971.

[GRW 76] H. GANZINGER, K. RIPKEN, R. WILHELM, "MUG 1 - An incremental compiler - compiler", Proceedings of the ACM Annual conference, Houston, Texas Octob, 1976, pp 415-418.

[GRW 77] H. GANZINGER, K. RIPKEN, R. WILHELM, "Automatic Generation of optimizing multipass compilers", Information processing 77, B. GILCHRIST Editor, IFIP, North - Holland publishing Company, 1977.
[GT 74] J.A. GOGUEN, J.W. THATCHER, "Initial algebra semantics",
Proceedings of the 15th IEEE Symposium in Switching and Automata
Theory, Nou. Orleans, Louisiana, October 1974, IEEE, New York,
pp. 63.77, 1974.

[GTWW 75] J.A. GOGUEN, J.W. THATCHER, E.G. WAGNER et J.B. WRIGHT,
"Initial algebra semantics and continuous algebras", IBM Thomas
J. Wakson Research Center, Yorktown Heights, New York, RC 5243,
Nov. 1975.

[JP 77] M. JAZAYERI, D. POZEFSKY, "Algorithms for efficient evaluation of
multi-pass attribute grammars without a parse-tree", DCS, Univ. of
North. Carolina, Chapel Hill, TR 77-001, Fev. 1977.

[Kn 68] D.E. KNUTH "Semantics of Context Free Languages", Mathematical System
Theory, 2,2,1968.

[Kn 69] D.E. KNUTH, "The art of computer programming, V1, Addison Wesley Pub.
Company, 1969.

[Kn 71a] D.E. KNUTH "Semantics of Context Free Languages".
Corrigenda-Mathematical System Theory 5, pp. 95.96, 1971.

[Kn 71b] D.E. KNUTH "Examples of formal semantics" lectures Notes in Maths.
N° 188. Springer-Verlag, Berlin 1971, pp 212-235.

[Ko 74] C.H.A. KOSTER "Using the CDL compiler compiler" in : F.L. Bauer and
J.Eickel eds. Compiler construction - an advanced course, lectures Notes
in Computer Science, V21, Springer Verlag, pp. 366.426, 1974.

[LB 74] D. LECARME and G.V. BOCHMANN, "A (touly) usable and portable compiler
writing system, Information Processing, pp. 218.221, 1974.

[Lo 74] B. LORHO "De la définition à la traduction des langages de programmation :
méthode des attributs sémantiques". Thèse d'Etat. Univ. Paul Sabatier,
Toulouse, 1974.

[LP 75] B. LORHO, C. PAIR, "Algorithms for checking the consistency of
attribute grammars. Colloque IRIA, 1.3 Juillet 75, Arc et Senans,
France.

[MW 77] Z. MANNA, R. WALDINGER, "The automatic synthesis of recursive
programs". CACM 1977.

[NA 74] D. NEEL, M. AMIRCHAHY, "Semantic attribute and Improvement of
Generated Code". ACM 74. Nov. 11.13 San Diego, California 1974.
[NAM 74] D. NEEL, M. AMIRCHAHY, M. MAZAUD,
"Optimization of Generated Code by Means of attributes : local
elimination of commun redondant syb-expressions". GI 74. Octobre 9.12.
Berlin, Germany, 1974.

[Ne 75] D. NEEL "Contribution à la formalisation de l'amélioration de code par attributs sémantiques". Thèse d'Etat, Univ. de Paris 6. 1975.

[W 71] Wilner W.T., "Declarative Semantic Definition", CSD, Stanford Univ, Palo Alto, California, STAN-CS 233-71, 1971.

[W 72] Wilner W.T., "Formal Semantic Definition Using Synthesized and
inherited Attributes", Proceedings of Courant Institute Computer
Science Symposium, NY Sept. 70, Prentice Hall, Eglewood Cliffs,
New Jersey, 1972, Vol 2, pp. 25.39.

[Wi 75] R. WILHELM, "Code optimierung mittels attributierter transformations
grammatiken", Lecture notes in Computer Sciences 26, Springer,
pp. 257.266, 1975.

[Wir 77] N. WIRTH, "What can we do about the unnecessary diversity of
notation for syntactic definitions?" CACM - Nov. 77, V20, N11.
PREUVE ET GENERATION D'ATTRIBUTS SEMANTIQUES

Communication n° 190 proposée au Congrès AFCET 78.

Auteur : Pierre DERANSART

IRIA - LABORIA

Domaine de Voluceau - Rocquencourt

BP 105

78150 LE CHESNAY