# Specifications incomplètes mais suffisantes de la représentation des types abstraits

Marie-Claude Gaudel

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

## To cite this version:

Marie-Claude Gaudel. Specifications incomplètes mais suffisantes de la représentation des types abstraits. [Rapport de recherche] IRIA-RR-320, IRIA. 1978, pp.18. hal-04716522

HAL Id: hal-04716522

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

Submitted on 1 Oct 2024

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published 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_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
RIA
laboria

laboratoire de recherche
en informatique
et automatique

ARCHIVES

SPÉCIFICATIONS INCOMPLÈTES
MAIS SUFFISANTES
DE LA REPRÉSENTATION
DES TYPES ABSTRAITS

Marie Claude GAUDEL

Rapport de Recherche N° 320

Août 1978

Institut de Recherche
d'Informatique
et d'Automatique

Domaine de Voluceau
Rocquencourt
B. P. 105 78150 - Le Chesnay
France
Tél.: 954 90 20
SPECIFICATIONS INCOMPLETES MAIS SUFFISANTES DE LA REPRESENTATION
DES TYPES ABSTRAITS

Marie Claude GAUDEL

RESUME :

On se place dans la cadre de la specification algébrique des types abstraits et on montre que la
représentation d'un tel type est caractérisée par la représentation d'un sous-ensemble de ses opéra-
tions (les constructeurs) et celle de l'égalité. A partir de ces hypothèses et des axioms des types
abstraits utilisés on peut retrouver la représentation de toutes les opérations. Une méthodologie
est dégagée et un exemple est complètement traité.

ABSTRACT :

Correctness of data representation can be proved in the framework of algebraic specifications of
abstract data type. This paper presents how to build systematically such representations from
incomplete but sufficient specifications.

From the representation of :

- a subset of the operations of the type to be implemented (the constructors),

- the equality relation defined by the axioms,

it is possible to get a representation for every operation of the type. An example is given and
completed.
# INTRODUCTION

Ce papier présente une réflexion sur la représentation des types de données. Nous avons été amenés à nous intéresser à ce problème dans le cadre de la traduction des langages de programmation [DEN 75, GAU 77], mais il s'avère que nos constations et les méthodologies qui en découlent rejoint des problèmes de programmation généraux.

Pour spécifier un type de données nous utilisons une définition algébrique [GUTT 76a] que certains auteurs qualifient d'équationelle [GOG 76]. Les notations sont à peu de choses près celles utilisées par Guttag.

**Exemple 1** : Le type tableau, paramétré par le type des indices et celui des valeurs, est défini de la manière suivante :

**type Tableau** [ ? Indice, ? Valeur ] :

**Opérations**

Tabvide : → Tableau ;

accès : (Tableau, Indice) → Valeur u { UNDEF } ;

assign : (Tableau, Indice, Valeur) → Tableau ;

**Axions**

pourtout t ∈ Tableau, i,j ∈ Indice, v ∈ Valeur. soit

(T1) accès (tabvide, i) = UNDEF ;

(T2) accès (assign (t,i,v),j) = si i = j alors v sinon accès (t,j) ;

fin Tableau ;

Etant donné de telles définitions pour un type "source" et des types "objets", on peut spécifier formellement une représentation du premier par les seconds et démontrer si cette spécification est correcte ou non : encore faut-il préciser ce qu'on entend par une spécification de représentation correcte et quelles sont ses propriétés. D'autre part, de telles représentations présentent un intérêt dans la mesure où les nouvelles expressions se prêtent plus simplement à la génération d'instructions opérationnelles que les anciennes.

Le problème abordé ici est le suivant : à partir des définitions du type source et des types objets et des propriétés connues des "bonnes" représentations comment trouver la spécification d'une telle représentation, et est-ce possible automatiquement ? de quelles données a-t-on besoin pour
caractériser une représentation et pouvoir en déduire une description complète de celle-ci ?

Dans l'état actuel de ce travail nous ne prétendons pas être exhaus tifs et notre démarche reste passablement empirique : nous nous contenterons de mettre en évidence un certain nombre de règles intéressantes.

