IRIA
laboria

Institut de Recherche
d'Informatique
et d'Automatique

Domaine de Voluceau
Rocquencourt
78150 - Le Chesnay
Tél. 954.90.20

laboratoire de recherche
en informatique
et automatique

Aspects de la notion de type
en programmation

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

J. Boulenger, M. Kronental

Rapport de Recherche n° 108.

Mars 1975.
# ASPECTS DE LA NOTION DE TYPE EN PROGRAMMATION

J. Boulenger, M. Kronental

## RESUME

Le texte qui suit introduit une définition précise de la notion de *type* de variable utilisée en programmation. La distinction entre spécification et représentation est mise en relation avec la construction descendante des programmes et leur preuve. Cette méthode de travail est illustrée par un exemple.

## ABSTRACT

The present paper introduces a precise definition of the data-type concept. The distinction between specification and representation is related to top-down programming and correctness. This working method is illustrated by an example.
L'histoire préférée de Chad Mulligan.

"Un très distingué professeur de philosophie donne son cours, face à ses étudiants. Il prend un morceau de craie et inscrit au tableau une proposition de logique formelle. Il se retourne vers l'assistance et dit : "Mes demoiselles et Messieurs, vous êtes bien d'accord pour dire que cette proposition est évidente ?".

Puis il se retourne, regarde à nouveau la formule, se gratte la tête, et dit : "Excusez-moi !". Et il s'en va.

Une demi-heure plus tard, il revient, radieux, et dit d'un air triomphant : "J'avais parfaitement raison, c'est évident !" "

John Brunner,
Tous à Zanzibar.
# SOMMAIRE

## SYMBOLES UTILISES.

1. INTRODUCTION :
   1.1 Présentation de la notion de type ;
   1.2 Travaux apparentés ;
   1.3 Objectif de l'étude.

2. NOTION DE TYPE :
   2.1 Notations ;
   2.2 Modèle d'un type ;
   2.3 Spécification d'un type ;
   2.4 Discussion ;
   2.5 Représentation d'un type ;
   2.6 Conformité d'une représentation d'un type à sa spécification.

3. UTILISATION DES TYPES POUR LA CONSTRUCTION DESCENDANTE DES PROGRAMMES :
   3.1 Enoncé et solution d'un problème de programmation ;
   3.2 Définition d'une étape de la construction ;
   3.3 Théorème de conformité ;
   3.4 Enchaînement des étapes de la construction.

4. EXEMPLE : PROGRAMME DE SELECTION :
   4.1 Enoncé du problème ;
   4.2 Programme proposé comme solution
   4.3 Démonstration du programme ;
   4.4 Représentation du type itemqueue ;
   4.5 Démonstration de la conformité de la représentation du type itemqueue ;
   4.6 Résultat obtenu.

5. CONCLUSIONS :
   5.1 Relatives à l'exemple traité ;
   5.2 Relatives à la méthode utilisée.

ANNEXE : Instruction comme transformateurs de prédicat.

## REFERENCES.
## SYMBOLES UTILISES.

Les noms des ensembles sont en italiques, ceux des autres entités (variables, procédures, types, prédicats) en caractères droits.

Les notations les plus fréquemment utilisées dans cet exposé emploient la
collection suivante de caractères (éventuellement ornés d'indices,
d'apostrophes,...) :

<table><tr><td>A</td><td>application inverse de la représentation, A est son extension,</td></tr><tr><td>B</td><td>condition dans un programme,</td></tr><tr><td>c</td><td>corps de procédure,</td></tr><tr><td>e</td><td>élément neutre d'un monoïde,</td></tr><tr><td>f,g,h</td><td>fonctions,</td></tr><tr><td>I</td><td>prédicat (invariant),</td></tr><tr><td>i,j,k</td><td>nombre entiers,</td></tr><tr><td>P,Q</td><td>prédicats,</td></tr><tr><td>p</td><td>procédure,</td></tr><tr><td>R</td><td>collection de variables r<sub>1</sub>, r<sub>2</sub>,... apparaissant dans une<br>représentation, T' est l'ensemble des valeurs de R,</td></tr><tr><td>S</td><td>instruction,</td></tr><tr><td>T,W</td><td>types,</td></tr><tr><td>t</td><td>variable de type T,</td></tr><tr><td>T,W</td><td>ensembles associés respectivement aux types T,W,</td></tr><tr><td>X,Y</td><td>ensembles.</td></tr></table>
# 1. INTRODUCTION

## 1.1 Présentation de la notion de type

La notion de *type* est utilisée en programmation de la façon suivante : dire qu'une variable *t* est de type *T* est une façon de résumer une collection de propriétés que *t* possède en permanence (invariants).

Exemple : si *t* est de type *integer*, alors :

* *t* prend ses valeurs dans l'ensemble des entiers relatifs (muni de la structure d'anneau habituelle) ;

