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

laboria

Institut de Recherche
d'Informatique
et d'Automatique

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

laboratoire de recherche
en informatique
et automatique

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

PREUVES DE DESCRIPTIONS
DE TRAITEMENTS DE
TEXTES PAR ATTRIBUTS

C. Pair, M. Amirchahy, D. Néel

Rapport de Recherche N° 163

Mars 1976
PREUVES DE DESCRIPTIONS DE TRAITEMENTS DE TEXTES
PAR ATTRIBUTS

C. Pair, M. Amirchahy, D. Néel
IRIA/LABORIA

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

Résumé :

On indique une méthode de preuves pour la description de traitements de textes par les attributs sémantiques de Knuth. La méthode est appliquée à des exemples intéressant l'optimisation des compilateurs. Elle permet en particulier de prouver des équivalences de descriptions par attributs.

Abstract :

A method is described for proofs of description of text processing by Knuth's semantic attributes.
The method is applied to examples concerning compiler otpimisation. In particular, it is applica-
ble to proofs of equivalence of description by attributes.
## SOMMAIRE

Introduction 1

I - Les attributs sémantiques 2

1 - La notion d'attribut 2

2 - Exemple de description par attributs 4

II - Exemple de preuve d'une description par attributs 9

1 - Attributs logiques et axiomes associés 9

2 - Démonstration par récurrence 11

III - Principe de preuve 13

IV - Autre exemple : Equivalence de deux descriptions par attributs 14

1 - Le problème 14

2 - Description par attributs 15

3 - Assertions à justifier 17

4 - Preuve d'équivalence 18

5 - Preuve de la propriété admise 21

V - La récurrence synthétisée 23

1 - Principe 23

2 - Application 24

3 - Preuve de la propriété admise sur la longueur des suites 25

VI - Conclusion 26
PREUVES DE DESCRIPTIONS DE TRAITEMENTS DE TEXTES

PAR ATTRIBUTS

INTRODUCTION

De nombreuses publications [2], [3], [5] ont montré que
l'utilisation des attributs sémantiques était un excellent moyen pour
décrire certains traitements de textes et en particulier la traduction
des langages de programmation. En effet, si la méthode des attributs
alourdit parfois le processus de compilation, elle lui apporte en
compensation clarté et formalisme : deux qualités non négligeables
surtout quand il s'agit de définir un compilateur que d'autres réali-
seront et d'autres encore utiliseront. Cependant, pour que la méthode
soit satisfaisante, il faut lui associer des techniques de preuves
ce qui n'a pas encore été fait à notre connaissance.

Dans le premier paragraphe nous dirons quelques mots de la
méthode des attributs que nous illustrerons par un exemple tiré de [6],
celui de la détermination d'instructions qui ne sont jamais exécutées
dans un programme.

Le second paragraphe introduit une méthode de preuve des
définitions par attributs, que nous appliquerons à l'exemple précédent.
Nous ferons appel à un raisonnement par récurrence sur lequel est basé
le principe de preuve qui est ensuite précisé au paragraphe III.

Au paragraphe IV nous appliquerons ce principe à un autre
exemple qui démontre l'équivalence de deux descriptions sémantiques,
l'une optimisée et l'autre non, concernant l'élimination de sous-expres-
sions communes redondantes [7].

Avant de conclure, nous traiterons un dernier exemple pour
lequel nous ferons intervenir un cas particulier de la méthode proposée :
la preuve par récurrence synthétisée.
# I - LES ATTRIBUTS SEMANTIQUES

## I - 1 - La notion d'attribut

Elle a été introduite par D.E. KNUTH en 1968 [ 2 ] dans le but de décrire formellement l'aspect sémantique des langages définis par une grammaire "Context-Free".

Un attribut qualifie d'une information "sémantique" un symbole non terminal de la grammaire. Exemple :

Soit N le symbole non terminal qui représente un Nombre ; on peut lui associer les attributs suivants :

$V_N$ = Valeur de ce nombre

$C_N$ = Chaîne de caractères qui représente ce nombre dans une certaine base de numération

$L_N$ = Longueur de cette chaîne

La description d'un langage s'exprime par les relations qui existent entre les attributs des non terminaux de sa grammaire. Ces relations sont regroupées localement au niveau de chaque règle de production. Elles peuvent être considérées comme des définitions, un attribut étant défini par la relation dans laquelle il apparaît à gauche du signe =.

Exemple :

<N> ::= <B>

$V_N = V_B$

<B> ::= 0

$V_B = 0$

<B> ::= 1

$V_B = 1$

<N> ::= <N'> <B>

$V_N = V_{N'} * 2 + V_B$

N.B. On distingue ici par N et N' les deux occurrences du non terminal N, de manière à ne pas confondre les deux valeurs associées, $V_N$ et $V_{N'}$, dans la définition.
Certains attributs sont définis en fonction des attributs de leur "père" dans l'arbre syntaxique, on dit qu'ils ont hérité leur valeur ; d'autres sont calculés à partir des noeuds inférieurs dont ils synthétisent l'information.

Reprenons l'exemple précédent des nombres, supposés écrits en numération binaire, l'attribut C peut être défini par :

<N> ::= <B>
C_N = C_B

<B> ::= 0
C_B = '0'

<B> ::= 1
C_B = '1'

<N> ::= <N'> <B>
C_N = C_N' || C_B' (|| désigne la concatenation)

C est ici un attribut de type synthétisé.

La signification d'une phrase est donnée par le calcul des attributs attachés au non-terminal racine de l'arbre syntaxique.

<figure><img src="image_4.png" /></figure>
La chaîne de caractères qui représente le nombre N est
construite à partir de la concatenation des attributs C des noeuds
inférieurs. C'est elle qui donne la chaîne complète correspondant
à la phrase 101 du langage des nombres binaires. Les définitions
d'attributs permettent de la calculer.

I - 2 - Exemple de description par attributs

Le langage au moyen duquel nous présenterons nos exemples est
défini par les règles suivantes :