# I - Propriétés d'une représentation correcte.

**Exemple 2** : Soit le type "File d'attente" paramétré par le type des valeurs contenues dans la file ;

**type File [? Valeur] :**

**opérations.**

* filevide : →File ;
* ajouter : (File, Valeur) → File ;
* enlever : (File) → File ;
* premier : (File) → Valeur u{UNDEF} ;

**axiomes.**

* pourtout f ∈ File, v ∈ Valeur soit
  (F1) enlever (filevide) = filevide ;
  (F2) enlever (ajouter (f,v)) = si f = filevide alors filevide sinon ajouter (enlever(f),v) ;
  (F3) premier (filevide) = UNDEF ;
  (F4) premier (ajouter (f,v)) = si f = filevide alors v sinon premier (f) fin File ;

Une représentation classique des files est un triplet formé d'un tableau, de l'indice dans ce tableau du premier élément de la file et de l'indice du premier élément libre après la file. Pour simplifier l'exemple le nombre d'éléments de la file et la dimension du tableau ne sont pas bornés. Le type des indices est défini par :
**Exemple 3 :**

Type Ent ;
opérations
zéro : → Ent ;
succ : (Ent) → Ent ;
fin Ent ;

Le type des valeurs n'est pas précisé.

Pour définir la représentation, on va se donner une fonction d'abs-traction $\mathcal{N}^b$ [HOA 72] de profil :

Tableau [Ent, ? Valeur] x Ent x Ent → File [? Valeur]

et la représentation de toute expression de type File :

**Exemple 4 :**

pourtout $t \in$ Tableau, $i, j \in$ Ent, $v \in$ Valeur soit

(R1) filevide = $\mathcal{N}^b(t,i,i)$ ;

(R2) ajouter ($\mathcal{N}^b(t,i,j),v$) = $\mathcal{N}^b(\text{assign}(t,j,v), i, \text{succ}(j))$ ;

(R3) enlever ($\mathcal{N}^b(t,i,i)$) = $\mathcal{N}^b(t,i,i)$ ;

(R4) enlever ($\mathcal{N}^b(t,i,j)$) = $\mathcal{N}^b(t,\text{succ}(i),j)$ ;

(R5) premier ($\mathcal{N}^b(t,i,i)$) = UNDEF ;

(R6) premier ($\mathcal{N}^b(t,i,j)$) = accès $(t,i)$ ;

fin ;

On va examiner d'une manière intuitive en quoi consiste cette défi-
nition et quelles sont les règles qui doivent être respectées pour qu'on ait
ainsi spécifié une représentation correcte.

Appelons A l'ensemble des objets (1) sources et C l'ensemble des
objets objets.

(1) Un objet d'un type abstrait est une entité qui peut être dénotée par une ou plusieurs expressions du type abstrait. Plus formellement, si on considère l'égalité induite par les axiomes sur l'ensemble de ces expressions un objet est une classe d'équivalence de cet ensemble.
<figure><img src="image_3.png" /></figure>

$\tilde{\mathcal{J}}$ doit être surjective : tous les objets sources doivent être représentés. Mais elle n'est pas forcément injective : un objet source peut avoir plusieurs représentations (c'est le cas de filevide) ; d'autre part, $\tilde{\mathcal{J}}$ n'est pas nécessairement définie sur tout le domaine concret.

Guttag dans [GUTT 76b] appelle "invariant de représentation" les propriétés qui caractérisent le domaine de définition de $\tilde{\mathcal{J}}$. Dans l'exemple des files, si $(t,i,j) \in \tilde{\mathcal{J}}^{t-1}$ (A) on a :
$$ |i| \le |j| \qquad (1) $$

et

$\forall k, \text{ tel que } |i| \le |k| < |j|, \text{ accès } (t,k) \ne \text{UNDEF}$

Il appelle "interprétation de l'égalité" la relation de ce domaine définie par :