* *t* peut être opérande d'une addition ou d'une multiplication (opérations de cette structure d'anneau) ;

* *t* on peut assigner à *t* la valeur résultat d'une addition ou d'une multiplication.

L'utilisation de la variable *t* dans un programme particulier correspond à des invariants bien plus élaborés que ceux que l'on peut décrire avec les types classiques d'un langage de programmation tel qu'ALGOL 60.

Exemple : la valeur de *t* est toujours comprise entre 0 et 100 au sens large ; il est impossible en ALGOL 60 d'exprimer cette propriété de *t* en disant que *t* est d'un certain type ; cela est par contre possible en PASCAL où on écrit :

*type* intervalle = 0..100;

*var* t : intervalle;

La tendance dans les langages de programmation actuels est d'exprimer de plus en plus de propriétés des variables par leur type. En conséquence ces langages fournissent des opérateurs de construction de nouveaux types (éventuellement à partir de types primitifs). Mais faute d'une conception claire de ce qu'est un type, ces opérateurs ne permettent d'exprimer qu'une collection disparate de propriétés choisies empiriquement ([Habermann 73]). Ces langages restent donc inutilisables comme outils de conception.

## 1.2 Travaux apparentés

Les idées menant à la notion de type que nous allons définir plus loin apparaissent notamment dans les travaux de D.L. Parnas et C.A.R. Hoare.

Parnas développe la notion de *module* ([Parnas 71A]). Un module est la description du comportement d'un objet en termes d'une collection de fonctions propre à cet objet et de rien d'autre. Parmi ces fonctions on peut particuliser les *observations*, qui fournissent des informations sur l'état de l'objet. Si complexe que soit l'objet, une observation de cet objet ne peut fournir qu'un entier, un réel ou un booléen. Les fonctions qui modifient l'état de l'objet (et qui peuvent être des observations) sont spécifiées par l'effet
qu'elles ont sur les observations de cet objet ou d'autres objets.

Hoare ([Hoare 72]) introduit une notion de type de variable conçu comme une collection d'opérations. Pour ce, il affine la notion de "class" de SIMULA 67. Il obtient ainsi un procédé de représentation des types. L'utilisation des propriétés propres à la représentation d'un type est limitée à la déclaration de ce dernier. On ne peut donc manipuler une variable de ce type que par les opérations qui lui sont associées. Une telle opération peut être une fonction-procédure ou une procédure. Une fonction-procédure appliquée à une variable ne modifie pas l'état de cette variable et fournit un résultat de l'un des types primitifs de SIMULA 67, (à l'exception des références). Une fonction-procédure ou une procédure qui s'applique à une variable d'un type représenté a pour arguments supplémentaires éventuels des expressions de types primitifs. Il est impossible d'accéder de quelque façon que ce soit à la valeur d'une variable d'un type représenté. Toutes les opérations sont spécifiées dans les termes d'un modèle mathématique du type (au sens où l'anneau Z est un modèle du type integer).

## 1.3 Objectif de l'étude

Comme Hoare et Parnas, nous cherchons à définir un outil de conception des programmes. Un tel outil doit permettre une description descendante de ces programmes qui facilite :

* leur compréhension donc leur maintenance, leur adaptation et la communication entre programmeurs ;

* leur découpage donc leur preuve et l'organisation de l'équipe de programmation.

Ces objectifs (liés) sont incompatibles avec l'utilisation des langages de programmation actuels comme outils de conception ; en effet :

* ces langages imposent un niveau d'abstraction, alors que l'on veut pouvoir travailler tantôt au niveau d'abstraction dicté par le problème lorsqu'on cherche à en construire la solution, tantôt aux niveaux d'abstraction imposés par le matériel ou le langage de programmation choisi lorsqu'on veut tenir compte des contraintes techniques.

* leur utilisation conduit à n'avoir qu'une seule description, précise mais très compliquée, de ce que fait le programme, ce qui en rend la preuve pratiquement impossible.

Un élément important de cet outil de conception est la notion de type. Afin de préciser cette notion de type, on la définira sous trois aspects différents (mais non indépendants) : le modèle, la spécification et la représentation. Le point commun à ces trois aspects est qu'un type est défini par la collection des opérations que l'on peut faire sur toute variable de ce type.
La *spécification* d'un type T décrit le mode d'emploi des opérations de ce type, c'est-à-dire :

• les invocations d'opérations qui sont valides,

• ce que font ces opérations en termes de fonctions et de l'ensemble des valeurs de type T.

Une définition mathématique de cet ensemble de valeurs (Z pour le type integer, l'ensemble des parties de Z ne comportant pas plus de 100 éléments pour le type smallintset de [Hoare 72],...) et de ces fonctions constitue un *modèle* du type T. Une *représentation* du type T permet de remplacer une variable de ce type par une collection fixe et finie de variables d'autres types, et toute opération sur cette variable par un programme travaillant sur cette collection de variables.

On introduit et on utilise dans cette étude un système de notations permettant de décrire les aspects d'un type quelconque. Quelle que soit la ressemblance qu'il présente avec SIMULA 67 dont il est issu, ce système de notations n'est pas un langage de programmation compilable.

Après avoir défini les divers aspects de la notion de type et leurs relations, cette étude décrit une méthode de construction des programmes les utilisant, et l'illustre par un exemple.

Cette étude doit beaucoup à [Hoare 72]. Elle lève certaines restrictions qui y sont implicitement introduites (par l'utilisation de SIMULA 67) et limitaient considérablement la puissance de la notion de type (voir la discussion dans le paragraphe 2.4).

## 2. NOTION DE TYPE

### 2.1 *Notations*

Le système de notations que nous introduisons dérive de SIMULA 67, avec quelques extensions et beaucoup de restrictions.

Il est utilisé dans les définitions de la spécification et de la représentation d'un type.

Un programme est de la forme :

```
begin
    <déclarations> ;
    <instructions>
end
```
où <déclarations> est une liste de déclarations de variables. Toute variable
a un type. Les types et les variables sont désignés par des identificateurs.
La déclaration d'une variable t de type T est de la forme :

`var(T) t`

et signifie qu'une variable de type T existe et est désignée dans le programme
par t. Il n'y a pas d'autre moyen de la désigner et par conséquent à deux
identificateurs de variable différents correspondent deux variables distinctes.
Cette propriété est utilisée implicitement dans les démonstrations.

Dans le programme, `<instructions>` est une liste d'instructions composée en
utilisant les opérateurs de composition classique "séquencement", "if",
"while",... et les opérations de manipulation des variables. Ces opérations
sont des procédures ou des fonction-procédures. Chacune d'elle est désignée
par un identificateur. Dans le cas où l'on veut manipuler la variable t de
type T au moyen de l'opération p, on écrit :

`t.p<paramètres effectifs>`

où `<paramètres effectifs>` est une liste d'expressions de types divers, fixés
dans l'en-tête de p. Pour l'instruction d'assignation, on conserve la nota-
tion :

`t:=<expression de type T>.`

Une expression de type T est soit l'identificateur d'une variable de type T,
soit l'invocation d'une fonction-procédure dont le résultat est de type T.
A chaque type T est associée biunivoquement une collection d'opérations. Une
invocation d'opération :

`t.p<paramètres effectifs>`

est valide si :

* p est une des opérations associées au type de la variable t

* les types des paramètres effectifs sont conformes aux types des
paramètres formels indiqués dans l'en-tête de la procédure p.

L'en-tête d'une procédure p est de la forme :

`procedure p <paramètres formels>; <déclaration des paramètres formels>`

L'en-tête d'une fonction-procédure p dont le résultat est de type W est de
la forme :

`obs(W) procedure p<paramètres formels>; <déclaration des paramètres formels>`

La déclaration d'un paramètre formel a la même forme que la déclaration d'une
variable.
La notion de procédure telle qu'elle existe en ALGOL 60 n'est pas utilisée.

On a donc défini sommairement ce qu'est syntaxiquement un programme. Il reste à lui donner une signification. On considère qu'on ne sait dire quelque chose sur les variables du programme qu'avant ou après l'invocation d'une opération (de manipulation de ces variables) et ceci sous forme de prédicats. Compte tenu de la définition des opérateurs de composition donnée en annexe, il suffit d'être capable d'énoncer pour chaque opération de manipulation de variables les transformations de prédicat que peut entraîner son invocation pour obtenir la signification du programme sous la forme :

$$P_o \{ \text{instructions} \} Q_o$$

où $P_o$ et $Q_o$ sont des prédicats portant sur les variables du programmes. Restent à définir les prédicats. Pour ce faire on considère que toute variable d'un type T a une valeur dans un ensemble $T$ et donc qu'un prédicat est une relation entre les valeurs de variables. On détermine mathématiquement les ensembles de valeurs des types du programme à partir par exemple de l'intuition qu'on a de ce que fait celui-ci. Dans cette étude, on choisit de regrouper les transformations de prédicat des opérations associées à un type pour constituer ce qu'on appelle la **spécification** de ce type. Tous les objets mathématiques utilisés dans cette specification sont regroupés dans ce que l'on appelle le **modèle** du type.

## 2.2 Modèle d'un type.

Le modèle d'un type T se compose de :

* un ensemble noté $T$ et appelé **ensemble des valeurs possibles** ; en général $T$ est muni d'une structure algébrique ;

* un élément $v_o$ de $T$ appelé **valeur initiale** ;

* une collection finie de fonctions de la forme :

$$f : T \times X_1 \times X_2 \times \dots \times X_n \longrightarrow Y$$

où $n$ est un entier positif ou nul, dépendant de $g$, et $X_1, X_2, \dots, X_n, Y$ sont des ensembles non nécessairement distincts de $T$ et apparaissant dans les modèles de $T$ ou d'autres types.

Dans le cas où $T$ est muni d'une structure algébrique, il est possible, mais nullement obligatoire, que certaines fonctions soient des lois de composition intervenant dans la définition de cette structure.
Exemple : le modèle du type integer d'ALGOL 60 se compose de :

• comme ensemble des valeurs possibles, l'ensemble des entiers relatifs $z$ muni de la structure d'anneau pour les lois de composition $+$ et $-$,

• la valeur initiale $0$,

• les fonctions :

$$f : Z^2 \underset{+}{\longrightarrow} Z \text{ telle que } f(z_1, z_2) = z_1 + z_2,$$

$$f : Z^2 \underset{-}{\longrightarrow} Z \text{ telle que } f(z_1, z_2) + z_2 = z_1,$$

$$f : Z^2 \underset{x}{\longrightarrow} Z \text{ telle que } f(z_1, z_2) = z_1 \times z_2$$

$$f : Z \underset{\div}{\longrightarrow} Z \text{ telle que } f(z_1, z_2) \text{ est le quotient entier de } z_1 \text{ par } z_2$$
etc...

Exemple : le modèle du type compteur se compose de :

• comme ensemble des valeurs possibles, l'ensemble des entiers naturels $N$,

• la valeur initiale $0$,

• la fonction $f : N \longrightarrow N$ telle que $f(z) = z+1$,

• la fonction $g : N \longrightarrow \{\text{true}, \text{false}\}$ telle que $g(z) = \text{true}$ si et seulement si $z \le 100$.

## 2.3 Spécification d'un type

A un type $T$ sont associées :

• la possibilité d'introduire dans un programme des variables de ce type et de les désigner,

• une collection fixe d'opérations (procédures et fonction-procédures) permettant de manipuler ces variables.

Une specification du type $T$ vise à définir l'effet de ces opérations par des transformations de prédicat. Le procédé de spécification utilisé dans la présente étude s'appuie sur un modèle du type $T$.
Lorsqu'une variable t est introduite, elle l'est avec la valeur initiale $v_o$ mentionnée dans le modèle, ce qui se traduit par la transformation de prédicat suivante :

$$ true \{var (T) t\} t = v_o $$

On distingue les opérations qui permettent de modifier la valeur d'une variable et qui sont les procédures, des opérations qui permettent d'obtenir une information sur la valeur de cette variable sans la modifier, et qui sont les fonctions-procédures. Dans cette étude on choisit d'associer biunivoquement à chaque opération une fonction du modèle.

A une procédure est donc associée une fonction de la forme :

$$ f : T \times X_1 \times \dots \times X_n \longrightarrow T. $$

On appellera indifféremment *transformation* cette procédure ou cette fonction. Transformer la variable t au moyen de la transformation f se fait ainsi en invoquant la procédure $p_f$ associée à f par :

$$ t \cdot p_f <\text{paramètres effectifs}> $$

Cette invocation a la signification suivante :

* les `<paramètres effectifs>` ont les valeurs $x_1, x_2, \dots, x_n$,

* si $t = v$ avant l'exécution de $p_f$, alors

$t = f(v, x_1, x_2, \dots, x_n)$ après l'exécution, si toutefois celle-ci se termine,

où $x_1, x_2, \dots, x_n$ sont des éléments quelconques respectivement des ensembles $X_1, X_2, \dots, X_n$ et $v$ est un élément quelconque de $T$.

Ceci est équivalent à la transformation de prédicat suivante :

$$ t = v\{t \cdot p_f <\text{paramètres effectifs}>\} \quad t = f(v, <\text{paramètres effectifs}>$$

De même à une fonction-procédure est associée une fonction de la forme :

$$ g : T \times Y_1 \times \dots \times Y_n \longrightarrow W. $$

On appellera indifféremment *observation* cette fonction-procédure ou cette fonction. En général $W$ est un ensemble apparaissant dans le modèle d'un type "plus simple" que $T$.
Observer la variable *t* au moyen de l'observation *g* se fait en invoquant la fonction-procédure *p*<sub>*g*</sub> associée à *g* par :

t.p<paramètres effectifs>

Cette invocation a la signification suivante :

. les <paramètres effectifs> sont des valeurs y<1>,y<2>,...y<sub>n</sub> ;

. si t = v avant l'exécution de p<sub>g</sub>, alors t = v et

t.p<paramètres effectifs> = g(v,y<1>,y<2>,...y<sub>n</sub>) = w après

l'exécution, si toutefois celle-ci se termine ;

où y<1>, y<2>,...y<sub>n</sub> sont des éléments quelconques respectivement des ensembles
Y<1>, Y<2>,... Y<sub>n</sub>, w est un élément de W, et v un élément quelconque de T.

Ceci est équivalent à la transformation de prédicat suivante :

t = v {t.p<paramètres effectifs>} t = v &t.p<paramètres effectifs>

Exemple : Pour déclarer un compteur C, on écrit :

var(compteur) C

correspondant à la transformation de prédicat :

true {var(compteur) C} C = 0,

pour la transformer, on invoque la

procedure compter.

correspondant à la transformation de prédicat :

C = z {C. compter} C = z + 1

et pour l'observer on invoque la

obs (boolean) procedure sûreté

correspondant à la transformation de prédicat :

C = z {C.sûreté} C = z&C.sûreté = (z≤100).

On remarque que contrairement à ce qui est admis par Parnas, les
observations ne modifient pas la valeur de la variable observée. S'il n'en
était pas ainsi, l'ordre dans lequel on fournit les <paramètres effectifs>
à une transformation ne serait pas indifférent, ce qui rendrait inutilisable
la transformation de prédicat correspondante.

On remarque également qu'à partir d'un modèle, on peut bâtir plusieurs
spécifications différant entre elles par les opérations qui y apparaissent.

Considérons par exemple le modèle d'un type MATRICE constitué par :

. l'ensemble *M* des (2,2) matrices à coefficients réels,

. la valeur initiale matrice identité,
notamment la fonction f : M → M qui à toute matrice x lui
fait correspondre son inverse s'il existe.

On peut associer à f une des trois opérations suivantes :

. la **procedure** inverser spécifiée par :

X = x{X.inverser} X = f(x),

. la **procedure** copierinverse (Y) ; obs(MATRICE)Y spécifiée par :

X = x & Y = y{X.copierinverse(Y)} X = f(y),

. la obs(MATRICE) procedure inverse spécifiée par :

X = x{Xpelastore} Xpelastore = f(x).

Les critères de choix seront la commodité de l'opération dans le programme
mais aussi les contraintes de représentation.

Ceci nous permet de souligner la distinction entre le modèle destiné à une étude mathématique et la spécification permettant d'écrire et de donner une signification à un programme.
## 2.4 Discussion

En utilisant les définitions et notations précédentes, une hypothèse faite et non discutée par Hoare et Parnas se formule de la manière suivante :

* le résultat d'une observation est de type primitif ;

* tout paramètre formel d'une procédure ou d'une fonction-procédure est de type primitif.

Une conséquence de cette hypothèse est que les opérations d'un type T sont T-unaires (i.e ne peuvent avoir qu'un seul argument de type T). En particulier, il ne serait pas possible d'introduire :

* la copie spécifiée par :

$$ Y := y\{X.copy(Y)}X = y \quad \text{où X et Y sont deux variables quelconques de type T;} $$

* la comparaison spécifiée par :

$$ X = x \& Y = y \{X.greater(Y)} X = x \& X.greater(Y) = (x>y) $$

où X et Y sont deux variables quelconques de type T, et > est une relation d'ordre sur l'ensemble T ; il serait alors impossible par exemple de séparer dans la description d'un programme de tri, la description de l'algorithme de tri proprement dit, dépendant seulement de l'existence d'une relation d'ordre, de celle de la relation d'ordre employée, qui dépend des données triées et devrait donc être associée à leur type ;

* des lois de composition internes telles que le produit matriciel ;

* les opérations associées à un type pile telles que :

$$ P.empiler(X) $$

dans laquelle P est une variable de type pile et X une variable d'un type dont on n'a aucune raison de supposer qu'il est primitif comme cela est fait par exemple dans [Parnas 71A].

Ces inconvénients expliquent l'extension que nous avons apporté à la notion de type de Hoare en donnant la possibilité d'introduire des opérations dont les paramètres formels sont de type quelconque ; en particulier on pourra donc introduire des opérations T-n-aires.

L'hypothèse mentionnée plus haut est liée à la possibilité d'une "implémentation" directe efficace (directe au sens où par exemple on fait correspondre à une opération d'un type une procédure du langage de programmation).
Lorsqu'un paramètre est transmis, il l'est "par valeur" donc il est recopié ;
s'il est d'un type construit, on peut craindre qu'il occupe une place importante
en mémoire et que sa recopie coûte cher en espace comme en temps.

Les trois raisons suivantes nous font rejeter cet argument :

• il peut exister des procédés câblés rendant cette recopie moins coûteuse ;

• une variable d'un type construit n'occupe pas nécessairement une place importante en mémoire ;

• dans l'"implémentation", on n'est pas obligé de faire cette recopie (emploi judicieux des références) ; l'outil de conception ne doit donc pas être conçu avec pour objectif d'optimiser de telles recopies.

Les opérations que nous introduisons peuvent donc être T-n-aires mais elles ne transforment qu'un paramètre au plus. Nous nous sommes imposés cette restriction pour les raisons suivantes :

• simplicité des opérations,

• rattachement "naturel" d'une opération à un type (celui du paramètre qu'elle transforme),

mais on pourrait l'abandonner tout en conservant la méthode, par exemple en introduisant la notion de paramètre résultat.

## 2.5 Représentation d'un type

La représentation d'un type T vise à décrire ce type en fonction de types "plus simples". Elle s'écrit dans notre système de notations comme la déclaration d'une "class" SIMULA 67 :

class T ;

begin

<déclarations> ;

<initialisation>

end

Les déclarations comprennent :

• des déclarations de variables $r_1, r_2, ...$ qui peuvent être par exemple des tableaux ; on notera $R$ la collection (finie) de ces variables, et $T'$ l'ensemble de toutes les combinaisons de valeurs possibles de ces variables.

si $T_1$ est l'ensemble des valeurs possibles de $r_1$, $T_2$ l'ensemble des valeurs possibles de $r_2$, ... alors $T' = T_1 \times T_2 \times ...$;

• la déclaration des procédures et des fonctions-procédures mentionnées dans la spécification de T.
L'<initialisation> est une instruction composée qui ne manipule que les variables de R.

La déclaration dans un bloc de la variable t par :

var(T) t

est équivalente à :

1. La déclaration d'une collection (que l'on notera t.R) de variables t.r₁, t.r₂,... qui sont une version propre à t de R ;

2. l'exécution à l'entrée dans le bloc de la partie <initialisation> portant sur t.R

L'invocation d'une procédure p par

t.p<paramètres effectifs>

entraîne l'exécution de son corps c. Cette exécution travaille sur les variables de t.R, sur les variables locales de p, elle observe les <paramètres effectifs> et, dans le cas d'une fonction-procédure en évalue le résultat.

Le traitement des paramètres d'une procédure pose des problèmes que l'on ne rencontre pas dans l'interprétation des appels de procédure SIMULA 67, où les seuls paramètres transmis "par valeur" sont de type primitif.

Or, comme on l'a vu dans la discussion précédente, nous admettons que les expressions transmises peuvent être de type quelconque. Ceci requiert une définition précise de l'interprétation des invocations de procédure (le procédé de macrogénération mentionné dans [Hoare 72] étant insuffisant).

Cette interprétation exige l'existence d'une instruction d'assignation associée aux types dont on veut transmettre des variables en paramètre.

Soit x l'un des <paramètres formels>. C'est une variable de type X que l'on a initialisée lors de l'invocation de la procédure p. Deux cas se présentent :

1. Le type X n'est pas le type T : dans ce cas les seules manipulations de x dans le corps de la procédure p sont :

• la transmission de x comme paramètre effectif dans l'invocation d'une procédure p' ;

• l'instruction d'assignation :

y := x

où y est une variable de type X faisant partie de R, ou une variable locale à p ;

• l'observation de x, au moyen d'une observation associée au type X.
2. Le type X est le type T : dans ce cas les seules manipulations possibles de x sont des observations des variables de x.R.

Exemple : on veut décrire la fonction produit scalaire de deux vecteurs de 1'espace à trois dimensions. La collection de variables R est

`var(real) x,y,z`

et la fonction produit scalaire sera représentée par :

`obs(real) procedure scalaire(V) ; obs(vecteur) V ;`

`scalaire := x*V.x + y*V.y + z*V.z ;`

Exemple : une représentation du type compteur est :

class compteur ;

begin
  var (integer) valeur ;
  procédure compter ;
    valeur := valeur + 1 ;
  obs (boolean) procedure sûreté ;
    sûreté := valeur ≤ 100 ;
end

2.6 Conformité d'une représentation d'un type à sa spécification.

Ayant deux descriptions d'un type T, sa spécification et sa représentation,
il s'agit de définir une relation entre elles, traduisant le fait qu'elles sont
relatives au "même" type. Cette relation est la _conformité_ de la représentation
à la spécification.

Sommairement, cette relation exprime que les corps

. de l'<initialisation>,

. des procédures associées aux transformations,

. des fonctions-procédures associées aux observations, ont sur t.R des effets "analogues" à ceux des opérations correspondantes sur t, pour les "mêmes" <paramètres effectifs>.

Le but de ce paragraphe est d'expliciter le sens qu'il faut donner aux
adjectifs "analogue" et "même" afin de préciser la relation de conformité, et
de décrire les techniques qui permettent de la démontrer.
2.61 Définition du critère de conformité.

On se donne une fonction que nous appellerons A (comme _abstraction_)
qui fait correspondre à toute combinaison de valeurs possibles
des variables de R, c'est-à-dire à tout élément v' dans T' la valeur A(v') dans
T que l'on notera également A(R).

Exemple : dans le cas du type compteur, T' est Z et A est donc la fonction :

Z $\rightarrow$ N telle que :

pour z < 0, A(z) est non définie,

pour z ≥ 0, A(z) = z.

2.611 Conformité de la représentation de l'initialisation.

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

L'instruction composée <initialisation> sera conforme à la spécification de
T si v' étant la valeur de R après son exécution, on a :
A(v'O) = vO, où vO est la valeur initiale définie dans le modèle du type T.
2.612 Conformité de la représentation $c_f$ d'une transformation $f$.

Intuitivement si $R = v'_1$ avant exécution de $c_f$ et $R = v'_2$ après celle-ci, pour une valeur donnée quelconque des <paramètres effectifs>, on doit avoir la relation :

$$ \bar{v}_2 = v_2 $$

dans laquelle :

$$ \bar{v}_2 = A(v'_2), $$

$$ v_2 = f(v_1, \langle \text{paramètres effectifs} \rangle), $$

$$ v_1 = A(v'_1) $$

Autrement dit les deux chemins mis en évidence dans la figure ci-dessous mènent au "même endroit" $\bar{v}_2 = v_2$.

<figure><img src="image_3.png" /></figure>
Malheureusement les choses ne sont pas aussi simples du fait que les <paramètres effectifs> peuvent très bien comporter des expressions de type T de sorte que parler de la "même" valeur des <paramètres effectifs> est une approximation. Il faut aussi utiliser $\bar{A}$ pour les <paramètres effectifs>. D'où les définitions qui suivent.

On introduit l'opérateur algébrique $\bar{A}$ ainsi défini : si $s'$ est la suite de valeurs $v'_1, v'_2, \dots, v'_n$ de variables de types respectifs $T_1, T_2, \dots, T_n$ alors $\bar{A}(s')$ est la suite de valeurs $v_1, v_2, \dots, v_n$ définie par :

$$ 
\begin{array}{l}
\text{pour tout } i, \quad 1 \le i \le n, \\
v_i = v'_i \quad \text{si} \quad T_i \text{ n'est pas } T, \\
v_i = A(v'_i) \quad \text{si} \quad T_i \text{ est } T.
\end{array}
$$

On peut alors donner le critère de conformité de la représentation $c_f$ d'une transformation $f$ par :

si $R = v'_1$ avant exécution de $c_f$ et $v'_2$ après cette exécution pour une valeur donnée quelconque des <paramètres effectifs> alors :

$$ A(v'_2) = f(A(v'_1), \bar{A}(\langle \text{paramètres effectifs} \rangle)). $$

De cette façon, on tient compte du fait que les paramètres effectifs de type $T$ n'ont pas dans le corps $c_f$ de la procédure une valeur dans $T$ mais une valeur dans $T'$.

Du fait que $c_f$ ne transforme aucune autre variable que celles de $R$ ou celles qui lui sont locales, on peut déduire que l'invocation :

$t.p<\text{paramètres effectifs}>$

ne modifie aucune autre variable du programme appelé que $t$.

### 2.613 Conformité de la représentation d'une observation $g$.

Supposons que $R = v'_1$ avant exécution du corps $c_g$ représentant l'observation $g$, et $R = v'_2$ après cette exécution, pour une valeur donnée quelconque des <paramètres effectifs> ; soit $\bar{w}$ la valeur de la fonction-procédure $p_g$ après cette exécution. On peut alors donner le critère de conformité de la représentation $c_g$ de $g$ par les relations :

* $A(v'_2) = A(v'_1)$, qui traduit le fait que l'observation $g$ n'a pas modifié la valeur dans $T$ de la variable observée ;

* $\bar{w} = g(A(v'_1), \bar{A}(\langle \text{paramètres effectifs} \rangle))$, qui traduit le fait que l'observation donne le même résultat dans la spécification et dans la représentation, dans le cas où $W$ est distinct de $T$.
Ce qui se traduit dans la figure suivante par les conditions

$v_1 = v_2 \text{ et } \bar{w} = w$

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

Dans le cas où W est T, g donne un résultat w dans T et $c_g$ un résultat w' dans T'; la condition $\bar{w}=w$ indiquée ci-dessus doit alors être remplacée par $w = A(w')$. On n'envisagera pas ce dernier cas dans la suite, afin de simplifier l'exposé.

## 2.62 Techniques de démonstration.

En pratique A n'est pas partout définie dans T'.

On caractérise le sous-ensemble de T' sur lequel A est définie par une relation (invariante) entre les variables de R, notée I.

Exemple : pour le type compteur, l'invariant est :

$valeur \geq 0.$
Donc la démonstration de la conformité d'une représentation d'un type à sa spécification se ramène à la démonstration des transformations de prédicats suivantes :

1) pour l'initialisation :

$$ \underline{\text{true}} \quad \{^c\langle\text{initialisation}\rangle\} \quad \mathbf{I} \ \& \ \mathbf{A}(\mathbf{R}) \ = \ v_o $$

2) pour chaque transformation f :

$$ \mathbf{I} \ \& \ \mathbf{A}(\mathbf{R}) \ = \ v\{c_f\}\mathbf{I} \ \& \ \mathbf{A}(\mathbf{R}) \ = \ f(v, \bar{\mathcal{A}}(\langle\text{paramètres effectifs}\rangle)), $$

3) pour chaque observation g :

$$ \mathbf{I} \ \& \ \mathbf{A}(\mathbf{R}) \ = \ v\{c_g\}\mathbf{I} \ \& \ \mathbf{A}(\mathbf{R}) \ = \ v \ \& \ p_g \ = \ g(v, \bar{\mathcal{A}}(\langle\text{paramètres effectifs}\rangle)), $$

Il peut arriver que la représentation d'une procédure $p_f$ ou $p_g$ ne soit pas conforme à sa spécification pour n'importe quelles valeurs des $\langle\text{paramètres effectifs}\rangle$ et n'importe quelle valeur de la variable manipulée. On caractérise alors l'ensemble des combinaisons possibles de valeurs des $\langle\text{paramètres effectifs}\rangle$ et de la variable manipulée par une pré-condition P qui dépend de la procédure considérée. Cette pré-condition est une relation entre les paramètres et les variables de R. Dans ce cas, les transformations de prédicats à démontrer s'écrivent

1) pour l'initialisation :

$$ \underline{\text{true}} \quad \{^c\langle\text{initialisation}\rangle\} \quad \mathbf{I} \ \& \ \mathbf{A}(\mathbf{R}) \ = \ v_o $$

2) pour chaque transformation f :