<P> ::= <L> ;                      (P : Programme, L : Liste d'instructions)
<L> ::= <I>                        (I : Instruction)
<L> ::= <L> ; <I>

<INE> ::= Etiquette : <INE>        (INE : Instruction Non Etiquetée)
<INE> ::= <INE>

<INE> ::= <V> = <E>                (V : Variable, E : Expression)
<INE> ::= COTO Etiquette

<INE> ::= <ID> ; <L> ; END          (ID : Instruction DO)
<ID> ::= DO <V> = <E> TO <E> BY <E>

<E> ::= <O>                        (O : Opérande)
<E> ::= <E> + <O>
<O> ::= <V>

<O> ::= Constante
<V> ::= Identificateur

Dans les règles de définition des attributs (ou règles
"sémantiques") nous indicerons chacun d'eux par le non terminal auquel
il se rapporte, comme cela a été déjà fait à l'exemple précédent.

Il arrive souvent que deux attributs l'un Hérité, l'autre Synthétisé transportent une information de même nature ; il sera alors commode de les désigner par le même identificateur, respectivement précédé de H. et S. .

Exemple :

Si on traduit les instructions d'un programme en triplets [1],
à chaque instruction I correspond un ou plusieurs triplets.
On utilise deux attributs ayant comme valeurs des numéros de
triplets : celui qui représente le numéro du premier triplet
engendré pour une instruction I est hérité, on le désigne
par H.NT<sub>I</sub>, celui qui porte le numéro du dernier triplet
produit pour I est synthétisé et est désigné par S.NT<sub>I</sub>.
Le problème posé ici est de déterminer dans tout programme
des instructions qui sont inaccessibles à l'exécution, par exemple les
instructions non étiquetées qui suivent un branchement inconditionnel.
Pour le résoudre, nous devons faire intervenir les notions d'étiquette,
de branchement inconditionnel et d'inaccessibilité pour chaque instruc-
tion. Nous définirons les attributs suivants :

ET<sub>I</sub> = 1 si l'instruction I est ETiquetée,
0 sinon.

BI<sub>K</sub> = 1 si la dernière instruction de K est un Branchement Inconditionnel,
0 sinon.

H.IE<sub>K</sub> = 0 si la première instruction de K n'est pas accessible à l'exécution (la première instruction du programme est toujours accessible).

S.IE<sub>K</sub> = 0 si la dernière instruction de K n'est pas accessible à l'exécution.

Description :

<P> ::= <L> ;

H.IE<sub>L</sub> = 1

<L> ::= <I>

BI<sub>L</sub> = BI<sub>I</sub>

H.IE<sub>I</sub> = H.IE<sub>L</sub>

S.IE<sub>L</sub> = S.IE<sub>I</sub>

<L> ::= <L'> ; <I>

BI<sub>L</sub> = BI<sub>I</sub>

H.IE<sub>L</sub> = H.IE<sub>L</sub>

S.IE<sub>L</sub> = S.IE<sub>I</sub>

H.IE<sub>I</sub> = si ET<sub>I</sub>=0 ^ (BI<sub>L</sub>=1 v S.IE<sub>L</sub>=0)
   alors 0
   sinon H.IE<sub>L</sub>

Il s'agit ici de la règle <L> ::= <L> ; <I> dans laquelle, comme nous l'avons déjà dit, on a distingué les deux occurrences de <L> en les notant <L> et <L'> pour pouvoir faire une différence entre les attributs qui leur sont associés.
<I> ::= <INE>

ET<sub>I</sub> = 0

BI<sub>I</sub> = BI<sub>INE</sub>

H.IE<sub>INE</sub> = H.IE<sub>I</sub>

S.IE<sub>I</sub> = S.IE<sub>INE</sub>

<I> ::= Etiquette : <INE>

ET<sub>I</sub> = 1

BI<sub>I</sub> = BI<sub>INE</sub>

H.IE<sub>INE</sub> = H.IE<sub>I</sub>

S.IE<sub>I</sub> = S.IE<sub>INE</sub>

<INE> ::= GOTO Etiquette

BI<sub>INE</sub> = 1

S.IE<sub>INE</sub> = H.IE<sub>INE</sub>

<INE> ::= <V> = <E>

BI<sub>INE</sub> = 0

S.IE<sub>INE</sub> = H.IE<sub>INE</sub>

<INE> ::= <ID> ; <L> ; END

BI<sub>INE</sub> = 0

H.IE<sub>ID</sub> = H.IE<sub>INE</sub>

H.IE<sub>L</sub> = H.IE<sub>INE</sub>

S.IE<sub>INE</sub> = H.IE<sub>INE</sub>

<ID> ::= DO <V> = <E> TO <E> BY <E>

BI<sub>ID</sub> = 0

S.IE<sub>ID</sub> = H.IE<sub>ID</sub>

Les définitions précédentes permettent d'évaluer les attributs en tout noeud de chaque arbre syntaxique engendré par la grammaire. On peut en effet montrer que la description est cohérente [2], c'est-à-dire qu'il existe un ordre d'évaluation où toute valeur d'attribut est calculée après celle dont elle dépend.
Exemple :

GOTO E ;
X = 1 ;
Y = 2 ;
E : ..........

Considérons l'arbre syntaxique de ces trois instructions :

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

Groupons les attributs à évaluer pour chaque non terminal :

L
H. IE_L = 1 , S. IE_L = S. IE_I

L3
H. IE_{L3} = H. IE_{L}, S. IE_{L3} = S. IE_{I3}, BI_{L3} = BI_{I3}

L2
H. IE_{L2} = H. IE_{L3}, S. IE_{L2} = S. IE_{I2}, BI_{L2} = BI_{I2}
L1

H.IE<sub>L1</sub> = H.IE<sub>L2</sub> , S.IE<sub>L1</sub> = S.IE<sub>I1</sub> , BI<sub>L1</sub> = BI<sub>I1</sub>

I1

S.IE<sub>I1</sub> = H.IE<sub>I1</sub> , BI<sub>I1</sub> = 1 , H.IE<sub>I1</sub> = H.IE<sub>L1</sub>

I2

ET<sub>I2</sub> = 0 , S.IE<sub>I2</sub> = H.IE<sub>I2</sub> , BI<sub>I2</sub> = 0 ,

H.IE<sub>I2</sub> = si ET<sub>I2</sub> = 0 ^ (BI<sub>L1</sub> = 1 ^ S.IE<sub>L1</sub> = 0) alors 0 sinon H.IE<sub>L2</sub>

I3

ET<sub>I3</sub> = 0 , S.IE<sub>I3</sub> = H.IE<sub>I3</sub> , BI<sub>I3</sub> = 0 ,

H.IE<sub>I3</sub> = si ET<sub>I3</sub> = 0 ^ (BI<sub>L2</sub> = 1 ^ S.IE<sub>L2</sub> = 0) alors 0 sinon H.IE<sub>L3</sub>

I

ET<sub>I</sub> = 1 , S.IE<sub>I</sub> = H.IE<sub>I</sub> ,

H.IE<sub>I</sub> = si ET<sub>I</sub> ^ (BI<sub>L3</sub> = 1 ^ S.IE<sub>L3</sub> = 0) alors 0 sinon H.IE<sub>L</sub>

Pour pouvoir calculer tous ces attributs, il faut établir un ordre d'évaluation de ces règles sémantiques. Cet ordre peut être déterminé piusque la description est cohérente. Après ordonnancement, on obtient un programme d'évaluation sémantique, par exemple :

H.IE<sub>L</sub> = 1

H.IE<sub>L3</sub> = H.IE<sub>L</sub>

H.IE<sub>L2</sub> = H.IE<sub>L3</sub>

H.IE<sub>L1</sub> = H.IE<sub>L2</sub>

H.IE<sub>I1</sub> = H.IE<sub>L1</sub>

S.IE<sub>I1</sub> = H.IE<sub>I1</sub>

S.IE<sub>L1</sub> = S.IE<sub>I1</sub>

BI<sub>I1</sub> = 1

BI<sub>L1</sub> = BI<sub>I1</sub>

ET<sub>I2</sub> = 0

H.IE<sub>I2</sub> = si ET<sub>I2</sub> = 0 ^ (BI<sub>L1</sub> = 1 ^ S.IE<sub>L1</sub> = 0) alors 0 sinon H.IE<sub>L2</sub>
S.IE<sub>I2</sub>=H.IE<sub>I2</sub>

S.IE<sub>L2</sub>=S.IE<sub>I2</sub>

BI<sub>I2</sub>=0

BI<sub>L2</sub>=BI<sub>I2</sub>

ET<sub>I3</sub>=0

H.IE<sub>I3</sub>= si ET<sub>I3</sub>=0 ^ (BI<sub>L2</sub>=1 v S.IE<sub>L2</sub>=0) alors 0 sinon H.IE<sub>L3</sub>

S.IE<sub>I3</sub>=H.IE<sub>I3</sub>

S.IE<sub>L3</sub>=S.IE<sub>I3</sub>

BI<sub>I3</sub>=0

BI<sub>L3</sub>=BI<sub>I3</sub>

ET<sub>I</sub>=1

H.IE<sub>I</sub>= si ET<sub>I</sub>=0 ^ (BI<sub>L3</sub>=1 v S.IE<sub>L3</sub>=0) alors 0 sinon H.IE<sub>L</sub>

S.IE<sub>I</sub>=H.IE<sub>I</sub>

S.IE<sub>L</sub>=S.IE<sub>I</sub>

On trouvera dans [3] une étude plus précise de l'évaluation des attributs, et en particulier des algorithmes qui déterminent la cohérence d'une description.

## II - EXEMPLE DE PREUVE D'UNE DESCRIPTION PAR ATTRIBUTS

### II - 1 - Attributs logiques et axiomes associés

Nous voulons prouver que la description précédente répond bien au but poursuivi, c'est-à-dire que pour toute liste d'instructions L d'un programme, ainsi que pour tout K (K = I, INE ou ID) on a :

- Si H.IE<sub>L</sub>=0 alors la lère instruction de L n'est pas accessible à l'exécution.

- Si S.IE<sub>L</sub>=0 alors la dernière instruction de L n'est pas accessible.

- Si H.IE<sub>K</sub>=0 alors l'instruction K n'est pas accessible.

- Si S.IE<sub>K</sub>=0 alors l'instruction K n'est pas accessible.

Dans le but de formaliser plus complètement ces assertions, nous allons intraduire la notion d'attribut "logique". Ceci permettra de préciser pour chaque règle syntaxique les axiomes qui nous ont servi intuitivement de base dans la description donnée au chapitre précédent.
Notons PJE<sub>L</sub> le fait que la première instruction de L ne sera jamais exécutée, DJE<sub>L</sub> le fait que la dernière instruction de L ne sera jamais exécutée et IJE<sub>K</sub> le fait que l'instruction K ne sera jamais exécutée. Les propriétés à démontrer s'écrivent alors :

$$
H. IE_L = 0 \Rightarrow PJE_L
$$

$$
S. IE_L = 0 \Rightarrow DJE_L
$$

$$
H. IE_K = 0 \Rightarrow IJE_K
$$

$$
S. IE_K = 0 \Rightarrow IJE_K
$$

Nous dirons que PJE, DJE et IJE sont des attributs logiques. Ils sont définis par des axiomes associés aux règles syntaxiques.

Les assertions à prouver lient donc les attributs "calculés" et les attributs logiques. Les attributs logiques vérifient des axiomes qui peuvent être associés aux diverses règles de production. Indiquons les dans le cas de notre exemple :

$$
\begin{align*}
& <L> ::= <I> \\
& \quad PJE_L \leftrightarrow IJE_I \\
& \quad IJE_I \leftrightarrow DJE_L \\[1em]
& <L> ::= <L'> ; <I> \\
& \quad PJE_L \leftrightarrow PJE_L' \\
& \quad IJE_I \leftrightarrow DJE_L \\
& \quad ET_I = 0 \land BI_{L'} = 1 \Rightarrow IJE_I \\
& \quad ET_I = 0 \land DJE_L' \Rightarrow IJE_I \\
& \quad PJE_L \Rightarrow IJE_I \tag{1}
\end{align*}
$$

$$
\langle I \rangle ::= \langle INE \rangle \\
\qquad IJE_I \rightleftharpoons IJE_{INE}
$$

$$
\langle I \rangle ::= \text{Etiquette : } \langle INE \rangle \\
\qquad IJE_I \rightleftharpoons IJE_{INE}
$$

$$
\begin{align*}
\langle INE \rangle ::= & \langle ID \rangle ; \langle L \rangle ; \text{END} \\
& IJE_{INE} \rightleftharpoons IJE_{ID} \\
& IJE_{INE} \Rightarrow PJE_L \tag{2}
\end{align*}
$$

N.B. Les axiomes (1) et (2) traduisent le fait que, dans la sémantique du langage, il est interdit d'entrer dans une itération depuis l'extérieur.
## II - 2 - Démonstration par récurrence

Il s'agit de démontrer, quel que soit le non terminal K parmi I, INE et ID, que :

$$H.IE_K = 0 \implies IJE_K$$

$$S.IE_K = 0 \implies IJE_K$$

$$H.IE_L = 0 \implies PJE_L$$

$$S.IE_L = 0 \implies DJE_L$$

Nous proposons, pour chaque "règle sémantique" définissant H.IE et S.IE, de démontrer la propriété pour l'attribut de la partie gauche de cette règle en l'admettant pour les attributs figurant en partie droite. Cette méthode se justifie par une récurrence sur l'ordre d'évaluation des attributs. Nous avons dit en effet que la description est **cohérente**, c'est-à-dire qu'il existe un ordre d'évaluation des attributs dans un arbre syntaxique, tel que tout attribut (partie gauche d'une égalité) soit évalué après ceux dont il dépend (c'est-à-dire ceux figurant dans la partie droite de cette égalité). En particulier, le premier attribut évalué ne dépend d'aucun autre : dans notre exemple, ce peut être $H.IE_L$, égal à 1.

On ramène ainsi la justification d'une propriété pour tout noeud de tout arbre syntaxique à un nombre fini de preuves portant sur les symboles non terminaux. Effectuons la démonstration dans le cas de l'exemple en reprenant les diverses règles :

```
< P > ::= < L > ;
```

Comme $H.IE_L=1$, on a bien $H.IE_L=0 \implies PJE_L$.

```
< L > ::= < I >
```

* $H.IE_I=H.IE_L$: On veut montrer que $H.IE_I=0 \implies IJE_I$.
  Par hypothèse de récurrence on a $H.IE_L=0 \implies PJE_L$.
  L'assertion à démontrer résulte alors de l'égalité et de l'axiome
  $PJE_L \iff IJE_I$.

* $S.IE_L=S.IE_I$: On veut montrer que $S.IE_L=0 \implies DJE_L$.
  Par hypothèse on a $S.IE_I=0 \implies IJE_I$.
  L'axiome $IJE_I \iff DJE_L$ nous permet de conclure que $S.IE_L=0 \implies DJE_L$.
<L>::=<L'>;<I>

• H.IE<sub>L</sub>=H.IE<sub>L</sub>: On veut montrer que H.IE<sub>L</sub>=0 = ⇒ PJE<sub>L</sub>.
Par hypothèse on a H.IE<sub>L</sub>=0 = ⇒ PJE<sub>L</sub>.
L'axiome PJE<sub>L</sub>⇔ PJE<sub>L</sub>, permet de démontrer que
H.IE<sub>L</sub>=0 = ⇒ H.IE<sub>L</sub>=0 = ⇒ PJE<sub>L</sub> = ⇒ PJE<sub>L</sub>.

• Démonstration analogue pour S.IE<sub>L</sub>=0 = ⇒ DJE<sub>L</sub>.

• H.IE<sub>I</sub> = IF ET<sub>I</sub>=0 ∧ (BI<sub>L</sub>=1 ∨ S.IE<sub>L</sub>=0) THEN 0 ELSE H.IE<sub>L</sub> :
  **Cas 1 :** ET<sub>I</sub>=0 ∧ BI<sub>L</sub>=1
    On déduit IJE<sub>I</sub> d'après 1'axiome ET<sub>I</sub>=0 ∧ BI<sub>L</sub>=1 = ⇒ IJE<sub>I</sub>.
  **Cas 2 :** ET<sub>I</sub>=0 ∧ S.IE<sub>L</sub>=0
    Par hypothèse on a S.IE<sub>L</sub>=0 = ⇒ DJE<sub>L</sub>.
    L'axiome ET<sub>I</sub>=0 ∧ DJE<sub>L</sub> = ⇒ IJE<sub>I</sub> entraine alors IJE<sub>I</sub>.
  **Cas 3 :** H.IE<sub>I</sub>=H.IE<sub>L</sub>
    Par hypothèse de récurrence, H.IE<sub>L</sub>=0 entraine PJE<sub>L</sub>.
    L'axiome PJE<sub>L</sub> = ⇒ IJE<sub>I</sub> permet de conclure que H.IE<sub>I</sub>=0 = ⇒ IJE<sub>I</sub>.

<I>::=<INE>

• On déduit H.IE<sub>INE</sub>=0 = ⇒ IJE<sub>INE</sub> de la règle sémantique H.IE<sub>INE</sub>=H.IE<sub>I</sub>,
de l'hypothèse de récurrence H.IE<sub>I</sub>=0 = ⇒ IJE<sub>I</sub> et de l'axiome
IJE<sub>I</sub> ⇔ IJE<sub>INE</sub>.

• Démonstration analogue pour S.IE<sub>I</sub>=0 = ⇒ IJE<sub>I</sub>.

<I>::= Etiquette : <INE>

Même démonstration.

<INE>::= GOTO Etiquette

S.IE<sub>INE</sub>=H.IE<sub>INE</sub>: l'hypothèse de récurrence est H.IE<sub>INE</sub>=0 = ⇒ IJE<sub>INE</sub>.

La démonstration est alors résumée par :

S.IE<sub>INE</sub>=0 = ⇒ H.IE<sub>INE</sub>=0 = ⇒ IJE<sub>INE</sub>

<INE>::=<V> =<E>

Même démonstration.

<ID>::= DO <V> = <E> TO <E> BY <E>

Même démonstration.

<INE>::=<ID>;<L>;END

Démonstration analogue.
### III - PRINCIPE DE PREUVE

Résumons et généralisons ce qui vient d'être fait dans le cadre de l'exemple traité au paragraphe précédent. Outre les attributs calculés grâce à la description à prouver, on peut utiliser des attributs logiques vérifiant des axiomes associés aux diverses règles de production. *Chaque assertion à démontrer lie des attributs (calculés et/ou logiques) d'un même symbole non terminal.*

Dans l'exemple, chaque assertion contenait un seul attribut calculé, de sorte qu'on pouvait effectuer une récurrence sur l'ordre d'évaluation de cet attribut. Dans le cas général, une assertion peut contenir plusieurs attributs calculés associés à un même non terminal et il faut donc choisir sur lequel on veut faire la récurrence; on pourrait aussi envisager une récurrence sur l'ordre d'évaluation d'attributs ne figurant pas dans les assertions. Pour préciser cela, à chaque assertion liant les attributs d'un non terminal, on convient d'associer un attribut calculé de ce symbole ; c'est l'ordre d'évaluation des attributs ainsi associés aux assertions qui est l'ordre de récurrence.

Le principe de preuve est alors le suivant :

- Pour chaque règle de production R et pour chaque règle sémantique qui lui est relative : $A_{No}^o = f(A_{N1}^1, ..., A_{Np}^p)$, s'il existe une assertion associée à l'attribut $A^o$ liant les attributs du non terminal No, alors déduire cette assertion à partir :

* des assertions portant sur les non terminaux N1, ..., Np associées aux attributs $A^1, ..., A^p$

* des règles sémantiques et des axiomes relatifs à la règle de production R.

C'est ce principe qui a été appliqué à l'exemple précédent pour les assertions :

H.IE$_L$=0 $\Rightarrow$ PJE$_L$ , associée à l'attribut H.IE$_L$

S.IE$_L$=0 $\Rightarrow$ DJE$_L$ , associée à l'attribut S.IE$_L$

H.IE$_K$=0 $\Rightarrow$ IJE$_K$ , associée à l'attribut H.IE$_K$

S.IE$_K$=0 $\Rightarrow$ IJE$_K$ , associée à l'attribut S.IE$_K$

avec K = I, INE ou ID.
Nous proposons d'appliquer ce principe de preuve à l'équivalence de
deux versions d'une traduction, l'une optimisée et l'autre non. Ceci nous
permettra de conclure que l'optimisation, décrite par attributs, a conservé
la signification. Plus généralement, l'exemple montre comment notre méthode
peut s'appliquer pour prouver une équivalence de descriptions par attributs.

IV - 1 - Le problème

Le problème posé est d'éliminer localement dans un programme les
sous-expressions communes redondantes [7], en appliquant l'algorithme des
"Nombres de Dépendance" au code objet formé de triplets [1], [5]. Chaque
triplet est repéré par un numéro qui est son rang dans la suite des triplets.
Un triplet est formé d'un opérateur binaire et de deux opérandes
qui sont des constantes, des variables ou des numéros de triplets.

A chaque triplet on associe un nombre de dépendance, en utilisant
des nombres de dépendance associés aux opérandes, de la manière suivante :

- le nombre de dépendance d'une constante C est dep(C)=0.

- le nombre de dépendance initial d'une variable A est dep(A)=0.

- si le triplet (i) affecte la valeur de la variable A, alors dep(A)=i à partir du triplet (i+1) jusqu'au prochain triplet affectant A.

- le nombre de dépendance du triplet (n) : opteur, opde1, opde2 est
dep(n) = 1 + MAX( dep(opde1) , dep(opde2) ).

On peut alors montrer le résultat suivant.
Soient deux triplets (i) et (j) ayant même opérateur et même opérandes
(dans un ordre quelconque si l'opérateur est commutatif). Si i<j et
dep(i)=dep(j) alors le triplet (j) est redondant par rapport au triplet (i).

Ce résultat permet d'optimiser la traduction d'un programme source
en triplets en éliminant les triplets redondants. Nous allons définir par
attribut le code objet non optimisé et le code optimisé, et montrer leur
équivalence, ce qui garantira d'une part la validité de l'algorithme d'opti-
misation utilisé (c'est-à-dire le résultat précédent) et d'autre part
l'exactitude de son application.
IV - 2 - Description par attributs

Le programme objet est une suite de triplets. Cette suite est construite
grâce à deux attributs, H.OB et S.OB : l'attribut H.OB<sub>K</sub> donne l'état de la
suite avant le début de la génération associée au non terminal K, et l'attribut
S.OB<sub>K</sub> donne l'état de la suite après la génération associée à K. Pour le
programme optimisé, on utilise les attributs analogues H.OBO et S.OBO qui
ont aussi pour valeurs des suites de triplets. Ces suites sont construites
en cours de compilation et leur longueur dépend du nombre de triplets produits
par les nons terminaux déjà traités. Pour une suite finie s, s(i) désigne
son ième élément et lg(s) sa longueur.

Les nombres de dépendance des opérandes sont portés par les attributs H.ND et S.ND qui ont pour valeurs des fonctions définies sur les repères de constantes et de variables ainsi que sur les entiers utilisés pour numéroter les triplets. Chaque opérande est donc repéré par un attribut : R (et RO pour la suite optimisée) qui donne l'adresse des constantes et variables, et le numéro du dernier triplet des autres expressions.

Nous étudions un langage source défini par la grammaire du paragraphe
I - 2, à l'exception des instructions de branchement, des étiquettes et de
l'instruction de boucle. Donnons les deux descriptions simultanées de la
traduction en triplets : S.OB<sub>p</sub> et S.OBO<sub>p</sub> sont les programmes objets non
optimisé et optimisé pour le programme source P :

<P> ::= <L>;

H.OB<sub>L</sub> = suite vide

S.OB<sub>p</sub>=S.OB<sub>L</sub>

H.OBO<sub>L</sub> = suite vide

S.OBO<sub>p</sub>=S.OBO<sub>L</sub>

H.ND<sub>L</sub> = fonction nulle

<L> ::= <I>

H.OB<sub>I</sub>=H.OB<sub>L</sub>

S.OB<sub>L</sub>=S.OB<sub>I</sub>

H.OBO<sub>I</sub>=H.OBO<sub>L</sub>

S.OBO<sub>L</sub>=S.OBO<sub>I</sub>

H.ND<sub>I</sub>=H.ND<sub>L</sub>

S.ND<sub>L</sub>=S.ND<sub>I</sub>
<L>::=<L';<I>

H.OB<sub>L</sub>=H.OB<sub>L</sub>
H.OB<sub>I</sub>=S.OB<sub>L</sub>,
S.OB<sub>L</sub>=S.OB<sub>I</sub>

H.OBO<sub>L</sub>=H.OBO<sub>L</sub>
H.OBO<sub>I</sub>=S.OBO<sub>L</sub>,
S.OBO<sub>L</sub>=S.OBO<sub>I</sub>
H.ND<sub>L</sub>=H.ND<sub>L</sub>
H.ND<sub>I</sub>=S.ND<sub>L</sub>,
S.ND<sub>L</sub>=S.ND<sub>I</sub>

<I>::=<V>=<E>

H.OB<sub>E</sub>=H.OB<sub>I</sub>
S.OB<sub>I</sub>=S.OB<sub>E</sub> || ' = R<sub>E</sub> R<sub>V</sub>'

H.OBO<sub>E</sub>=H.OBO<sub>I</sub>
S.OBO<sub>I</sub>=S.OBO<sub>E</sub> || ' = RO<sub>E</sub> RO<sub>V</sub>'
H.ND<sub>E</sub>=H.ND<sub>I</sub>
S.ND<sub>I</sub>(x)=S.ND<sub>E</sub>(x) si x≠RO<sub>V</sub> et
S.ND<sub>I</sub>(RO<sub>V</sub>)=lg(S.OBO<sub>E</sub>)+1

N.B. || désigne la concaténation et lg donne la longueur d'une suite de triplets. Nous ne supprimons pas ici les triplets d'affectation redondants : il s'agirait d'un cas particulier de la suppression des affectations inutiles [5].

<E>::=<O>

S.OB<sub>E</sub>=H.OB<sub>E</sub>
R<sub>E</sub>=R<sub>O</sub>

S.OBO<sub>E</sub>=H.OBO<sub>E</sub>
RO<sub>E</sub>=RO<sub>E</sub>
S.ND<sub>E</sub>=H.ND<sub>E</sub>

<E>::=<E'+<O>

H.OB<sub>E</sub>=H.OB<sub>E</sub>
S.OB<sub>E</sub>=S.OB<sub>E</sub>, || '+ R<sub>E</sub>, R<sub>O</sub>'

R<sub>E</sub>=lg(S.OB<sub>E</sub>)+1

H.OBO<sub>E</sub>=H.OBO<sub>E</sub>
S.OBO<sub>E</sub>= RO<sub>E</sub>=lg(S.OBO<sub>E</sub>)+1
alors S.OBO<sub>E</sub>, || '+ RO<sub>E</sub>, RO<sub>O</sub>'
sinon S.OBO<sub>E</sub>'
H.ND<sub>E</sub>=H.ND<sub>E</sub>
S.ND<sub>E</sub>(x)=S.ND<sub>E</sub>,(x) si x≠RO<sub>E</sub> et
S.ND<sub>E</sub>(RO<sub>E</sub>)=d avec
d=1+MAX(S.ND<sub>E</sub>,(RO<sub>E</sub>),S.ND<sub>E</sub>,(RO<sub>O</sub>))
RO<sub>E</sub>=s'il existe i tel que 1≤i≤lg(S.OBO<sub>E</sub>),
^ S.ND<sub>E</sub>,(i)=d
^ ( S.OBO<sub>E</sub>,(i)='+ RO<sub>E</sub>, RO<sub>O</sub>'  ∨
S.OBO<sub>E</sub>,(i)='+ RO<sub>O</sub> RO<sub>E</sub>,')
alors i sinon lg(S.OBO<sub>E</sub>)+1
Pour permettre une démonstration par récurrence, comme nous l'avons envisagée, nous aurons besoin de démontrer une équivalence analogue pour d'autres non terminaux :

(1) $\text{var}(\text{S.OB}_K,x) = \text{var}(\text{S.OBO}_K,x)$ quel que soit $x$, pour $K=P,L,I,E$ il faudra aussi démontrer une assertion analogue pour l'attribut hérité associé :

(2) $\text{var}(\text{H.OB}_K,x) = \text{var}(\text{H.OBO}_K,x)$ quel que soit $x$, pour $K=L,I,E$.

Enfin, nous verrons la nécessité d'assertions concernant les expressions :

(3) $R_E$ numéro de triplet $\Rightarrow R_E=\lg(\text{S.OB}_E)^{\text{RO}_E}$ numéro de triplet de $\text{S.OBO}_E$ $\wedge \text{val}(\text{S.OB}_E)=\text{val}(\text{S.OBO}_E(1:\text{RO}_E))$

(4) $R_K$ repère une constante ou une variable $\Rightarrow R_K=\text{RO}_K$ pour $K=E,O,V$.

On peut associer ces assertions, par exemple, aux attributs respectifs :

$\text{S.OB}_K$, $\text{H.OB}_K$, $\text{S.OB}_E$ et $R_K$. On n'utilise ici aucun attribut logique.

## IV - 4 - La preuve

### $<P> ::= <L>$;

• $\text{H.OB}_L$ suite vide :
on déduit $\text{var}(\text{H.OB}_L,x) = \text{var}(\text{H.OBO}_L,x)$ de $\text{H.OB}_L=\text{H.OBO}_L$=suite vide.

• $\text{S.OB}_P=\text{S.OB}_L$ :
on déduit $\text{var}(\text{S.OB}_P,x) = \text{var}(\text{S.OBO}_P,x)$ des règles sémantiques
$\text{S.OB}_P=\text{S.OB}_L$ et $\text{S.OBO}_P=\text{S.OBO}_L$ ainsi que de l'hypothèse de récurrence
$\text{var}(\text{S.OB}_L,x) = \text{var}(\text{S.OBO}_L,x)$.

### $<L> ::= <I>$

Les assertions à justifier sont du type (2) avec $K=I$ et (1) avec $K=L$, les démonstrations sont immédiates.

### $<L> ::= <L'| ; <I>$

Les assertions à justifier sont du type (2) pour $L'$ et $I$ et (1) pour $L$ ; les démonstrations sont immédiates.

### $<I> ::= <V> = <E>$

• $\text{H.OB}_E=\text{H.OB}_I$ :
L'assertion à justifier est du type (2) avec $K=E$; la démonstration est immédiate.
S.OB<sub>I</sub>=S.OB<sub>E</sub> || ' = R<sub>E</sub> R<sub>V</sub>'

on déduit var(S.OB<sub>I</sub>,x)=var(S.OB<sub>O</sub><sub>I</sub>,x) quel que soit x,

- des règles sémantiques : S.OB<sub>I</sub>=S.OB<sub>E</sub> || ' = R<sub>E</sub> R<sub>V</sub>'
S.OB<sub>O</sub><sub>I</sub>=S.OB<sub>O</sub><sub>E</sub> || ' = R<sub>O</sub><sub>E</sub> R<sub>O</sub><sub>V</sub>'

- de la définition de la fonction var :

var(S.OB<sub>E</sub> || ' = R<sub>E</sub> R<sub>V</sub>', x)=var(S.OB<sub>E</sub>, x) pour x≠R<sub>V</sub>

var(S.OB<sub>E</sub> || ' = R<sub>E</sub> R<sub>V</sub>', R<sub>V</sub>)=var(S.OB<sub>E</sub>, R<sub>E</sub>) si R<sub>E</sub> repère une variable
ou une constante

var(S.OB<sub>E</sub> || ' = R<sub>E</sub> R<sub>V</sub>', R<sub>V</sub>)=val(S.OB<sub>E</sub>(1:R<sub>E</sub>)) si R<sub>E</sub> est un numéro de
triplet

var(S.OB<sub>O</sub><sub>E</sub> || ' = R<sub>O</sub><sub>E</sub> R<sub>O</sub><sub>V</sub>', x)=var(S.OB<sub>O</sub><sub>E</sub>, x) pour x≠R<sub>O</sub><sub>V</sub>

var(S.OB<sub>O</sub><sub>E</sub> || ' = R<sub>O</sub><sub>E</sub> R<sub>O</sub><sub>V</sub>', R<sub>O</sub><sub>V</sub>)=var(S.OB<sub>O</sub><sub>E</sub>, R<sub>O</sub><sub>E</sub>) si R<sub>O</sub><sub>E</sub> repère une variable ou une constante

var(S.OB<sub>O</sub><sub>E</sub> || ' = R<sub>O</sub><sub>E</sub> R<sub>O</sub><sub>V</sub>', R<sub>O</sub><sub>V</sub>)=val(S.OB<sub>O</sub><sub>E</sub>(1:R<sub>O</sub><sub>E</sub>)) si R<sub>O</sub><sub>E</sub> est un numéro de triplet

- des hypothèses de récurrence :

var(S.OB<sub>E</sub>, x)=var(S.OB<sub>O</sub><sub>E</sub>, x) quel que soit x

R<sub>V</sub>=R<sub>O</sub><sub>V</sub>

R<sub>E</sub>=R<sub>O</sub><sub>E</sub> si R<sub>E</sub> repère une variable ou une constante

val(S.OB<sub>E</sub>)=val(S.OB<sub>O</sub><sub>E</sub>(1:R<sub>O</sub><sub>E</sub>)) si R<sub>O</sub><sub>E</sub> est un numéro de triplet

<E>::=<O>

Les assertions à justifier sont du type (1), (3) et (4) pour K=E,
les démonstrations sont immédiates.

<O>::=<V>

Démonstration immédiate pour l'assertion de type (4).

<O>::= Constante

Démonstration immédiate pour l'assertion de type (4).

<V>::= Identificateur

Démonstration immédiate pour l'assertion de type (4).
<E> ::= <E'> + <O>

* Démonstration immédiate pour l'assertion de type (2) avec K=E'.

* L'assertion (1) : var(S.OBE, x)=var(S.OBOE, x) quel que soit x, résulte des règles sémantiques définissant S.OBE et S.OBOE, ainsi que des propriétés de var et de l'hypothèse de récurrence (1) appliquée à E'.

* ROE est un numéro de triplet de S.OBOE et RE=lg(S.OBE) résulte des règles sémantiques.

* Montrons que val(S.OBE)=val(S.OBOE(1:ROE)), en distinguant deux cas selon que RE, repère ou non un numéro de triplet :

- RE est une variable ou une constante
  cas 1 (le triplet créé n'est pas redondant) :
    les règles sémantiques sont S.OBE=S.OBE' || '+ RE, RO' et
    S.OBOE=S.OBOE' || '+ ROE, ROO';
    la définition de val donne :
    val(S.OBE)=var(S.OBE', RE')+var(S.OBE', RO)
    val(S.OBOE)=var(S.OBOE', ROE')+var(S.OBOE', ROO);
    les hypothèses de récurrence conduisent à var(S.OBE', RE')=var(S.OBOE', ROE') et RE'=ROE', ainsi qu'a var(S.OBE', RO)=var(S.OBOE', ROO) et RO=ROO ;
    on en déduit que val(S.OBE)=val(S.OBOE) . de plus on a
    ROE=lg(S.OBOE')+1=lg(S.OBOE), ce qui achève la démonstration.
  cas 2 (le triplet créé est redondant par rapport au triplet ROE=i) :
    les règles sémantiques sont S.OBE=S.OBE' || '+ RE, RO' et
    S.OBOE=S.OBOE';
    la suite S.OBOE(1:ROE) se termine par le triplet (i) qui est '+ ROE, ROO' ou '+ROOROE' ; la définition de val donne :
    val(S.OBE)=var(S.OBE', RE')+var(S.OBE', RO) et
    val(S.OBOE(1:ROE))=var(S.OBOE, (1:ROE-1), ROE')+var(S.OBOE, (1:ROE-1), ROO);
    les hypothèses de récurrence sont les mêmes que dans le cas précédent;
    si on admet (ce qui sera démontré au paragraphe IV-5) que dans S.OBOE', aucun triplet d'affectation à ROE, et ROO n'a un numéro supérieur à RO=i, alors on voit que
    var(S.OBOE, (1:ROE-1), ROE')=var(S.OBOE, , ROE')=var(S.OBE', RE') et
    var(S.OBOE, (1:ROE-1), ROO)=var(S.OBOE, , ROO)=var(S.OBE', RO) ce qui achève la démonstration.
- $R_E$ est un numéro de triplet :

cas 1 (le triplet créé n'est pas redondant) :

les règles sémantiques sont $S.OB_E=S.OB_E, || '+ R_E, R_O' et S.OBO_E=S.OBO_E, || '+ RO_E, RO_O';

la définition de val donne :

$val(S.OB_E)=val(S.OB_E,(1:R_E,))+var(S.OB_E,,R_O)$ et

$val(S.OBO_E)=val(S.OBO_E,(1:RO_E,))+var(S.OBO_E,,RO_O);$

les hypothèses de récurrence conduisent à $val(S.OB_E,(1:R_E,))=val(S.OB_E,)=val(S.OBO_E,(1:RO_E,)), ainsi qu'à $var(S.OB_E,,R_O)=var(S.OBO_E,,RO_O)$ et $R_O=RO_O$ ; on en déduit que $val(S.OB_E)=val(S.OBO_E), de plus on a $RO_E=lg(S.OBO_E,)+1=lg(S.OBO_E),$ ce qui achève la démonstration.

cas 2 (le triplet créé est redondant par rapport au triplet $RO_E=i$) :

les règles sémantiques sont $S.OB_E=S.OB_E, || '+ R_E, R_O' et S.OBO_E=S.OBO_E;$

la suite $S.OBO_E(1:RO_E)$ se termine par le triplet (i) qui est '+ RO_E, RO_O';

la définition de val donne :

$val(S.OB_E)=val(S.OB_E,(1:R_E,))+var(S.OB_E,,R_O)$

$val(S.OBO_E(1:RO_E))=val(S.OBO_E,(1:RO_E,))+var(S.OBO_E,(1:RO_E-1),RO_O);$

les hypothèses de récurrence sont les mêmes que dans le cas précédent;
si on admet (cf. IV - 5) qu'aucune affectation à $RO_O=R_O$ n'est effectuée
par les triplets de $S.OBO_E$, dont les numéros sont supérieurs à $RO_E=i$,
alors on voit que $var(S.OB_E,,R_O)=var(S.OBO_E,(1:RO_E-1),RO_O)$ ce qui
achève la démonstration.

L'assertion (4) est évidente car $R_E$ est un numéro de triplet, donc ne repère ni constante ni variable.

## IV - 5 - Preuve de la propriété admise

Il nous reste à justifier la propriété admise dans la démonstration du paragraphe précédent : dans $S.OBO_E$, aucun triplet d'affectation à $RO_E$, et $RO_O$ n'a un numéro supérieur à $RO_E=i$.

Pour cela, il suffit de montrer les deux propriétés suivantes des nombres de dépendance :

- si $x$ est un numéro de triplet $S.ND_E(x) \le x$

- si $x$ repère une variable ou une constante, $S.ND_E(x)$ est le numéro du dernier triplet d'affectation à $x$ dans $S.OBO_E$, s'il existe et sinon $S.ND_E(x)=0$.
<E>::=<E'>+<O>, on déduit de la première propriété :

$$i \geq S.ND_E, (i)=d>S.ND_E, (RO_E)$$

$$i \geq S.ND_E, (i)=d>S.ND_E, (RO_O) :$$

La dernière affectation à $RO_E$, et $RO_O$, s'il elle existe porte donc un numéro inférieur à i.

Pour effectuer une démonstration par récurrence, nous aurons à prouver des assertions analogues pour $S.ND_I$ et $S.ND_I$, ainsi que pour les attributs hérités associés. Plus précisément, démontrons :

pour $K=L,I,E$ :

(5) (x est un numéro de triplet $\Rightarrow H.ND_K(x) \leq x$)

et (x repère une variable ou une constante $\Rightarrow H.ND_K(x)$ est le numéro du dernier triplet d'affectation à x dans $H.OBO_K$, s'il existe et sinon $H.ND_K(x)=0$).

(6) (x est un numéro de triplet $\Rightarrow S.ND_K(x) \leq x$)

et (x repère une variable ou une constante $\Rightarrow S.ND_K(x)$ est le numéro du dernier triplet d'affectation à x dans $S.OBO_K$, s'il existe et sinon $S.ND_K(x)=0$).

On associe (5) et (6) aux attributs $H.ND_K$ et $S.ND_K$ respectivement. La démonstration est la suivante :

<P>::=<L>;

$H.ND_I$ = fonction nulle : l'assertion (5) est évidente.

<L>::=<I>

• $H.ND_I=H.ND_I$ : on déduit l'assertion (5) pour $K=I$ de la règle sémantique $H.ND_I=H.ND_I$ ainsi que de l'hypothèse de récurrence (5) pour $K=L$.

• $S.ND_I=S.ND_I$ : l'assertion à justifier est du type (6) pour $K=L$, la démonstration est la même que précédemment.

<L>::=<L'>;<I>

Les assertions à justifier sont du type (5) pour $K=L'$ et $I$ , (6) pour $K=L$, les démonstrations sont immédiates.

<I>::=<V>=<E>

• $H.ND_E=H.ND_I$ : L'assertion à justifier est du type (5) pour $K=E$, la démonstration est immédiate.

• $S.ND_I(x)=S.ND_E(x)$ pour $x \neq RO_V$ et $S.ND_I(RO_V)=\lg(S.OBO_E)+1$ : On déduit l'assertion (6) pour $K=I$ et $x \neq RO_V$ de l'hypothèse de récurrence (6) pour $K=E$ ainsi que de la règle sémantique $S.ND_I(x)=S.ND_E(x)$; pour $x=RO_V$ l'assertion est vérifiée car le dernier triplet qui affecte $RO_V$ dans $S.OBO_I=S.OBO_E \parallel ' = RO_E RO_V'$ a pour numéro $\lg(S.OBO_E)+1$.
<E> ::= <0>

L'assertion à vérifier est du type (6) pour K=E, la démonstration est immédiate à partir de l'hypothèse de récurrence (5) var H.OBE.

<E> ::= <E'> + <0>

* H.OBE,=H.OBE : l'assertion à justifier est du type (5) pour K=E' ; la démonstration est immédiate.

* L'assertion à justifier est du type (5) pour K=E', la démonstration est immédiate.

* S.NDE(x)=S.NDE, (x) pour x≠ROE et S.NDE(ROE)=1+MAX(S.NDE', (ROE'), S.NDE, (ROO)) : on déduit l'assertion (6) pour K=E et x≠ROE de l'hypothèse de récurrence sur (6) pour K=E' ainsi que de la règle sémantique S.NDE(x)=S.NDE, (x) ; pour x=ROE, la justification de l'assertion se décompose en deux cas :

cas 1 : ROE=i tel que S.NDE,(i)=d=S.NDE(ROE) :

par hypothèse de récurrence S.NDE,(i)≤i, d'où S.NDE(ROE)≤ROE

cas 2 : ROE=lg(S.OBOE')+1 :

par hypothèse de récurrence S.NDE,(ROO) est nul ou est un numéro de triplet d'affectation de S.OBOE', et S.NDE,(ROE') est inférieur au numéro de triplet ROE, de S.OBOE', ou est nul ou est un triplet d'affectation de S.OBOE' : dans tous les cas, S.NDE(ROE)=d≤1+lg(S.OBOE')=ROE.

La justification des assertions (5) et (6) complète celle des assertions (1), (2), (3) et (4) du paragraphe précédent.

# V - LA RECURRENCE SYNTHETISEE

## V - 1 -Principe

On peut, dans certains cas démontrer des propriétés des attributs en tout point d'un arbre syntaxique, de manière plus simple, en parcourant l'arbre depuis les feuilles vers la racine : il s'agit de prouver que les propriétés sur les fils d'un noeud entrainent les propriétés en ce noeud.

Cette méthode de preuve, qu'on peut appeler récurrence synthétisée, revient à :

pour chaque règle de production R déduire les assertions portant sur le non terminal en partie gauche de R, à partir

- des assertions portant sur les non terminaux figurant en partie droite,

- des règles sémantiques et des axiomes relatifs à R.
Il est facile de voir que la récurrence synthétisée n'est qu'un cas particulier du principe général de preuve donné au paragraphe III. Pour cela, il suffit d'introduire un attribut synthétisé S tel que pour chaque règle de production R :

<NT> ::= <NT1>...<NTn> on ait une définition : S<NT> = f(S<NT1> ... S<NTn>);
on associe alors cet attribut S à chaque assertion à démontrer.

La preuve par récurrence synthétisée ne s'applique pas aux exemples précédents.

## V - 2 - Application

Reprenons l'exemple donné au paragraphe IV. On peut vouloir démontrer, pour s'assurer que la description répond bien à son intention intuitive, que pour toute instruction K on a : H.OB<sub>K</sub>=S.OB<sub>K</sub>(1:lg(H.OB<sub>K</sub>)). Pour justifier ceci, nous utiliserons la méthode de récurrence synthétisée

<P> ::= <L>;

L'assertion à justifier est H.OB<sub>p</sub>=S.OB<sub>p</sub>(1:lg(H.OB<sub>p</sub>)) :
elle est évidente d'après la règle sémantique H.OB<sub>p</sub>=suite vide.

<L> ::= <I>;

On déduit l'égalité H.OB<sub>L</sub>=S.OB<sub>L</sub>(1:lg(H.OB<sub>L</sub>)) :
- des règles sémantiques H.OB<sub>I</sub>=H.OB<sub>L</sub> et S.OB<sub>L</sub>=S.OB<sub>I</sub>,
- de l'hypothèse de récurrence H.OB<sub>I</sub>=S.OB<sub>I</sub>(1:lg(H.OB<sub>I</sub>)).

<L> ::= <L'>;<I>;

La vérification de l'assertion H.OB<sub>L</sub>=S.OB<sub>L</sub>(1:lg(H.OB<sub>L</sub>)) se fait à partir :

- des règles sémantiques H.OB<sub>L</sub>=H.OB<sub>L</sub>, H.OB<sub>I</sub>=S.OB<sub>L</sub>, et S.OB<sub>I</sub>=S.OB<sub>I</sub>,
- des hypothèses de récurrence pour K=L' et I.

Alors :

H.OB<sub>L</sub>=H.OB<sub>L</sub>=S.OB<sub>L</sub>(1:lg(H.OB<sub>L</sub>))
=H.OB<sub>I</sub>(1:lg(H.OB<sub>L</sub>))
=S.OB<sub>I</sub>(1:lg(H.OB<sub>L</sub>))
=S.OB<sub>L</sub>(1:lg(H.OB<sub>L</sub>)).
<I> ::= <V> = <E>

L'assertion à justifier est $H.OB_I=S.OB_I(1:lg(H.OB_I))$ : elle se déduit
- des règles sémantiques $H.OB_E=H.OB_I$ et $S.OB_I=S.OB_E \parallel ' = R_E R_V$,
- de l'hypothèse de récurrence $H.OB_E=S.OB_E(1:lg(H.OB_E)),$

<E> ::= <0>

L'égalité $H.OB_R=S.OB_E(1:lg(H.OB_E))$ résulte immédiatement de la règle sémantique $S.OB_E=H.OB_E$.

<E> ::= <E> + <0>

La justification de l'égalité $H.OB_E=S.OB_E(1:lg(H.OB_E))$ se fait à partir :
- des règles sémantiques $H.OB_E=H.OB_E$ et $S.OB_E=S.OB_E \parallel '+ R_E R_O$,
- de l'hypothèse de récurrence $H.OB_E=S.OB_E(1:lg(H.OB_E))$.

## VI CONCLUSION

Le formalisme des attributs appliqué à la définition d'un traitement de langage semble intéressant dans la mesure où non seulement il lui confère une plus grande clarté, mais encore il offre des facilités pour justifier la description du traitement.

Nous avons vu au paragraphe II comment prouver qu'un attribut rempli bien le rôle qui lui a été assigné. Pour cela, nous avons introduit la notion d'attribut logique dont l'utilisation permet de formaliser les propriétés à démontrer; ces attributs logiques sont précisés par des axiomes associés aux diverses règles syntaxiques.

Une autre application des techniques de preuve est de démontrer l'équivalence de deux descriptions par attributs. On peut ainsi justifier en particulier des optimisations pour des compilateurs décrits par la méthode des attributs. C'est ce que nous avons fait au paragraphe III.

Les méthodes présentées ont l'avantage d'être modulaires car elles découpent la preuve en un certain nombre de démonstrations indépendantes, chacune faisant intervenir les règles sémantiques et les axiomes associés à une règle de production.
REFERENCES

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

[2] D.E. KNUTH
"Semantics of Context-Free Languages".
Mathematical Systems Theory, 2, 2, 1968.

[3] B. LORHO
"De la Définition à la Traduction des Langages de Programmation :
Méthode des Attributs Sémantiques".
Thèse d'Etat, Université Paul Sabatier, Toulouse, 1974

[4] B. LORHO et C. PAIR
"Algorithms for checking consistency of attribute grammars".
Colloque IRIA, 1-3 juillet 1975, Arc et Senans, France

[5] D. NEEL
"Contribution à la Formalisation de l'Amélioration de Code
par Attributs Sémantiques".
Thèse d'Etat, Université de Paris VI, 1975

[6] D. NEEL and M. AMIRCHAHY
"Semantic Attributes and Improvement of Generated Code."
ACM 74, November 11-13, San Diego, California, 1974.

[7] D. NEEL, M. AMIRCHAHY and M. MAZAUD
"Optimization of Generated Code by Means of Attributes : Local
Elimination of Common Redundant Sub-Expressions".
GI 74, October 9-12, Berlin, Germany, 1974.