$$ c \rightleftharpoons \tilde{\mathcal{J}}(c) = \tilde{\mathcal{J}}(c') $$

Par exemple, $\forall t, t' \in \text{Tableau}, \forall i, j \in \text{Ent}$ on a

$$ (t,i,i) = (t',j,j). $$

Si on considère maintenant non plus C, mais l'ensemble des classes d'équivalence de $\tilde{\mathcal{J}}^{t-1}$ (A) définies par cette relation, $\tilde{\mathcal{J}}$ est une bijection de cet ensemble dans A. La fonction inverse de $\tilde{\mathcal{J}}$ est la fonction de re-

(1) si i est une formule de type Ent, on note $|i|$ le nombre d'opérateurs que comporte cette formule :

$$ |\text{zéro}| = 1 $$

$$ |\text{succ}(i)| = |i| + 1 $$

On voit que $|i| - 1$ est la valeur de i, au sens familier du terme.
présentation proprement dite ; dans le cas où le type source a une structure libre, c'est-à-dire quand chaque formule définit un objet différent (cf. Exemple 3), on n'a pas ces problèmes d'interprétation de l'égalité et on peut se donner directement $\mathcal{A} \not\vdash \Omega$. On trouvera un exemple intéressant dans [BUR 77].

Pour que la représentation définie par $\mathcal{A}$ soit correcte, il faut non seulement qu'elle soit surjective, mais aussi que les propriétés du type source se retrouvent dans le domaine objet : les axiomes doivent être conservés par la représentation.

Soit $c \in \mathcal{A}^{-1}(A)$. Dans l'exemple 4 on a défini pour toute fonction fa du type source, une composition de fonctions du type objet, $fc$ qui vérifie :

$$fa(\mathcal{A}(c)) = \mathcal{A}(fc(c))$$

si fa est à résultat dans A (c'est le cas pour ajouter, enlever, filevide) et sinon

$$fa(\mathcal{A}(c)) = fc(c)$$

(ce qui est le cas pour premier).

Cela revient à se donner un homomorphisme. Cet homomorphisme doit conserver les axiomes, c'est-à-dire que tout axiome du type source doit devenir un théorème dans $\mathcal{A}^{-1}(A) / \simeq$, théorème démontrable à partir des axiomes du type objet, des invariants de représentation, et de l'interprétation de l'égalité.

On peut par exemple montrer que l'axiome (F4) est conservé par la représentation de l'exemple 4 ; rappelons l'axiome (F4) :

$$\begin{array}{l} \text{premier (ajouter } (f,v)) = \underline{\text{si }} f = \text{filevide } \underline{\text{alors }} v \\ \qquad \underline{\text{sinon premier }} (f); \end{array}$$

Dans le premier cas, on a $f = \text{filevide}$ :

$$\text{premier (ajouter (filevide), v)) =}$$
d'après (R1) :
premier (ajouter ($\hat{c}_b(t,i,i),v$)) =

d'après (R2) :
premier (assign ($t,i,v$), i, succ (i))) =

d'après (R6) :
accès (assign($t,i,v$), i) =

d'après (T2)
v c.q.f.d.

Dans le deuxième cas, f est quelconque, différent de filevide :
premier (ajouter ($\hat{c}_b(t,i,j), v$)) =

d'après (R2) :
premier (assign ($t,j,v$), i, succ (j))) =

d'après (R6) =
accès (assign ($t,j,v$), i) =

d'après (T2) et les invariants de représentation

accès ($t,i$) =

d'après (R6) (1)
premier ($\hat{c}_b(t,i,j)$) = premier (f) c.q.f.d.

Les démonstrations de ce genre ne sont pas très difficiles mais assez longues. Elles sont automatisables comme il a été montré dans [GUT 76b]

## II - Spécifications incomplètes (mais suffisantes) de représentations

Le caractère systématique et répétitif de ces démonstrations de correction amène à penser qu'il est possible, à partir de la représentation d'un sous-ensemble des opérations, de déduire la représentation complète systématiquement, voire même automatiquement. Cela semble une démarche plus constructive que de faire une preuve longue et coûteuse, "à postériori". D'ailleurs intuitivement, il semble raisonnable d'utiliser le fait qu'une fois qu'on a donné - disons la représentation de l'adjonction dans une table