$$ \mathbf{I} \ \& \ \mathbf{A}(\mathbf{R}) \ = \ v \ \& \ P_f\{c_f\}\mathbf{I} \ \& \ \mathbf{A}(\mathbf{R}) \ = \ f(v, \bar{\mathcal{A}}(\langle\text{paramètres effectifs}\rangle)), $$

3) pour chaque observation g :

$$ \mathbf{I} \ \& \ \mathbf{A}(\mathbf{R}) \ = \ v \ \& \ P_g\{c_g\}\mathbf{I} \ \& \ \mathbf{A}(\mathbf{R}) \ = \ v \ \& \ p_g \ = \ g(v, \bar{\mathcal{A}}(\langle\text{paramètres effectifs}\rangle)). $$
### 3. UTILISATION DES TYPES POUR LA CONSTRUCTION DESCENDANTE DES PROGRAMMES

#### 3.1 Enoncé et solution d'un problème de programmation

Un problème de programmation est défini lorsque l'on connait :

* l'ensemble des données possibles,

* l'ensemble des résultats possibles,

* la relation entre données et résultats.

On considère que données et résultats sont les valeurs d'une collection de variables dites principales de types spécifiés. La relation entre données et résultats se traduit par une relation entre les valeurs de ces variables avant et après exécution d'un programme appelé programme solution S. On l'exprime par la transformation de prédicat :