<footnote>(1) Ici (R6) a été utilisée de droite à gauche. C'est ce que Burstall et Darlington appellent un "folding" par opposition aux "unfoldings" qui ont précédé.</footnote>
- on a implicitement donné la représentation de la recherche dans cette table ; du moins a-t-on considérablement restreint les représentations acceptables pour cette recherche.

Un premier problème est le choix des éléments à donner pour avoir une "sous-spécification suffisante". Pour cela, il est bon de se rappeler les caractéristiques de la fonction $\mathcal{F}$ étudiée au paragraphe précédent.

$\mathcal{F}$ doit être surjective : il est donc nécessaire que les opérations dont on donne la représentation permettent d'engendrer tous les objets sources. D'où l'intérêt de la notion de "constructeurs" d'un type abstrait que nous allons préciser.

## II - 1 Forme normale - Constructeurs.

Reprenons l'exemple des Files. On a le théorème suivant :
**Théorème :** Pour tout f de type File [? Valeur], on a :

f = filevide ou f = ajouter (fl,v)
avec fl ∈ File [? Valeur] et v ∈ ? Valeur.

La démonstration est élémentaire et se fait par induction struc-
turelle, en utilisant les axiomes du type File. On déduit de ce théorème que
toute expression de type File est égale à une expression de la forme :

ajouter(ajouter (...ajouter(filevide,v1)..., vn)

qui est appelée forme normale.

L'utilisation des fonctions "filevide" et "ajouter" permet donc
d'obtenir tous les objets du type abstrait File. Les constructeurs d'un type
abstrait sont de telles fonctions, qui permettent de calculer tous les
objets de ce type.
On voit qu'en donnant la représentation de ces constructeurs on
donne une représentation pour chaque objet du type abstrait.

## II - 2 Rôle de l'interprétation de l'égalité

Pour avoir toutes les représentations possibles d'un objet, il
faut se donner en plus l'interprétation de l'égalité.

Ces deux données :

- l'implémentation des constructeurs,

- l'interprétation de l'égalité.

permettent de caractériser une représentation.

Si on reprend l'exemple de la File, les hypothèses de départ vont
être :

pourtout $t \in \text{Tableau}, i,j \in \text{Ent}, v \in \text{Valeur soit}$
(R1) $\quad \mathcal{D}^b(t,i,i) = \text{filevide}$
(R2) $\quad \mathcal{D}^b(\text{assign}(t,j,v), i, \text{succ}(j)) = \text{ajouter}(\mathcal{D}^b(t,i,j),v)$

**fin ;**

ainsi que

(Int E) ($t1, i1, j1$) $\rightleftharpoons$ ($t2, i2, j2$)
$|j1|-|i1| = |j2|-|i2|$ et $\forall k \text{ tel que}$
$0 \le |k| < |j1|-|i1|$, accès ($t1, \text{succ}^k(i1)$) = accès ($t2, \text{succ}^k(i2)$)

La relation ainsi définie doit être une relation d'équivalence.
D'autre part, il faut vérifier que ces hypothèses, représentation des cons-
tructeurs et interprétation de l'égalité, sont cohérentes - ici, on a bien :

$\mathcal{A}^b(t1,i1,j1) = \mathcal{A}^b(t2,i2,j2) = \text{filevide}$
$\Rightarrow (t1,i1,j1) = (t2,i2,j2)$

en effet $|j1|-|i1| = |j2|-|i2| = 0$ et il n'y a pas de $k$ vérifiant
D'autre part, la relation $\equiv$ est conservée par la représentation de ajouter, c'est-à-dire :

$$ (t1,i1,j1) \equiv (t2,i2,j2) \iff \\ \text{ajouter } (\tilde{o}_6(t1,i1,j1),v) = \text{ajouter } (\tilde{o}_6(t2,i2,j2),v) \\ \iff (\text{assign}(t1,j1,v), i1, \text{succ}(j1)) = (\text{assign}(t2,j2,v), i2, \text{succ}(j2)) $$

Pour cette démonstration on a besoin de certaines propriétés élémentaires des expressions de type `Ent`, en particulier :

$$ 
\begin{array}{l}
|i| = |j| \iff i = j \\
|j| - |i| = |k| \iff j = \text{succ}^k(i)
\end{array}
 $$

moyennant quoi, il est assez simple, en utilisant l'axiome (T2) de montrer que :

$$ |\text{succ}(j1)| - |i1| = |\text{succ}(j2)| - |i2| \\ \text{et } \forall k \text{ telque } o \le |k| < |\text{succ}(j1)| - |i1| $$

$$ \text{accès } (\text{assign}(t1,j1,v), \text{succ}^k(i1)) = \text{accès } (\text{assign}(t2,j2,v), \text{succ}^k(i2)) $$

ce qui démontre la relation cherchée.

A partir des hypothèses [R1], [R2] et [Int E] on retrouve les invariants de représentations (par exemple ici $|j|-|i| \ge o$) et la représentation des autres opérations du type `abstrait`.

## II - 3 Un exemple de synthèse d'opérations :

A partir des hypothèses [R1], [R2], [IntE] on va chercher des représentations des opérations premier et enlever, c'est-à-dire en reprenant les notations du paragraphe 1 deux opérations "premier c" et "enleverc" telles que :
- premier c est de profil (Tableau, Ent, Ent) → Valeur et vérifie l'égalité

[P1] premier c (t,i,j) = premier (db(t,i,j))

- enlever c est de profil (Tableau, Ent, Ent) → (Tableau, Ent, Ent) et vérifie

[E1] db(enlever c (t,i,j)) = enlever (db(t,i,j))

a) Etude de premier c :