$$P_o\{S\} Q_o$$

où $P_o$ et $Q_o$ portent sur les variables principales et sont énoncés dans les termes des modèles des types de ces variables.

Tout ou partie des variables principales reçoit une valeur (qui peut ne pas être la valeur initiale du type correspondant) avant l'exécution du programme S.

Le problème étant énoncé sous cette forme, on construit par une méthode quelconque le programme S censé le résoudre ; on utilise pour cela :

* les opérations de manipulation des variables principales (mentionnées dans la spécification des types de ces variables) ;

* une collection de variables auxiliaires, dont on spécifie les types, et par suite les opérations permettant de les manipuler ;

* les opérateurs de composition d'instructions.

Disposant de la spécification des types de toutes les variables utilisées dans le programme et d'opérateurs de composition bien définis, on peut démontrer que le programme résout bien le problème posé. Cette démonstration est possible en pratique parce que le programme est petit (types adaptés au problème) et que les opérateurs de composition sont simples.

#### 3.2 Définition d'une étape de la construction

Les types des variables (principales ou auxiliaires) qui apparaissent dans le programme S peuvent être très "éloignés" des types habituellement
disponibles dans les langages de programmation. On en construit donc une
représentation en utilisant des types plus "simples" que l'on spécifie si
nécessaire à cette occasion, et on en démontre la conformité. Cette
construction est poursuivie jusqu'à ce que les types spécifiés soient
suffisamment "faciles à implémenter". L'objet de ce paragraphe est de
préciser ce qu'est une étape de cette construction.

Lors d'une étape, on construit une représentation de l'un des types
de variable de S. Soit T ce type. La démonstration D de S est fondée sur
la spécification de tous les types utilisés dans S et en particulier de
celle du type T. D utilise les hypothèses H suivantes, valides pour toute
variable t de type T :

1) pour la déclaration :

`true {var(T) t} t = v_o,`

2) pour toute transformation f associée au type T :

$t=v\{t.p_f<paramètres effectifs>\} t=f(v,<paramètres effectifs>),$

3) pour toute observation g associée au type T :

$t=v\{t.p_g<paramètres effectifs>\} t=v\&t.p_g=g(v,<paramètres effectifs>).$

Malheureusement, la démonstration de la conformité de la représentation
du type T à sa spécification n'établit pas H mais les transformations de
prédicat H' suivantes :

1) pour l'initialisation :

`true {t.c<initialisation>} I&A(t.R) = v_o`

2) pour toute transformation f :

$I\&A(t.R)=v\{t.c_f\}I\&A(t.R)=f(v, \bar{A}(<paramètres effectifs>)),$

3) pour toute observation g :

$I\&A(t.R)=v\{t.c_g\}I\&A(t.R)=V\&t.p_g=g(v, \bar{A}(<paramètres effectifs>)),$
où I porte sur les variables de t.R.

La substitution de H' à H invalidant la démonstration D, il faudrait
produire une nouvelle démonstration D' de S qui tienne compte de H'.
Heureusement le théorème de conformité que nous allons présenter rend
inutile la démonstration D', et ceci quel que soit le programme S et le
type T représenté. D'où l'intérêt de cette méthode de construction.
### 3.3 Théorème de conformité.

### 3.31 Exécutions du programme S.

Soit U l'ensemble de toutes les combinaisons possibles de valeurs des variables du programme S compte-tenu des hypothèses H. Représenter le type T revient à remplacer l'ensemble T des valeurs des variables du type T par l'ensemble T' des combinaisons de valeurs de t.R. Cela impose de remplacer l'ensemble U par l'ensemble U' obtenu à partir de U en changeant ses composantes cartésiennes T en T'. On peut alors associer à tout élément u' de U' l'élément u de U défini de la manière suivante :

si $u' = (x'_{1}, x'_{2}, \dots, x'_{n})$

alors $u = (x_{1}, x_{2}, \dots, x_{n})$ avec pour tout $i$, $1 \le i \le n$ :