La première règle de représentation [R1] donne :

premier (db(t,i,i)) = premier (filevide)

d'après l'axiome [F3] on a
= UNDEF

d'où un premier résultat :

[P2] premier c (t,i,i) = UNDEF

La deuxième règle de représentation [R2] donne :

premier (db(assign(t,j,v),i,succ(j))) =
premier (ajouter (db(t,i,j),v) =

d'après (F4)

si db(t,i,j) = filevide

alors v

sinon premier (db(t,i,j))

D'après [R1] et [Int E] la condition (db(t,i,j) = filevide) est équivalente à (i = j). En effet

(i = j) $\Rightarrow$ db(t,i,j) = filevide d'après [R1]

et

db(t,i,j) = filevide $\Rightarrow$ (t,i,j) = (t,i,i) $\Rightarrow$ i = j

d'après [Int E].
On arrive donc au résultat suivant :

premier ( $\mathcal{O}_b(\text{assign}(t,j,v),i, \text{succ}(j)) =$
$\underline{si} \ i = j \ \underline{alors} \ v \ \underline{sinon} \ premier (\mathcal{O}_b(t,i,j))$

On essaye par des changements de variables de simplifier la partie
gauche : soit $t_1 = \text{assign}(t,j,v)$.

D'après [T2] on a :
$$v = \text{accès}(t_1,j)$$

et d'après [INT E] :
$$ (t,i,j) = (t_1,i,j) $$

On a alors

premier ( $\mathcal{O}_b(t_1,i,\text{succ}(j)) =$
$\underline{si} \ i = j$
$\underline{alors} \ \text{accès}(t_1,j)$
$\underline{sinon} \ premier (\mathcal{O}_b(t_1,i,j)) ;$

Ceci donne une définition récursive de la représentation "premier c
de "premier" :

premier c (t1,i,succ(j)) = $\underline{si} \ i = j \ \underline{alors}$
$\text{accès}(t_1,j) \ \underline{sinon} \ premier c (t_1,i,j)$ ;

La récursivité de ce résultat est une conséquence de celle de
l'axiome (F4) qui définit l'opération "premier". Si on introduit une fonction
$pred = \text{succ}^{-1}$, on peut encore simplifier le premier membre en posant
$j_1 = \text{succ}(j)$ et la définition de premier c devient :

[P3]
premier c (t1,i,j1) = $\underline{si} \ succ(i) = j1 \ \underline{alors}$
$\text{accès}(t1,i) \ \underline{sinon} \ premier c (t1,i,pred(j1))$

D'après l'invariant de représentation on a $|j1| > |i| \text{ c'est-à-dire}$
$j1 = \text{succ}^k(i)$ et on montre par récurrence sur k que, avec cette hypothèse
$\text{accès}(t1,i)$ est solution de [P3].
Une telle solution n'existe pas toujours parmi les opérations du type objet, et dans certains cas, on doit se contenter d'une définition du type de [P3].

b) Etude de Enlever c

[R1] donne :

enlever ( $\int_b^c (t,i,i)$ ) = enlever (filevide)
= filevide = $\int_b^c (t,i,i)$

d'où le résultat

[E2] enlever c (t,i,i) = (t,i,i)

La deuxième règle de représentation [R2] donne :

enlever ( $\int_b^c (assign (t,j,v),i, succ (j))$ ) =
enlever ( ajouter ( $\int_b^c (t,i,j),v$) =

d'après [F2]

si $\int_b^c (t,i,j)$ = filevide
alors filevide
sinon ajouter (enlever ( $\int_b^c (t,i,j),v$) =

on a vu en a) que la condition se simplifie :

si i = j
alors filevide
sinon ajouter (enlever ( $\int_b^c (t,i,j),v$) =

On effectue les mêmes changements de variables que précédemment soit :

t1 = assign (t,j,v)
j1 = succ (j)

et toujours en utilisant l'interprétation de l'égalité et les axiomes des tableaux comme en a) on obtient :
enlever (enlever(t1,j,i1)) = si i = pred(j1) alors filevide
sinon ajouter (enlever(enlever(t1,i,pred(j1))), accès (t1,pred(j1)))

On passe au domaine concret.

enlever c (t1,i,j1) = si i = pred(j1)
alors (t1,i,i) [ou (t1,j1,j1)]
sinon ajouter c (enlever c (t1,i,pred(j1))), accès (t1,pred(j1)))

[E3]              = si i = pred (j1)

alors (t1,i,i) [ou (t1,j1,j1)]

sinon (assign (t2,j2,accès (t1,pred(j1))), i2, succ(j2))

avec (t2,i2,j2) = enlever c (t1,i,pred(j1))

C'est ce que donne une application systématique et automatique
de [R1], [R2], [Int E] et des axiomes.

On essaye un certain nombre de transformations, par exemple, soit :

t3 = assign (t2,j2,accès(t1,pred(j1)))

d'après [T2] on a

accès (t3,j2) = accès (t1,pred(j1))

et d'après [E3], si i ≠ pred (j1) on a

enlever c (t1,i,j1) = (t3,i2,succ(j2))

enlever c (t1,i,pred(j1)) = (t2,i2,j2)

Ces trois relations amènent à essayer les identifications suivantes

t3 = t1 = t2

j2 = pred(j1)
Moyennant quoi on obtient :

enlever c (t1,i,j1) =
si i = pred (j1)
alors (t1,i,i) [ou (t1,j1,j1)]
sinon (assign (t1,pred(j1), accès(t1,pred(j1))), i2,j1)

Ce dernier triplet est équivalent à (t1,i2,j1)
d'où

enlever c (t1,i,j1) =
si i = pred(j1)
alors (t1,i,i) [ou (t1,j1,j1)]
sinon (t1,i2,j1)

enlever c laisse inchangé t1, et j1 dans le cas général ; pour des raisons
de cohérence, il est souhaitable que cela soit vrai si i = pred(j1) donc

enlever c (t1,i,j1) =
si i = pred(j1)
alors (t1,j1,j1)
sinon (t1,i2,j1)

Il reste une seule inconnue qui est i2, la deuxième composante de
enlever c (t1,i,j1) mais aussi de enlever c (t1,i,pred(j1)). Comme
j1 = succ<sub>k</sub>(i) d'après les invariants de représentation on montre que

[E4] enlever c (t1,i,j1) = (t1,succ(i),j1)

II - 4. Conclusion

On voit sur ces deux exemples que la méthode employée est toujours
la même : on utilise d'abord systématiquement les règles de représentation
et les axiomes. On simplifie la définition obtenue par des changements
de variables appropriés et en passant au domaine concret on obtient une
définition de l'opération cherchée. Si les axiomes de départ sont récursifs,
cette définition est récursive et il faut chercher une solution éventuelle.

Si les opérations sont définies par des axiomes non récursifs, on n'a pas ce phénomène ; par exemple, ajoutons une opération "dernier" au type File, définie par :

$$ (F7) \text{ dernier } (\text{ajouter } (f,v)) = v; $$

$$ (F8) \text{ dernier } (\text{filevide}) = UNDEF; $$

on a les réécritures suivantes :

$$ \begin{align*} \text{dernier } (\text{\textit{cb}}(\text{assign}(t,j,v),i,\text{succ}(j))) &= \\ \text{dernier } (\text{\textit{ajouter}} (\text{\textit{cb}}(t,i,j),v)) &= \\ v \text{ d'après } (F7) \end{align*} $$

Soit $tl = \text{assign}(t,j,v)$, en appliquant la même méthode que pour "premier c" on obtient :

$$ \text{dernier c } (tl,i,\text{succ}(j)) = \text{accès } (tl,j) $$

Ce genre de démarche s'applique relativement bien à tous les types qui sont des "agrégats de valeurs organisés" comme les piles, les ensembles, les ensembles avec répétitions, les séquences, etc... Darlington [DAR 77] a utilisé son système de transformation de programmes pour effectuer un travail assez voisin (les données de départ ne sont pas les mêmes). On devrait pouvoir réaliser un système plus limité de réécritures permettant de compléter ce genre de spécifications incomplètes, et qui ne serait guère plus couteux qu'un système de preuve "à postériori".

## REMERCIEMENTS

Ce travail doit beaucoup à Messieurs C. PAIR et G. TERRINE. Il a pour origine les discussions avec J. GUTTAG lors de sa visite au Laboria en Juin 1977. J.P. FINANCE et P. LESCANNE ont été des critiques constructifs et encourageants.
[BER 77] D. BERT et P. JACQUET, Generic Abstract data types Proc. of 5th III Conference, J. André and J.P. Banatre Ed., IRIA Mai 1977.

[BUR 77] R.M. BURSTALL and J. DARLINGTON, A Transformation System for Developing Recursive Programs, J.A.C.M., Vol 24, n° 1, pp 44-67, 1977.

[DAR 77a] J. DARLINGTON, Program Transformation and Synthesis : Present Capabilities. Dept of Artificial Intelligence, Report n° 48, University of Edinburg (1977).

[DAR 77b] J. DARLINGTON, The Design of Efficient Data Representations, Dec 1977. (non publié).

[DEN 76] M.C. DENDIEN-GAUDÉL, Structures de Données et Traduction des Langages de Programmation, Rapport Laboria n° 193, Oct. 1976.

[GAU 77] M.C. GAUDEL, A Formal Approach to Translation Specification, Information Processing 1977, B. Gilchrist Ed., North-Holland, pp 123-129, 1977.

[GOG 75] J.A. GOGUEN, J.W. THATCHER, E.G. WAGNER, J.B. WRIGHT, Abstract Data Types as Initial Algebras and the Correctness of Data Representations, Proc. Conf. on Computer Graphics, Pattern Recognitions and Data Structure, Mai 1975.

[GUT 76a] J.V. GUTTAG, E. HOROWITZ, D.R. MUSSER, The Design of Data type Specifications, University of Southern California, Report ISI/RR-76-49, Nov 1976.

[GUT 76b] J.V. GUTTAG, E. HOROWITZ, D.R. MUSSER, Abstract Data Types and Software Validation, University of Southern California, Report ISI/RR-76-48, Aug 1976.

[HOA 72] C.A.R. HOARE, Proof of Correctness of Data Representations, Acta Informatica 1, pp 271-281, 1972.