$x_i = A(x'_i)$ si $x_i$ est la valeur d'une variable de S de type T,

$x_i = x'_i$ dans le cas contraire,

soit encore $u = \bar{A}(u')$.

Une exécution du programme S est caractérisée par la suite des valeurs que prennent ses variables. Le passage d'une valeur de cette suite à la valeur consécutive correspond à l'exécution d'une instruction non composée de S, c'est-à-dire d'une transformation d'une variable de S. Cette suite est finie si et seulement si l'exécution se termine.

Suivant que l'on prend en compte la spécification ou la représentation de T, on a une suite d'éléments de U :

$E = (u_0, u_1, \dots)$

ou dans $U'$ :

$E' = (u'_0, u'_1, \dots).$

### 3.32 Théorème de conformité.

Si la représentation du type T est conforme à sa spécification, alors deux exécutions E et E' vérifiant :

$u_0 = \bar{A}(u'_0)$

et

E' finie

sont telles que :

* E est finie, et a la même longueur k que E',

* $u_k = \bar{A}(u'_k)$.

Si T est le type d'au moins une variable principale donnée, par
exemple t, il faut en outre que l'invariant apparaissant dans la
représentation de T soit vrai par la valeur de départ de t.R (afin
que $\bar{A}$ soit défini en $u'_o$).

On démontre ce théorème en raisonnant par récurrence sur l'indice i de $u_i$ dans E et en utilisant les propriétés des opérateurs de composition d'instructions ("séquencement", "if", "while",...).

L'inutilité de D' en découle à condition que I(t.R) soit initialement vrai pour toute variable t de type T qui soit une donnée.

L'introduction d'une pré-condition ne permet plus d'appliquer le théorème de conformité.

Trois attitudes peuvent alors être adoptées :

1) faire directement la démonstration D' en utilisant les transformateurs de prédicat tels qu'ils sont définis dans la représentation de T ;

2) modifier la spécification de T afin que les pré-conditions disparaissent, et remanier la construction ;

3) introduire dans la représentation de T le test des pré-conditions ; la description de ce qui se passe lorsque l'un de ces tests est négatif relève, selon la politique de traitement des **erreurs** choisie, de la représentation de T, ou bien du programme où T est employé, etc...

### 3.4. Enchaînement des étapes de la construction.

La représentation des types des variables du programme S peut a priori
se faire dans n'importe quel ordre.

Ces représentations nécessitent éventuellement l'introduction de types
auxiliaires. Le graphe obtenu en associant un noeud à chaque type et en
introduisant une flèche du noeud $T_1$ vers le noeud $T_2$ si on utilise le type $T_2$ dans la représentation du type $T_1$, est un latticiel. Ceci résulte du
fait que la collection de variables par laquelle on représente une variable
d'un type est fixe et finie. De ce latticiel on peut déduire la relation d'or
partiel "plus simple" employée dans le paragraphe 2.3 : $T_2$ est **plus simple** que $T_1$ s'il existe un chemin menant du noeud $T_1$ au noeud $T_2$. Les types **primitifs** sont ceux qui n'ont pas de successeur dans le latticiel. On ne
les représente pas parce qu'ils sont disponibles dans le langage de
programmation utilisé sous une forme compatible avec leur spécification.
## 4. EXEMPLE : PROGRAMME DE SELECTION.

### 4.1 Enoncé du problème.

Il s'agit de sélectionner dans une file F des articles satisfaisant un certain critère et de les ranger dans une file G dans l'ordre où ils étaient dans F.

Les articles sont des variables du type item. Un modèle de ce type est constitué par :

* un ensemble de valeurs noté *item* ;

* une fonction $f : item \times item \rightarrow item$ telle que $f(x,y) = y$ (copie) ;

* une fonction $g$ à valeurs booléennes (critère).

La spécification du type *item* est donc constituée par :

$$ 
\begin{align*}
X &= x \ \& \ Y = y \ \{ X.copy(Y) \} \ X = f(x,y) \\
X &= x \ \{ X.test \} \ X = x \ \& \ X.test = g(x)
\end{align*}
$$

où X et Y sont des variables du type *item* et x et y des éléments quelconques de l'ensemble *item*.

Les files F et G sont des variables du même type *itemqueue*. Le modèle de ce type a comme ensemble de valeurs possibles $item^*$ (monodé libre sur l'ensemble *item*). Les données du problème correspondent aux valeurs initiales e pour G et une valeur quelconque w pour F. Les résultats correspondent aux valeurs finales e pour F et $h^*(w)$ pour G, avec :

$$ 
\begin{align*}
h & : \quad item \rightarrow item^* \quad \text{telle que } h(x) = \text{si } g(x) = \underline{\text{true}} \quad \text{alors } x \text{ sinon e,} \\
h^* & : \quad item^* \rightarrow item^* \quad \text{telle que } h^*(e) = e \text{ et } h^*(vx) = h^*(v) h(x).
\end{align*}
$$

Ceci constitue la spécification du programme de sélection.

### 4.2 Programme proposé comme solution.

```
begin
    var(itemqueue) F,G;
    var(item) X;
    comment production d'une valeur pour F;
    while F.empty
        do
            begin
                X.copy(F head);
                if X.test
                    then G.append(X);
                        F.remove
            end
        end
end
```
Pour donner une signification à ce programme, il reste à préciser `itemqueue`.
La spécification de ce type est :

```
    true {var(itemqueue) F} F = e
X = x & F = v {F.append(X)} F = f₁(v,x),
F ≠ e & F = v {F.remove} F = f₂(v),
F = v {F.empty} F = v & F.empty = g₁(v),
F ≠ e & F = v {F-head} F = v & F-head = g₂(v),
```

où X est une variable de type item, F une variable de type `itemqueue`, x un élément quelconque de `item` et v un élément quelconque de `item*`.

Les fonctions employées dans cette spécification sont définies dans le
modèle du type `itemqueue` de la façon suivante :

$f_1 : item^* \times item \rightarrow item^*$ telle que

$f_1(v,x) = vx$ (concaténation dans `item*`),

$f_2 : item^* \rightarrow item^*$ telle que $f_2(xv) = v,$

$f_2(e)$ étant indéfini ;

deux observations $g_1$ et $g_2$ :

$g_1 : item^* \rightarrow \{\underline{true}, \underline{false}\}$ telle que

$g_1(v) = (v = e),$

$g_2 : item^* \rightarrow item$ telle que $g_2(xv) = x,$

$g_2(e)$ étant indéfini.

## 4.3 Démonstration du programme.

Cette démonstration se décompose en trois étapes :

* traitement de la boucle "while",

* traitement du "if",

* traitement du corps du "while",

correspondant aux décompositions successives du programme :
• `while B₁ do S₁`

• $S_3 = \underline{\underline{\text{if} \ B_2 \ \text{then} \ S_4 \ \underline{\underline{\text{else} \ S_5}}}}$

• $S_1 : \underline{\underline{\text{begin} \ S_2 \ ; \ S_3 \ ; \ S_6 \ \underline{\underline{\text{end}}}}}^*$

Dans ce qui suit x est un élément de *item*, et t,q,q' des éléments de *item*^*.

### Traitement de la boucle "while".

Considéré comme un transformateur de prédicat (portant sur F et G), le programme est défini par :

(d₀) $P_o$ {programme} $Q_o$ où $P_o$ est le prédicat : F = w & G = e et $Q_o$ le prédicat : F = e & G = h*(w).

Comme le programme est de la forme :

```
while B₁ do S₁
```

où $B_1$ est le prédicat $\neg F$.empty, la règle (5) mentionnée dans l'annexe nous amène à chercher un prédicat $P_1$ (sur F et G) tel que de :

(d₁) $P_1 \{\underline{\underline{\text{while} \ B_1 \ do \ S_1}}\} P_1 \ & \ \neg B_1$

on puisse déduire (d₀). Si on suppose un tel P₁ trouvé, en vertu de la règle (5) la démonstration du programme se ramène à la démonstration de :

(d₂) $P_1 \ & \ B_1\{S_1\}P_1$

Pour pouvoir déduire d₀ à partir de d₁ il suffit en vertu des règles (1) et (2) de démontrer les deux implications :

$P_o$ implique $P_1$'

$P_1 \ & \ \neg B_1$ implique $Q_o$.

Nous prenons pour $P_1$ le prédicat :

il existe t,q dans *item*^* tels que w = tq & F = q & G = h*(t). En effet,

$F = w \ & \ G = e$ implique $w = ew \ & \ F = w \ & \ G = h^*(e)$, donc $P_o$ implique $P_1$.

D'autre part, $\neg B_1$ est équivalent à $F = e$, en vertu de la spécification de la programme itemqueue. Donc $P_1 \ & \ \neg B_1$ implique $q = e \ & \ t = w \ & \ F = e \ & \ G = h^*(w)$ qui implique $Q_o$.

Il reste à démontrer (d₂).

### Traitement du "if".

Il s'agit de l'instruction $S_3$ :

```
if X.test then G.append(X)
```

qui est sous la forme :
if B₂ then S₄ else S₅

où S₅ est l'instruction vide null.

La règle (4) nous amène à chercher deux prédicats P₃ et Q₃ tels que :

(d₃) P₃ & B₂ { S₄ } Q₃ et

(d₄) P₃ & ¬ B₂ { S₅ } Q₃

de telle façon que l'on puisse en déduire :

(d₅) P₃ { if B₂ then S₄ else S₅ } Q₃.

Nous allons montrer que les prédicats P₃ :

$X = x \& G = v$

et Q₃ :

$X = x \& G = \text{vh}(x)$

satisfait (d₃) et (d₄).

1°) Cas de (d₃) :

$X = x \& X.\text{test implique } h(x) = x.$

En utilisant la spécification de append :

$X = x \& G = v \{ G.append(X) \} G = vx,$

on a :

$X = x \& X.\text{test} \& G = v \{ G.append(X) \} X = x \& X.\text{test} \& G = vx$

d'où l'on déduit en utilisant la règle (2) :

$X = x \& X.\text{test} \& G = v \{ G.append(X) \} X = x \& G = \text{vh}(x)$

et en appliquant la règle (1), (d₃).

2°) Cas de (d₄) :

En vertu de la spécification du type item, si X = x alors X.test
équivaut à g(x) = true. Donc :

$X = x \& \neg X.\text{test implique } h(x) = e$

et par conséquent :

$G = v \& X = x \& \neg X.\text{test implique } G = \text{vh}(x).$

D'où :

$G = v \& X = x \& \neg X.\text{test} \{ \underline{\text{null}} \} G = \text{vh}(x) \& X = x$

et en appliquent la règle (1), (d₄).
## Traitement du corps du "while".

Le corps du "while" est de la forme :

```
begin S₂ ; S₃ ; S₆ end
```

Donc (d₂) se réécrit :

$P₁ \& B₁ \{ S₂ ; S₃ ; S₆ \} P₁.$

L'idée de la démonstration est d'appliquer successivement la règle (3) aux deux séquences :

$S : S₂ ; S₃$

$S ; S₆.$

### 1°) Séquence S :

En appelant $P₂$ le prédicat :

$F = xq' \& G = h^*(t) \& w = txq'$

on a :

$P₁ \& B₁$ implique $P₂$.

Des spécifications de copy et de head on déduit :

$F = xq' \{ F head \} F = xq' \& F head = x$

puis :

$F = xq' \{ X copy (F head) \} F = xq' \& X = x$

puis :

$P₂ \{ S₂ \} Q₂$

en appelant $Q₂$ le prédicat :

$F = xq' \& X = x \& G = h^*(t) \& w = txq'$.

En utilisant (d₅), la règle (3) et le fait que $Q₂$ implique $P₃$, on obtient :

$P₂ \{ S₂ ; S₃ \} Q₃.$

Du fait que $S₃$ ne manipule pas $F$ on peut en inférer :

(d₆) $P₂ \{ S₂ ; S₃ \} Q₃ \& F = xq'$

### 2°) Séquence finale :

De la spécification de remove on déduit :

$F = xq' \{ F remove \} F = q'$.
Le prédicat $Q_3$ :

$$X = x \ \& \ G = h^*(t)h(x)$$

ne concerne pas F qui est la seule variable manipulée par F.remove.

Il est donc laissé invariant par cette instruction et on a :

$$(d_7) \qquad Q_3 \ \& \ F = xq' \{ S_6 \} \ Q_3 \ \& \ F = q'$$

De $(d_6)$ et $(d_7)$ en appliquant la règle (3) on déduit :

$$(d_8) \qquad P_2 \{ S_2 ; S_3 ; S_6 \} Q_3 \ \& \ F = q'$$

Par définition de $h^*$ on a $h^*(t)h(x) = h^*(tx)$. Donc :

$$Q_3 \ \& \ F = q' \text{ implique } F = q' \ \& \ G = h^*(tx) \ \& \ w = txq' \\ \text{qui implique } P_1.$$

Des deux implications :

$$P_1 \ \& \ B_1 \text{ implique } P_2 \text{ et}$$

$$Q_3 \ \& \ F = q' \text{ implique } P_1$$

et de $(d_8)$ on déduit, en appliquant les règles (1) et (2)

$$P_1 \ \& \ B_1 \{ S_2 ; S_3 ; S_6 \} P_1$$

ce qui établit $(d_2)$.

On a donc démontré que si le programme se termine, alors il est solution du problème. En supposant que $S_2$ ; $S_3$ et $S_6$ se terminent toujours, on peut en plus montrer que la boucle "while" se termine en raisonnant sur la longueur de F, qui est par définition toujours positive, et qui décroit strictement.

### 4.4 Représentation du type itemqueue.

Une file est représentée au moyen d'un tableau Z de n variables du type item, et de deux variables entières m et tête. m contient la longueur de la file ; tête contient l'indice du premier élément de la file dans Z.

<figure><img src="image_5.png" /></figure>
C'est l'onde :

class itemqueue ;

begin

var (item) array Z[0:n-1] ;

var (integer) m, tête ;

procedure append(X) ; obs (item) X ;

begin

Z[mod(tête+m,n)]. copy(X) ;

m := m + 1

end ;

procedure remove ;

begin

tête := mod(tête+1, n) ;

m := m - 1

end ;

obs (boolean) procedure empty ;

empty := m = 0 ;

obs (item) procedure head ;

head.copy(Z[tête]) ;

m := 0 ; tête := 0

end

où mod(a, b) désigne le reste de la division entière de a par b.

Pour alléger l'écriture, on a conservé les notations traditionnelles pour les opérations sur les variables du types integer.

Toutes les files représentées de cette façon ont une longueur maximale n.

## 4.5 Démonstration de la conformité de la représentation du type itemqueue.

Dans le cas considéré, R est la collection des 3 variables Z, m, tête. A est une fonction à valeurs dans item* définie par :

$$A(R) = \sum_{i=1}^{i=m} Z[\text{mod}(\text{tête}+i-1, n)]$$
où $\sum_{i=1}^{i=m} a_i$ désigne la concaténation des m éléments de item $a_1, a_2, ..., a_m$ dans cet ordre ; par convention $\sum_{i=j}^{i=k} a_i = e$ lorsque l'on a $j > k$.

A n'est définie que si les conditions suivantes sont réalisées :

* la longueur de la file représentée ne peut excéder n ;

* tête est un indice dans Z.

D'où l'invariant I :

$$0 \le m \le n \ \& \ 0 \le \text{tête} \le n-1.$$

### 4.51 Conformité de la représentation de l'initialisation.

La transformation (à démontrer) :

$$\underline{\text{true}} \left\{ c_{<\text{initialisation}>} \right\} I \ \& \ A(R) = v_o$$

s'écrit dans le cas considéré :

$$\underline{\text{true}} \left\{ m := 0 ; \text{tête} := 0 \right\} \begin{array}{l} 0 \le m \le n \ \& \ 0 < \text{tête} < n-1 \ \& \\ \displaystyle \sum_{i=1}^{i=m} z[\text{mod}(\text{tête}+i-1,n)] = e. \end{array}$$

La substitution conformément à la règle (6) de $0$ à $m$ est de $0$ à tête dans le prédicat conclusion donne :

$$0 \le 0 \le n \ \& \ 0 \le 0 \le n-1 \ \& \ \sum_{i=1}^{i=0} z[\text{mod}(0+i-1,n)] = e$$

qui est universellement vrai c'est-à-dire égal à *true*.

### 4.52 Conformité de la représentation de append.

La procédure append étant associée dans la spécification type `itemqueue` à la transformation $f_1$, il faut démontrer :

$$I \ \& \ A(R) = v \left\{ c_{f_1} \right\} I \ \& \ A(R) = f_1(v,x),$$

où $x$ est la valeur du paramètre $X$, et $c_{f_1}$ la séquence :
$$Z[\mod(tête+m,n)] \cdot copy(X) ; m := m + 1.$$

D'une part, en ce qui concerne l'invariant :

$$O \leq m \leq n \text{ & } O \leq tête \leq n-1,$$

pour être vrai après exécution de :

$$m := m + 1$$

il exige avant cette exécution :

$$O \leq m+1 \leq n \text{ & } O \leq tête \leq n-1$$

qui, pour être vrai après exécution de :

$$Z[\mod(tête+m,n)] \cdot copy(X)$$

exige avant cette exécution :

$$O \leq m+1 \leq n \text{ & } O \leq tête \leq n-1$$

(en utilisant l'équivalence des spécifications (6) et (7) de l'assignation ou copie démontrée dans l'annexe).

Il n'est donc conservé par $c_{f_1}$ que si la pré-condition $m < n$ est vraie

(avant exécution de $c_{f_1}$).

D'autre part, on doit obtenir pour R après exécution de $c_{f_1}$ :

$$\sum_{i=1}^{i=m} Z[\mod(tête+i-1,n)] = vx$$

qui pour être vrai après exécution de :

$$m := m + 1$$

exige avant cette exécution :

$$\sum_{i=1}^{i=m+1} Z[\mod(tête+i-1,n)] = vx,$$

que l'on appelera P'. Ce prédicat P' se met sous la forme :

$$Z[\mod(tête+m,n)] = x \text{ & } P,$$

où, parce que $I \text{ & } m < n$, le prédicat P :

$$\sum_{i=1}^{i=m} Z[\mod(tête+i-1,n)] = v$$

ne concerne pas la variable $Z[\mod(tête+m,n)]$.
Donc, en vertu des spécifications de copy :

$$X = x \{ Y.\text{copy}(X) \} \quad Y = x,$$

pour que P' soit vrai après exécution de :

$$Z[\text{mod}(tête+m, n)].\text{copy}(X)$$

il suffit que avant cette exécution, P soit vrai. Or P est justement $A(R) = v$.

La conformité de la représentation de append est donc démontrée moyennant la pré-condition $m < n$.

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

### 4.53 Conformité de la représentation de remove.

La procédure remove étant associée dans la spécification du type itemqueue à la transformation $f_2$, il faut démontrer :

$$I \ \& \ A(R) = v \ \& \ v \neq e \{c_{f_2}\} \quad I \ \& \ A(R) = f_2(v),$$

où $c_{f_2}$ est la séquence :

$$tête := \text{mod}(tête+1, n) ; m := m - 1.$$

D'une part en ce qui concerne l'invariant :

$$0 \leq m \leq n \ \& \ 0 \leq tête \leq n-1,$$

pour être vrai après exécution de :

$$m := m - 1$$

il exige avant cette exécution :

$$0 \leq m-1 \leq n \ \& \ 0 \leq tête \leq n-1$$

qui, pour être vrai après exécution de :

$$tête := \text{mod}(tête+1, n)$$

exige avant cette exécution :

$$0 \leq m-1 \leq n$$

en vertu des propriétés de la fonction mod.

Il n'est donc conservé par $c_{f_2}$ que si la pré-condition $m > 0$ est vraie

(avant exécution de $c_{f_2}$). Cette pré-condition est équivalente à la

condition $v \neq e$ mentionnée ci-dessus.
D'autre part, on doit obtenir pour R, après exécution de $c_{f_2}$ :

$$ \sum_{i=1}^{i=m} Z[\mod(tête+i-1,n)] = f_2(v), $$

qui pour être vrai après exécution de :

$$ m := m - 1 $$

exige avant cette exécution :

$$ \sum_{i=1}^{i=m-1} Z[\mod(tête+i-1,n)] = f_2(v) $$

qui, pour être vrai après exécution de :

$$ tête := \mod(tête+1,n) $$

exige avant cette exécution :

$$ \sum_{i=1}^{i=m-1} Z[\mod(\mod(tête+1,n)+i-1,n)] = f_2(v) $$

qui équivaut au prédicat P :

$$ \sum_{i=1}^{i=m-1} Z[\mod(tête+i,n)] = f_2(v) $$

en vertu de la propriété de la fonction mod :

$$ \mod(\mod(a,n)+b,n) = \mod(a+b,n) $$

pour tous entiers relatifs a et b.

P se transforme en :

$$ \sum_{i=2}^{i=m} Z[\mod(tête+i-1,n)] = f_2(v) $$

qui, compte tenu de ce qu'on a $m > 0$, est impliqué par :

$$ \sum_{i=1}^{i=m} Z[\mod(tête+i-1,n)] = v. $$
La conformité de la représentation de remove est donc démontrée sans pré-condition, m > 0 (ou v ≠ e) exprimant simplement que $f_2$ est définie en v.

### 4.54 Conformité de la représentation de empty.

La fonction-procedure empty étant associée dans la spécification du type itemqueue à l'observation $g_1$, il faut démontrer :

$$I \ \& \ A(R) = v \ \{c_{g_1}\} \ I \ \& \ A(R) = v \ \& \ empty = g_1(v)$$

où $c_{g_1}$ est la séquence :

$$empty := m = 0.$$

D'une part, du fait que $c_{g_1}$ ne modifie aucune variable de R, il conserve $I \ \& \ A(R) = v$.

D'autre part, on doit obtenir après exécution de $c_{g_1}$ :

$$empty = g_1(v)$$

qui pour être vrai après exécution de :

$$empty := m = 0$$

exige avant cette exécution :

$$(m=0) = g_1(v)$$

qui résulte de :

$$(m=0) \text{ équivaut à } A(R) = e.$$

La conformité de la représentation de empty est donc démontrée sans pré-condition.

### 4.55 Conformité de la représentation de head.

La fonction procédure head étant associée dans la spécification du type itemqueue à l'observation $g_2$, il faut démontrer :

$$I \ \& \ A(R) = v \ \& \ v \neq e \ \{c_{g_2}\} \ I \ \& \ A(R) = v \ \& \ head = g_2(v)$$

où $c_{g_2}$ est la séquence :

head.copy(z[tête]).
D'une part, du fait que $c_{g_2}$ ne modifie aucune variable de R,
il conserve $I \& A(R) = v$.

D'autre part, on doit obtenir après exécution de $c_{g_2}$ :

$$head = g_2(v)$$

qui pour être vrai après exécution de :

$$head.copy(Z[tête])$$

exige avant cette exécution la véracité du prédicat P :

$$Z[tête] = g_2(v)$$

en vertu de la spécification de copy, et $v \neq e$ pour que $g_2(v)$ soit défini.

L'égalité $A(R) = v$ s'écrit :

$$\sum_{i=1}^{m} Z[\text{mod}(\text{tête}+i-1, n)] = v.$$

La condition $v \neq e$ implique qu'il existe q dans $item^*$ tel que $v = g_2(v)q$.

Cette condition implique aussi $m \geq 1$ et donc :

$$\sum_{i=1}^{m} Z[\text{mod}(\text{tête}+i-1, n)] = Z[\text{mod}(\text{tête}, n)] \sum_{i=2}^{m} Z[\text{mod}(\text{tête}+i-1, n)].$$

On déduit de l'égalité obtenue en portant ces deux résultats dans l'écriture
de $A(R) = v$ :

$$Z[\text{mod}(\text{tête}, n)] = g_2(v)$$

qui implique P compte tenu de l'invariant I. P est donc une conséquence
de :

$$I \& A(R) = v \& v \neq e.$$

La conformité de la représentation de head est donc démontrée
sans pré-condition.
4.6 Résultat obtenu.

Dans cet exemple, on est parti d'un programme que l'on a démontré à partir des spécifications des types itemqueue et item ; on a construit ensuite une représentation du type itemqueue, dont on a démontré qu'elle était conforme à sa spécification moyennant l'introduction d'une précondition pour la procédure append. Il faudrait donc reprendre la démonstration du programme afin de vérifier que cette pré-condition est vraie avant l'invocation de cette procédure. Dans le cas considéré, il est facile de s'en convaincre en constatant que la longueur de la file G est toujours inférieure à la longueur initiale de F, supposée inférieure ou égale à n. On peut alors appliquer le théorème de conformité.
# 5. CONCLUSIONS.

Ces conclusions sont relatives d'une part à la représentation choisie dans l'exemple et d'autre part à la méthode présentée.

## 5.1 Conclusions relatives à l'exemple traité.

Dans cet exemple, on a simplement représenté le type itemqueue. On aurait pu continuer ce travail en construisant une représentation du type item, dont il faudrait alors démontrer qu'elle est conforme à sa spécification ; cependant, cette représentation ne comporterait pas de description de ce qu'est un tableau de variables du type item. Cette omission correspond au point de vue selon lequel on considère que la structure de tableau est "universelle", c'est-à-dire que quel que soit le type T, on peut disposer de tableaux de variables de ce type.

Considérons la dépendance du type itemqueue vis à vis du type item :

* le modèle de itemqueue utilise le modèle de item ;

* la représentation de itemqueue utilise la spécification de item ;

* il n'y a pas d'autre relation entre itemqueue et item.

Nous laisserons de côté les changements de spécification. On ne peut considérer que deux sortes de changements du type item, qui laissent sa spécification inchangée :

1. on conserve l'ensemble *item* ; dans ce cas f ne peut être changée, en revanche on peut remplacer g par toute fonction de la forme : *item* → {true, false}, ce qui revient à changer de critère.

2. on change d'ensemble *item* ; dans ce cas f est encore imposée par l'équation fonctionnelle $f(x,y) = y$ ; g doit être encore une fonction de la forme : *item* → {true, false}.

Dans les deux cas, pourvu que les conditions mentionnées soient respectées, le changement n'affecte ni la démonstration du programme ni celle de la conformité de la représentation de itemqueue. Donc la représentation du type itemqueue exhibée est valide "quel que soit" le type item. On a donc défini une *structure* dont le type item est le paramètre mais on n'en a pas de matérialisation syntaxique au sens où on ne peut pas écrire :
`var (item) queue...`

de la même façon que l'on écrit :

`var (item) array...`

## 5.2 Conclusions relatives à la méthode.

L'existence de pré-conditions dans la démonstration de conformité
de la représentation d'un type peut être interprétée comme :

* une insuffisance de la spécification du type ;

* le non-respect de cette spécification.

Dans l'exemple traité, la limitation à n de la longueur des files de type
itemqueue ne figure que dans la représentation, le modèle correspondant à
des files de longueur illimitée. D'où la pré-condition $m < n$. On pourrait
éliminer cette pré-condition en faisant figurer la limitation à n de la
longueur des files du type itemqueue dans le modèle et dans la spécification
de ce type. Ceci se généralise. L'insuffisance de la spécification du type
itemqueue provient du fait que l'on a regardé son utilisation dans un seul
programme, où le problème de la longueur ne se posait pas (il se serait posé
si par exemple on avait regardé la partie du programme assignant une valeur
à F). En pratique on ne peut obtenir une spécification "suffisante" de item-
queue que lorsque l'on connait toutes les conditions de son utilisation. Ceci
se généralise également.

On peut soulever le problème de savoir en quels termes doit
être exprimée la spécification d'un type. Il existe au moins deux écoles :

1. celle de C.A.R. Hoare ([Hoare 72]), reprise dans cet exposé, qui utilise ce que nous avons appelé un modèle du type ;

2. celle de D.L. Parnas, ([Parnas 71A]) qui exprime l'effet de toute transformation en termes des observations avant et après invocation, ce qui supprime le modèle du type (la notion de type se déduit facilement de la notion de "module" définie par cet auteur).
Pour comparer ces deux méthodes, nous allons les expliciter dans le cas du type `itemstack` des variables qui sont les piles de variables du type `item`, en utilisant chaque fois notre système de notations.

Dans les deux méthodes on a la même spécification du type `itemstack` qui comporte :

* la déclaration des opérations suivantes :

`procedure push(X) ; obs(item)X`

`procedure pop`

`obs (boolean) procedure empty`

`obs(item) procedure top`

* les transformations de prédicat suivantes :

`true {var (itemstack) P} P = e`

`P = p & X = x {P.push(X)} P = f₁(p,x)`

`P = p {P.pop} P = f₂(p)`

`P = p {P.empty} P.empty = g₁(p)`

`P = p {P.top} P.top = g₂(p)`

où P est une variable de type `itemstack`, X une variable de type `item`, p un élément quelconque de l'ensemble `itemstack` et x un élément quelconque de l'ensemble `item` des valeurs possibles des variables du type `item`.

En revanche les modèles du type `itemstack` diffèrent dans les deux méthodes mais ont des caractéristiques communes :

* un ensemble de valeurs possibles noté `itemstack`,

* une valeur initiale e,

* des fonctions de la forme suivante :

`f₁ : itemstack × item → itemstack`

`f₂ : itemstack → itemstack`

`g₁ : itemstack → {true, false}`

`g₂ : itemstack → item`
Avec la première méthode on prend :

pour *itemstack* le monoïde libre *item*\*,

pour valeur initiale et l'élément neutre de ce monoïde,

pour fonctions :

$f_1(p,x) = px,$
lorsque p est de la forme qx, $f_2(p) = q$, autrement $f_2$ n'est pas
définie,

$g_1(p) = (p = e);$
lorsque p est de la forme qx, $g_2(p) = x$, autrement $g_2$ n'est pas
définie,

où p et q sont des éléments quelconques de *item*\* et x un élément quelconque
de *item*. Avec la deuxième méthode :

• *itemstack* est un ensemble qui contient au moins un élément noté e et qui permet l'existence de fonctions $f_1, f_2, g_1, g_2$ satisfaisant les équations fonctionnelles suivantes :

$f_2 \circ f_1(p,x) = p, f_2(e)$ étant non défini,

$g_2 \circ f_1(p,x) = x, g_2(e)$ étant non défini,

$g_1(p) = (p = e),$

pour tout p dans *itemstack* et tout x dans *item*.

Il semble que cette deuxième méthode très pratique dans certains cas parce
qu'elle évite de recourir à un modèle compliqué, soit difficile à utiliser
dans l'exemple du programme de sélection et exige en tout cas de repenser
la façon d'énoncer les prédicats.

REMERCIEMENTS.

Nous tenons à remercier MM. C. KAISER et C. PAIR pour leur lecture
attentive et leurs critiques constructives de cette étude, ainsi que MM. J.
ABRIAL et G. KAHN pour leurs remarques pertinentes.
# ANNEXE

## Instructions comme transformateurs de prédicats
(d'après [Hoare 69])

Une instruction S est une transformation portant sur des variables, elle est donc caractérisée par une relation entre les valeurs de ces variables avant exécution et les valeurs de ces mêmes variables après exécution, lorsque celle-ci se termine. Toutes les conséquences de cette relation peuvent se mettre sous la forme :

$$P\{S\}Q$$

où P et Q sont des prédicats portant sur (les valeurs de) ces variables ; cette écriture veut dire que si le prédicat P est vrai avant exécution de S et si S se termine, alors le prédicat Q est vrai après exécution de S. Vis à vis de l'implication des prédicats, on a les règles suivantes :

(1) $P\{S\}Q$ et P' implique P entraînent $P'\{S\}Q$

(2) $P\{S\}Q$ et $\Omega$ implique Q' entraînent $P\{S\}Q'$

On définit les opérateurs de composition "séquencement", "if", et "while" par les règles suivantes :

(3) $P\{S\}P'$ et $P'\{S'\}P''$ entraine $P\{S; S'\}P''$

(4) $P \& B\{S_1\}Q$ et $P \& \neg B\{S_2\}Q$ entraine $P\{\text{if } B \text{ then } S_1 \text{ else } S_2\}Q$

(5) $P \& B\{S\}P$ entraine $P\{\underline{\text{while}} \ B \ \underline{\text{do}} \ S\}P \ \& \ \neg B$.

Dans ces règles B est une condition dont l'évaluation est supposée ne pas modifier les variables. On peut utiliser d'autres opérateurs ("repeat",...) pourvu que l'on en donne une définition analogue.
En considérant tout ce que l'on sait dire sur les variables, on obtient une collection de prédicats Q possibles, et pour chacun d'eux un prédicat $P_o$ correspondant, qui est le plus faible (au sens de la relation d'ordre qu'est l'implication : si A implique B, B est plus faible que A) prédicat P tel que $P\{S\}Q$. On peut donc considérer l'instruction S comme un transformateur de prédicat :

$P_o = S(Q), \text{ pour tout Q possible.}$

Ainsi l'instruction d'assignation

$X := e$

où X est une variable et e une expression du même type que cette variable, sera définie comme le transformateur de prédicat :

$$ (6) \quad P_e \{ X := e \} P_X $$

où $P_X$ est un prédicat portant notamment sur la variable X et $P_e$ est le prédicat obtenu à partir de $P_X$ en y substituant e à toute occurrence de X. Par exemple, pour l'instruction d'assignation

$X := Y + 1$

on a la transformation de prédicat

$$ Y + 1 \geq 0 \{ X := Y + 1 \} X \geq 0 $$

ce qui signifie que si l'on veut avoir après exécution de cette instruction $X \geq 0$ vrai, il faut avant exécution avoir un prédicat vrai qui implique que $Y + 1 \geq 0$ soit vrai ; et de la même façon

$$ Y + 1 = 5 \{ X := Y + 1 \} X = 5. $$

La règle (6) est une spécification de l'instruction d'assignation. Cette spécification est équivalente à la spécification :

$$ (7) \quad e = x \{ X := e \} X = x $$

où y est un élément quelconque de l'ensemble des valeurs du type de la variable X. La démonstration se fait en deux étapes :

• (6) entraîne (7) : on prend pour $P_X$ le prédicat $X = x$ ; en y substituant e à toute occurrence de X, on obtient (7).

• (7) entraîne (6) : soit Q un prédicat quelconque sur la variable X; il est équivalent à un prédicat de la forme $X = x \& R(x)$ ou $R(x)$ est un prédicat concernant la valeur x, puisque la valeur d'une variable résume toutes ses propriétés ; pour qu'il soit vrai après exécution de $X := e$, il faut d'après (7) que $e = x \& R(x)$ soit vrai avant cette exécution (puisque $R(x)$ ne porte pas sur la variable modifiée X) ; ce dernier prédicat est précisément celui obtenu par (6) à partir de Q.
REFERENCES.

Dijkstra E.W.

73 : A simple axiomatic basis for programming language constructs.
*Note EWD372.*

Habermann N.

73 : Critical comments on the programming language PASCAL
*CMU-CS report, Pittsburgh, Oct. 1973.*

Hoare C.A.R.

69 : An axiomatic basis for computer programming.
CACM, 12, 10, (1969).

72 : Proof of correctness of data representations.
*Acta Informatica, 1* (1972).

Parnas D.L.

71 : Information distribution aspects of design methodology
*Proceedings IFIP Congress, 1971, pp. TA/3/26 - TA/3/30.*

71A: A technique for software module specification with examples.
*CMU-CS report, 1971 & C. ACM, May 1972, pp. 330-336.*