GLO-3004

Spécification formelle
et vérification de logiciels

Notes de cours
Automne 2016
Reproduites avec l’autorisation des auteurs

Module 2 :
Spécification formelle avec les langages Z et Perfect

Jean-Lou de Carufel et Josée Desharnais

Table des matières

1 Introduction 5

2 Rappels de théorie des ensembles et de logique 6

2.1 Théorie des ensembles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
2.1.1 Opérations sur les ensembles . . . . . . . . . . . . . . . . . . . . . . . 8
2.2 Logique, calcul propositionnel, calcul des prédicats . . . . . . . . . . . . . . . 10
2.2.1 Calcul propositionnel . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.2.2 Calcul des prédicats . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

3 Syntaxe du langage Z 13
3.1 Composantes d’une spécification Z . . . . . . . . . . . . . . . . . . . . . . . 13
3.1.1 Définition de types ou d’ensembles . . . . . . . . . . . . . . . . . . . 13
3.1.2 Définition de constantes . . . . . . . . . . . . . . . . . . . . . . . . . 15
3.2 Opérateurs en Z . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
3.2.1 Théorie des ensembles . . . . . . . . . . . . . . . . . . . . . . . . . . 16
3.2.2 Arithmétique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
3.2.3 Paires et relations binaires . . . . . . . . . . . . . . . . . . . . . . . . 17
3.2.4 Fonctions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
3.2.5 Suites . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
3.3 Schémas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3.3.1 Schéma qui représente l’état général du système (ou d’une partie du
système) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3.3.2 Schéma qui représente une opération . . . . . . . . . . . . . . . . . . 29
3.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30

4 Premier exemple : le dictionnaire 31

4.1 Description de l’exemple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
4.2 Analyse de la spécification . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32

5 Théorie du contrat 40
5.1 La notion de contrat . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
5.2 Applications en programmation orientée objets . . . . . . . . . . . . . . . . . 41
5.3 Applications en Z . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
5.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

2
6 Bibliothèque 45
6.1 Une spécification de la bibliothèque . . . . . . . . . . . . . . . . . . . . . . . 46
6.2 Tableau des préconditions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
6.3 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55

7 Document de spécification 56
7.1 Le document de spécification . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
7.2 Exemple : la Bibliotheque . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
7.3 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63

8 Perfect Developer 64
8.1 Quelques notations Perfect . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
8.2 Un aperçu de l’exemple de la bibliothèque . . . . . . . . . . . . . . . . . . . 66

9 Démonstration de propriétés 73
9.1 Vérification de domaine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
9.2 Théorème de l’état initial . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
9.3 Théorème des préconditions . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
9.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85

10 Vérification avec Perfect Developer 88

10.1 Obligations de preuves . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
10.2 Exemples de preuves non réalisées par Perfect Developer . . . . . . . . . . . . 89
10.3 Exemple 1 : une preuve de la banque d’articles . . . . . . . . . . . . . . . . . 89
10.4 Exemple 2 : une preuve du jeu de chiffres . . . . . . . . . . . . . . . . . . . . 91
10.5 Messages de PD . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92

11 Exemple de l’éditeur 94
11.1 Première solution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
11.1.1 Commentaires . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
11.2 Deuxième solution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
11.2.1 Commentaires . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
11.3 Troisième solution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
11.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109

12 Machine de radiothérapie 111

12.1 Présentation du projet . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112
12.2 Architecture du réseau et architecture du programme . . . . . . . . . . . . . 113
12.3 Logiciels et pièces utilisés . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
12.4 Méthode de développement . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
12.4.1 Écrire les besoins . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
12.4.2 Écrire la spécification formelle . . . . . . . . . . . . . . . . . . . . . . 115
12.4.3 Analyse de la spécification formelle . . . . . . . . . . . . . . . . . . . 116
12.4.4 Coder le programme . . . . . . . . . . . . . . . . . . . . . . . . . . . 116

3
 12.4.5 Tester et évaluer le programme . . . . . . . . . . . . . . . . . . . . . 117
12.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117

A Les fondements de Perfect Developer 118

4
Chapitre 1

Introduction

Die ganzen Zahlen hat Gott gemacht,

alles endere ist Menschenwerk.
L. Kronecker

Dans la première partie de cours, nous étudierons la spécification formelle en utilisant

le langage Z. Lors des semaines qui vont suivre, gardez toujours en tête que plusieurs des
principes que vous apprenez ne sont pas exclusifs au langage Z, mais qu’ils constituent plu-
tôt des principes de base en spécification formelle. On peut penser à des notions comme les
pŕeconditions, les postconditions ou les invariants. On peut aussi penser à des techniques de
démonstrations de propriétés, etc. Ce sont des concepts que nous étudierons avec le support
du langage Z, mais il ne faut jamais oublier qu’ils ne sont pas exclusifs à ce langage.

Les bases mathématiques nécessaires à l’étude du langage Z sont la théorie des ensembles
et la logique du premier ordre. Vous avez vu de nombreux résultats sur ces deux sujets en
IFT-1000 Logique et techniques de preuves ainsi qu’en MAT-1902 Mathématiques pour in-
formaticiens. Ces résultats vous seront très utiles pour bien comprendre le langage Z. La
difficulté ne sera pas dans la complexité des concepts utilisés. C’est votre capacité à modéli-
ser des programmes à l’aide de ces deux outils mathématiques qui sera davantage solicitée.
C’est habituellement là que l’on se cogne à quelques difficultés. Ces notes de cours ainsi que
les exercices proposés devraient vous aider à y parvenir.

Pour la présentation de la matière, nous utiliserons la même approche jusqu’à la fin de

cette partie. Nous alternerons les sections théoriques et les sections pratiques. Nous présen-
tons d’abord la théorie et ensuite, comment ces opérateurs et théorèmes nous permettent de
faire du Z. L’essentiel de cette matière est inspiré des deux livres suivants :
1. J. Jacky, The Way of Z, practical programming with formal methods, Cambridge, 1997.
2. B. Potter, J. Sinclair, D. Till, An Introduction to Formal Specification and Z, Prentice
Hall, 2e édition, 1996.
Un exemple important sera étudié plus loin, il s’agit de la spécification d’une bibliothèque.
Cet exemple est tiré de [2].

5
Chapitre 2

Rappels de théorie des ensembles et de

logique

Nous parlerons dans cette section de théorie des ensembles et de logique. Il ne s’agit
pas de mathématiques très avancées, par contre vous vous devez de très bien comprendre
chacune des définitions de base pour parvenir à bien modéliser les programmes à l’aide du
Z 1 . Nous en ferons un traitement intuitif pour commencer, autant dans la présentation des
concepts que dans les exercices.

Il ne s’agit pas d’une section trés chargée, on n’y trouve que les définitions de base, par
contre, les exercices sont très importants. Sauf peut-être pour l’opérateur F, il n’y a aucune
nouvelle matière. En ce sens, la série d’exercices est pratiquement plus importante que la
section elle-même.

2.1 Théorie des ensembles

D’abord, nous ne donnerons pas de définition formelle du concept d’ensemble. Nous di-
rons tout simplement qu’il s’agit d’une collection d’éléments. La notion d’ensemble est donc
définie de façon intuitive. On peut penser à plusieurs exemples d’ensembles.

Exemples:
1. E1 = {0, 2, 4, 6, 8}
2. E1 = {n ∈ N | n < 10 ∧ n est pair}
3. E2 = {0, 2, 4, 6, 8, ...}
4. E2 = {n ∈ N |n est pair}
1. Le logiciel utilisé pour spécifier avec le langage Z s’appelle Z-eves. Depuis l’hiver 2008, ce logiciel n’est
plus utilisé dans ce cours. Le langage Perfect et son outil ont pris sa place. Notez cependant que ces notes
font encore mention de cet outil.

6
 5. E3 = {chat, chien, oiseau, girafe}
6. E4 = {∅, {1}, {2}, {1, 2}, {1, 3}, {2, 3}}
Il est important de noter qu’en Z, les ensembles ne doivent contenir que des éléments du
même type. On ne pourrait pas avoir un ensemble qui contient des nombres et des couleurs
par exemple. Mathématiquement parlant, cet ensemble serait bien défini, mais Z ne reconnaît
pas ces ensembles. Il faudra toujours faire attention aux types des éléments quand viendra
le temps de faire des opérations sur les ensembles. Pour le moment, nous ne précisons pas ce
que l’on entend par “type” en Z ; nous reviendrons sur cette notion à la prochaine section.

Il y a un ensemble qui est particulier parce qu’il ne contient aucun élément. Il s’agit de
l’ensemble vide.

Définition 2.1.1 (Ensemble vide) L’ensemble qui ne contient aucun élément se nomme
ensemble vide et est noté ∅. La notation {} est aussi acceptée par Z.

Si un ensemble E contient un nombre fini d’éléments, on peut compter le nombre d’élé-

ments qu’il contient ( !).

Définition 2.1.2 (Cardinalité) Soit E un ensemble fini. La cardinalité de l’ensemble E

est le nombre d’éléments que E contient et est notée #E .

Exemples:
1. #E1 = 5
2. On ne peut pas écrire #E2 car E2 contient une infinité d’éléments.
3. #E3 = 4
4. #E4 = 6
5. #∅ = 0
Remarque: En théorie des ensembles, la notion de cardinalité d’un ensemble infini existe,
mais ce concept n’est pas reconnu par Z-eves. C’est pourquoi nous nous restreignons aux
ensembles finis quand nous parlons de cardinalité. Quand nous arriverons à la partie du
cours où il faut dompter le démonstrateur semi-automatique de Z-eves, plusieurs d’entre
vous auront oublié cette nuance et cela entraînera plusieurs problèmes (et des larmes pour
certains).

Définition 2.1.3 (Singleton) Un ensemble E est appelé singleton lorsque #E = 1.

Définition 2.1.4 (élément) Le fait qu’un élément x soit dans un ensemble E est noté
x ∈ E . Si toutefois x n’est pas élément de E , on écrit x 6∈ E .

7
Définition 2.1.5 (Inclusion, sous-ensemble) On dit qu’un ensemble E1 est inclus dans
un ensemble E2 si
x ∈ E1 =⇒ x ∈ E2 .
On peut aussi dire que E1 est un sous-ensemble de E2 . La notation utilisée est E1 ⊆ E2 .

Exemples:
1. 2 ∈ E1
2. 3 6∈ E1
3. 0 6∈ ∅
4. ∅ ∈ E4
5. E1 ⊆ E2
6. E2 ⊆ E2
7. ∅ ⊆ E3
8. ∅ ⊆ E4
9. {∅} ⊆ E4
Définition 2.1.6 (égalité) On dit que deux ensembles E1 et E2 sont égaux si leurs éléments
sont exactement les mêmes. Autrement dit, E1 est égal à E2 si
x ∈ E1 ⇐⇒ x ∈ E2 .
On le note alors E1 = E2 . S’ils ne sont pas égaux, on le note E1 6= E2 .
Lemme 2.1.7 Deux ensembles E1 et E2 sont égaux si et seulement si E1 ⊆ E2 et E2 ⊆ E1 .
Ce lemme peut sembler banal... en fait il l’est ! Il est présenté (comme plusieurs autres défi-
nitions d’ailleurs) en guise de rappel. Il sera indispensable tout au long de la session.

Exemples:
1. {0, 2, 4, 6, 8} = {n ∈ N | n < 10 ∧ n est pair}
2. {0, 2, 4, 6, 8} =
6 {n ∈ N | n est pair}

2.1.1 Opérations sur les ensembles

Voici les principales opérations sur les ensembles utilisées en Z.

Définition 2.1.8 (Union, intersection) L’ union de deux ensembles E1 et E2 est notée
E1 ∪ E2 et est obtenue par
E1 ∪ E2 = {x | x ∈ E1 ∨ x ∈ E2 }.
L’ intersection de deux ensembles E1 et E2 est notée E1 ∩ E2 et est obtenue par
E1 ∩ E2 = {x | x ∈ E1 ∧ x ∈ E2 }.

8
Définition 2.1.9 (Différence) La différence entre deux ensembles E1 et E2 est notée
E1 \ E2 et est obtenue par

E1 \ E2 = {x | x ∈ E1 ∧ x 6∈ E2 }.

Exemples:
1. {0, 2, 4, 6, 8} ∪ {1, 3, 5, 7, 9} = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}
2. {0, 2, 4, 6, 8} ∩ {1, 3, 5, 7, 9} = ∅
3. {0, 2, 4, 6, 8} \ {1, 3, 5, 7, 9} = {0, 2, 4, 6, 8}
4. {bleu, blanc, rouge} ∪ ∅ = {bleu, blanc, rouge}
5. {bleu, blanc, rouge} ∩ ∅ = ∅
6. {bleu, blanc, rouge} \ ∅ = {bleu, blanc, rouge}
Remarque: Pour ces trois opérateurs (∪, ∩ et \), les éléments des ensembles E1 et E2
doivent être du même type de sorte que le résultat consiste en un ensemble qui ne contienne
que des éléments du même type.

Définition 2.1.10 (Ensemble puissance) Soit E un ensemble. On note par P(E ) l’en-
semble des sous-ensembles de E .

En Z, il y a un symbole particulier pour désigner l’ensemble des sous-ensembles finis.

Définition 2.1.11 (Ensemble des sous-ensembles finis) Soit E un ensemble. On note
par F(E ) l’ensemble des sous-ensembles finis de E , autrement dit

F(E ) = {S ∈ P(E ) | S est fini}.

Exemples:
1. P(∅) = {∅}
2. P({1, 2}) = {∅, {1}, {2}, {1, 2}}
3. P({∅, 1, {1}}) = {∅, {∅}, {1}, {{1}}, {∅, 1}, {∅, {1}}, {1, {1}}, {∅, 1, {1}}}
4. P(P({soleil })) = {∅, {∅}, {{soleil }}, {∅, {soleil }}}
5. P(N) = {∅, {0}, {1}, ..., {0, 1}, {0, 2}, ..., {0, 1, 2}, {0, 1, 3}, ...} et cet ensemble contient
aussi les sous-ensembles infinis.
6. F(N) = {∅, {0}, {1}, ..., {0, 1}, {0, 2}, ..., {0, 1, 2}, {0, 1, 3}, ...} et cet ensemble ne con-
tient pas les sous-ensembles infinis.
7. F({1, 2}) = {∅, {1}, {2}, {1, 2}}

Définition 2.1.12 (Produit cartésien) Soient E et F deux ensembles. Le produit carté-

sien de E et F , noté E × F est tel que

E × F = {(e, f ) | e ∈ E ∧ f ∈ F }.

9
Exemples:
1. {1, 2} × {a} = {(1, a), (2, a)}
2. ∅ × N = ∅
3. {1} × N = {(1, 0), (1, 1), (1, 2), (1, 3), ...}

Remarque: Pour ces trois opérateurs (P, F et ×), si les ensembles sont bien typés (mais
pas nécessairement identiquement typés), le résultat est correctement typé. Pourquoi ? Nous
verrons l’intuition qui se cache derrière ce fait dans le prochain chapitre.

2.2 Logique, calcul propositionnel, calcul des prédicats

L’autre outil fondamental en Z est la logique mathématique. Avec la théorie des ensembles,
elle permet de bien comprendre tout le langage Z.

2.2.1 Calcul propositionnel

Les variables utilisées en calcul propositionnel sont appelées variables propositionnelles.

On associe un symbole aux principales expressions utilisées dans le raisonnement mathéma-
tique. On les appelle les connecteurs logiques.

Le nombre 1 n’est pas premier. ¬(Le nombre 1 est premier.)

3 = 3 et 4 < 15 3 = 3 ∧ 4 < 15
3 ≤ 2 ou 3 > 2 3≤2∨3>2
Si 5 est pair, alors 5 est divisible par 2 5 est pair → 5 est divisible par 2
3 < 4 si et seulement si 4 > 3 3<4 ↔4>3

Définition 2.2.1 (Table de vérité) À chaque connecteur logique, on associe une table de
vérité représentant l’ensemble des valeurs de vérité possibles.

Exemples: Voici la sémantique des cinq connecteurs.

1. Négation
p (∼p)
V F
F V
2. Conjonction
p q (p ∧ q)
V V V
V F F
F V F
F F F

10
 3. Disjonction
p q (p ∨ q)
V V V
V F V
F V V
F F F
4. Conditionnelle
p q (p → q)
V V V
V F F
F V V
F F V
5. Biconditionnelle
p q (p ↔ q)
V V V
V F F
F V F
F F V

2.2.2 Calcul des prédicats

Dans le calcul des prédicats, on utilise les outils du calcul propositionnel avec des quantifi-
cateurs. On a alors des variables, des connecteurs logiques, des prédicats et des quantificateurs
(∀ et ∃). Par exemple, dans l’énoncé
∀ x : N • (x < x + 1 ∧ x 4 ≥ 2x 3 − x 2 ),
x est une variable, ∧ est un connecteur logique, (x < x + 1 ∧ x 4 ≥ 2x 3 − x 2 ) est un prédicat
et ∀ est un quantificateur. Mais nous n’insisterons pas sur ces termes et de toutes façons,
vous les avez déjà rencontrés dans d’autres cours.

En Z, lorsque l’on quantifie sur une variable, il faut toujours indiquer dans quel ensemble
est choisie cette variable. Par exemple, on n’écrira pas ∀ n • n + 1 > n. On va plutôt écrire
∀ n : N • n + 1 > n. Plusieurs d’entre vous oublierez aussi cette remarque lorsque viendra
le temps d’utiliser le démonstrateur semi-automatique et l’idéal serait de toujours l’avoir en
tête. La notation la plus générale acceptée par Z est la suivante.
∀ x : E | p(x ) • A(x )
∃ x : E | p(x ) • A(x )
Cette notation vous rappelle probablement celle de IFT-1000 Logique et techniques de
preuve.

11
 Pour qu’une expression de la forme ∀ x : E | p(x ) • A(x ) soit vraie, il faut que le prédicat
A(x ) soit vrai quel que soit x ∈ E qui satisfait p(x ).

Pour qu’une expression de la forme ∃ x : E | p(x ) • A(x ) soit vraie, il doit exister un
x ∈ E qui satisfait p(x ) et qui rend le prédicat A(x ) vrai.

12
Chapitre 3

Syntaxe du langage Z

Comme le Z n’est pas exécutable, on ne peut pas vérifier si le code que l’on écrit est
bon de la même façon qu’avec un compilateur C par exemple. On ne peut donc pas faire
d’essais ou de simulations pour s’assurer que ce que l’on a écrit représente réellement ce
qui doit être représenté. Il faut donc se fier à notre bonne connaissance des opérateurs.
C’est pourquoi il est important d’être habile avec les concepts de théorie des ensembles et de
logique mathématique ainsi qu’avec tous les opérateurs qui seront présentés dans ce chapitre.

La bonne nouvelle est que la liste des opérateurs disponibles en Z est relativement suc-
cinte. Dans ce chapitre, nous verrons l’essentiel des opérateurs nécessaires pour cette partie
du cours. Bien qu’ils soient peu nombreux, ils sont extrêmement expressifs.

Nous choisissons de tous les présenter en bloc pour que vous puissiez immédiatement en
avoir un aperçu. Les exemples, les exercices et les laboratoires des prochaines semaines vous
aideront à les maîtriser. Il ne faut pas oublier non plus qu’à la base, ils ne font intervenir que
des concepts très simples que vous avez déjà étudiés (plus en profondeur même). Comme il
a déjà été mentionné, la nouveauté dans ce cours est l’utilisation que nous en faisons.

3.1 Composantes d’une spécification Z

Une spécification en Z est formée de

— définitions globales : définitions de types, d’ensembles fixés, de constantes,
— schémas qui peuvent représenter des états ou des opérations (Sect. 3.3, page 28).

3.1.1 Définition de types ou d’ensembles

Il y a plusieurs façons de définir des types ou des ensembles en Z. Voyons d’abord les
types.
1. Le seul ensemble de nombres déjà défini comme type en Z est Z.

13
 2. On peut déclarer (comme dans l’exemple du dictionnaire, voir Chap. 4) un type de
la façon suivante.

[TYPE ]

3. On peut définir un type en énumérant ses éléments un à un :

TYPE ::= Marie | Marc | Denis

On a alors que l’ensemble {Marie, Marc, Denis} s’appelle TYPE et qu’il ne peut pas
contenir d’autres éléments.
Voici maintenant différentes façons de définir un ensemble. Ces opérateurs ne donnent
habituellement pas naissance à un type.
1. Les ensembles déjà définis en Z sont {} et N = {n : Z | n ≥ 0}.
2. On peut identifier un intervalle de nombres de la façon suivante

INTERVALLE == 42..55

qui correspond à INTERVALLE = {42, 43, 44, ..., 55}.

3. On peut utiliser les opérateurs ∪, ∩, \, ×, P ou F. Par exemple, on peut écrire la chose
suivante.

ENSEMBLE == 42..55 ∩ 23..40

Il ne faut pas oublier que les opérateurs ∪, ∩ et \ doivent être utilisés sur des ensembles
dont les éléments sont de même type.
4. De façon générale, on peut utiliser la notation

ENSEMBLE == {x : E | p(x ) • f (x )}

où E est un ensemble, p est un prédicat et f est une fonction dont le domaine est E .
Il s’agit alors de l’ensemble de tous les f (x ) pour les x ∈ E tels que p(x ) est vrai. Les
raccourcis suivants sont acceptés :

{x : E • f (x )}

qui correspond à {x : E | true • f (x )} et

{x : E | p(x )}

qui correspond à {x : E | p(x ) • x }.

5. On peut définir un ensemble à l’aide de la notation suivante.

Declaration
Predicat

14
 6. Pour définir un ensemble de couples (pris par exemple dans E × F ), la notation
d’ensemble (no 4 de la page précédente) se généralise :

ENSEMBLE == {x : E ;y : F | p(x , y) • (x , y)}

qui peut être abrégé en {x : E ;y : F | p(x , y)}. Autrement dit l’expression x : E ;y : F

indique de prendre des couples. De plus, si E = F , on peut écrire :

ENSEMBLE == {x , y : E | p(x , y) • (x , y)}.

À la place de (x , y) dans ENSEMBLE ci-haut, on peut mettre n’importe quelle fonc-

tion de x et y. Par exemple

ENSEMBLE == {x : Z ;y : N | y > 1 • x 2 + 7y 2 }
ENSEMBLE == {x : N ;y : Z | −1 ≤ x < y < 2) • (x 2 , x + y)}

3.1.2 Définition de constantes

Il peut être utile de déclarer des constantes (par exemple la constante EntierMax est
souvent pratique) ; notez qu’un ensemble peut aussi être constant. La façon générale de
déclarer une constante est la suivante.

Declaration
Predicat

Il faut toujours déclarer une constante en identifiant son type. Les déclarations ont donc
toujours la forme suivante.

constante : TYPE

Attention, si l’on écrit x : Z, on déclare un nombre entier. Si l’on écrit x : P(Z ), on déclare
un ensemble d’entiers.

Le racourci suivant est accepté par Z.

Declaration

Il représente la déclaration suivante.

Declaration
true

15
3.2 Opérateurs en Z
Voici l’ensemble des opérateurs et/ou symboles à connaître. À peu de choses près, il
s’agit de tous les opérateurs disponibles en Z. Nous avons regroupé les différentes fonctions
par catégorie. Le but est de simplifier la présentation, mais vous remarquerez que certains
pourraient apparaître à plus d’un endroit.

3.2.1 Théorie des ensembles

Vous connaissez déjà les opérateurs et/ou symboles suivants : {}, ∪, ∩, \, # (cardinalité
d’un ensemble fini), ×, P, F, ∈, 6∈, ⊂ et ⊆. N’oubliez pas que deux ensembles doivent être
identiquement typés pour que l’on puisse en faire l’union, l’intersection ou la différence.

3.2.2 Arithmétique
Voici un tableau qui résume les opérateurs arithmétiques disponibles.

Exemple(s) Commentaire
Z Z = {..., −2, −1, 0, 1, 2, ...} - C’est un type
N N = {0, 1, 2, ...} - Ce n’est pas un type
+ 222 + 7 = 229
− 5 − 90 = −85
∗ 5 ∗ 7 = 35
div 12 div 7 = 1 - On ne peut pas diviser par 0 !
12 div 4 = 3
mod 12 mod 7 = 5 - On ne peut pas calculer en mod 0
12 mod 4 = 0
12 mod 1 = 0
−1 mod 2 = 1
4 mod −2 = 0
< 3<4
≤ 3≤4
4≤4
> 13 > 4
≥ 13 ≥ 4
4≥4
min min{−1, 41, 121, 2005} = −1 - L’ensemble doit être non vide
min N = 0 - Le minimum de l’ensemble doit exister
max max{−1, 41, 121, 2005} = 2005 - L’ensemble doit être non vide
- Le maximum de l’ensemble doit exister
.. −3..4 = {−3, −2, −1, 0, 1, 2, 3, 4}

16
3.2.3 Paires et relations binaires
C’est à partir d’ici qu’il faut réfléchir et chercher à faire des liens entre les opérateurs
disponibles ainsi que les différentes représentations équivalentes possibles. Plus vous serez
habiles à jongler avec ces notions, plus vous serez à l’aise à faire de la modélisation de pro-
grammes avec le langage Z.

Nous parlerons ici de paires et de relations binaires. Qu’est-ce qu’une relation binaire ?
Qu’est-ce qu’une relation ? Une relation, c’est un ensemble. Plus précisément, un ensemble
d’associations. Pensons à Paires de l’exemple du Dictionnaire (voir Chap. 4). C’est effec-
tivement une relation. On parle de relation binaire pour insister sur le fait qu’il s’agit de
relation faisant intervenir deux ensembles : un ensemble de départ et un ensemble d’arrivée.

Définition 3.2.1 En Z, on utilise la notation X ↔ Y pour représenter l’ensemble de toutes

les relations entre les ensembles X et Y . Les ensembles X et Y doivent être fixés (ne pas
être des variables) pour que la notation soit acceptée.

Le graphe très général d’une relation pourrait ressembler au suivant.

Quand on regarde ce graphe et que l’on pense à une relation comme étant un ensemble
d’associations entre les éléments d’un ensemble X et les éléments d’un ensemble Y , on peut
voir qu’une relation est un sous-ensemble de X × Y . Justement, on a l’égalité suivante.

X ↔ Y = P(X × Y )

Attention, la notation X ↔ Y représente l’ensemble de TOUTES les relations entre X et Y

(où le domaine est inclus dans X et l’image dans Y ). Quand on veut déclarer UNE relation
R de X vers Y , on utilise la syntaxe suivante.

R:X ↔Y

C’est une nuance bien simple, mais elle a tendance à se faire oublier avec le temps.

17
 On parle beaucoup de couples et d’associations, voici deux notations possibles pour re-
présenter des couples de X × Y .

(x , y)
x 7→ y

La notation (x , y) fait penser à un couple, alors que la notation x 7→ y fait penser davantage
à une association, mais elles sont totalement équivalentes. En fait, on a

(x , y) = x 7→ y

quels que soient x et y.

Exemple: Prenons la relation R = {(1, 5), (3, −4), (3, 7)}. On a (1, 5) ∈ R, 1 7→ 5 = (1, 5)
et (3 7→ −4) ∈ R.

Ensuite, on a les opérateurs first et second qui peuvent être utiles. Voici leur définition.

Définition 3.2.2 Soient X et Y des ensembles fixés. Prenons (x , y) ∈ X × Y , on a

first(x , y) = x
first(x 7→ y) = x
second (x , y) = y
second (x 7→ y) = y

Exemple: Prenons la relation R = {(1, 5), (3, −4), (3, 7)}. On a

first(1, 5) = 1
first(3 7→ −4) = 3
first(3, 7) = 3
second (1 7→ 5) = 5
second (3, −4) = −4
second (3 7→ 7) = 7

Voyons maintenant deux opérateurs utilises, les opérateurs de domaine et d’image.

Définition 3.2.3 Soient X et Y des ensembles fixés. Prenons R ∈ X ↔ Y , on a

dom R = {x ∈ X | ∃ y : Y • (x , y) ∈ R}
ran R = {y ∈ Y | ∃ x : X • (x , y) ∈ R}

La notation ran pour l’image vient de l’anglais “range”.

18
Exemple: Prenons la relation R = {(1, 5), (3, −4), (3, 7)}. On a

dom R = {1, 3}
ran R = {−4, 5, 7}

Les prochains opérateurs que nous allons présenter sont moins standards. Il s’agit d’opé-
rateurs de restriction (et de corestriction) de domaine ou d’image.

Définition 3.2.4 Soient X et Y des ensembles. Prenons aussi E ⊆ X et F ⊆ Y . Soit

finalement R ∈ X ↔ Y , on a

E CR = {x :X ;y :Y |x ∈E ∧ (x , y) ∈ R}
E−CR = {x :X ;y :Y |x 6∈ E ∧ (x , y) ∈ R}
RBF = {x :X ;y :Y |y ∈F ∧ (x , y) ∈ R}
R−BF = {x :X ;y :Y |y 6∈ F ∧ (x , y) ∈ R}

Dans le cas de l’opérateur C, on se concentre sur les associations de R dont la première

composante est élément de E . C’est une restriction de domaine. Pour l’opérateur − C, on se
concentre sur les associations de R dont la première composante n’est pas élément de E . On
va parler alors de corestriction de domaine (ou restriction négative). On a la nomenclature
correspondante pour l’image. Un truc mémotechnique pour mémoriser ces symboles : la par-
tie verticale du triangle est toujours du côté de la relation alors que l’angle opposé pointe
vers l’ensemble à retirer ou auquel on veut restreindre la relation. On peut écrire : E CR BF .

Exemples: Prenons

R:Z↔Z
E : PN
F : PZ
R = {(1, 2), (1, 7), (2, 5), (7, −1), (7, −71)}
E = {1, 3, 5}
F = {x : Z | x < 3}

E CR = {(1, 2), (1, 7))}

E−CR = {(2, 5), (7, −1), (7, −71)}
RBF = {(1, 2), (7, −1), (7, −71)}
R−BF = {(1, 7), (2, 5)}

Continuons notre exploration des opérateurs en Z dans le contexte des paires et des
relations binaires. On a l’opérateur ∼ de transposition qui est défini comme suit.

19
Définition 3.2.5 Soient X et Y des ensembles fixés. Prenons R ∈ X ↔ Y , on a

R ∼ = {y : Y ;x : X | (x , y) ∈ R}

On a donc que R ∼ ∈ Y ↔ X . Cet opérateur transforme l’ensemble de départ en ensemble

d’arrivée et vice-versa.

Exemple: Prenons la relation R = {(1, 5), (3, −4), (3, 7)}. On a

R ∼ = {(−4, 3), (5, 1), (7, 3)}

Un autre opérateur, la composition de relations.

Définition 3.2.6 Soient X , Y et Z des ensembles fixés. Prenons R ∈ X ↔ Y et S ∈ Y ↔

Z . On a
R o9 S = {x : X ;z : Z | ∃ y : Y • (x , y) ∈ R ∧ (y, z ) ∈ S }

Intuitivement, on peut voir cet opérateur de composition comme l’ensemble des chemins
possibles entre les ensembles aux deux extrémités.

Exemples:
1. Prenons

R, S : Z ↔ Z
R = {(1, 2), (1, 7), (2, 5), (7, −1), (7, −71)}
S = {(−1, 2), (1, 7), (2, 5), (3, 3)}

R o9 S = {(1, 5), (7, 2)}

2. Prenons

20
 R, S : Z ↔ Z
R = {(1, 2), (1, −2), (3, 4), (3, −4), (5, 6), (5, −6)}
S = {(1, 1), (1, −1), (3, 1), (3, −1), (5, 1), (5, −1)}

R o9 S = {}
3. Prenons

R, S : Z ↔ Z
R = {(1, 1), (2, −2), (3, 3), (4, −4), (5, 5), (6, −6)}
S = {(1, 1), (1, −1), (2, 2), (2, −2), (3, 3), (3, −3), (4, 5), (4, −5)}

R o9 S = {(1, 1), (1, −1), (3, 3), (3, −3)}

Finalement l’opérateur de mise à jour.
Définition 3.2.7 Soient X et Y des ensembles fixés. Prenons R, S ∈ X ↔ Y . On a

R ⊕ S = ((dom S ) −
C R) ∪ S (3.1)

Il s’agit d’une mise à jour. Les anciennes données sont stockées dans R et on met à jour avec
S qui est considéré comme l’information plus récente. Si l’on décortique la formule (3.1),
on peut voir que l’on garde (dans R) toute l’information dont le domaine diffère de celui
de S et la mise à jour est faite avec le ∪S . Le tout apparaît plus clairement avec des exemples.

Exemples:
1. Prenons

R, S : Z ↔ Z
R = {(1, 2), (1, 7), (2, 5), (7, −1), (7, −71)}
S = {(−1, 2), (1, 7), (2, 5), (3, 3)}

R ⊕ S = ((dom S ) −
C R) ∪ S
= {(7, −1), (7, −71)} ∪ S
= {(−1, 2), (1, 7), (2, 5), (3, 3), (7, −1), (7, −71)}

2. Prenons

R, S : Z ↔ Z
R = {(1, 2), (1, −2), (3, 4), (3, −4), (5, 6), (5, −6)}
S = {(1, 1), (1, −1), (3, 1), (3, −1), (5, 1), (5, −1)}

21
 R ⊕ S = ((dom S ) C− R) ∪ S
= {} ∪ S
= {(1, 1), (1, −1), (3, 1), (3, −1), (5, 1), (5, −1)}

3. Prenons

R, S : Z ↔ Z
R = {(1, 1), (2, −2), (3, 3), (4, −4), (5, 5), (6, −6)}
S = {(1, 1), (1, −1), (2, 2), (2, −2), (3, 3), (3, −3), (4, 5), (4, −5)}

R ⊕ S = ((dom S ) C− R) ∪ S
= {(5, 5), (6, −6)} ∪ S
= {(1, 1), (1, −1), (2, 2), (2, −2), (3, 3), (3, −3), (4, 5), (4, −5), (5, 5), (6, −6)}

3.2.4 Fonctions

On a vu précédemment qu’une relation est un ensemble d’associations. Il n’y a aucune

restrictions sur les associations en question. Certaines contraintes sont utiles, comme celles
qui mènent à la définition de fonction. Qu’est-ce qu’une fonction ? Il s’agit d’une relation
dans laquelle chaque point de départ a au plus un point d’arrivée. Une image vaut mille mots.

Note au lecteur attentif, la notion de fonction en Z est quelque peu différente de celle que
l’on rencontre habituellement dans plusieurs livres. Fréquemment, on rencontre une définition
qui dit qu’une fonction doit être totale et déterministe. Bien sûr, le déterminisme est crucial.
Par contre, on permet aux fonctions d’être partielles.
Pour des ensembles X et Y fixés, il y a un opérateur qui représente l’ensemble de toutes
les fonctions de X dans Y . En fait, en Z, on doit distinguer entre fonction totale et fonction

22
partielle. Une fonction totale est une fonction où TOUS les éléments de X sont associés à un
élément de Y . Une fonction partielle est une fonction où pas nécessairement tous les éléments
de X sont associés à un élément de Y (on accepte même la fonction vide comme fonction
partielle, c’est-à-dire la fonction représentée par l’ensemble vide). Bref, nous sommes dans la
même situation qu’en IFT-1000 Logique et techniques de preuves. Nous présentons le tout
sous la forme d’une définition ; nous en profitons pour définir formellement les notions de
fonctions totales et fonctions partielles 1 .
Définition 3.2.8 (Fonction) Soient X et Y des ensembles fixés. On note X → Y l’en-
semble de toutes les fonctions totales de X dans Y . On note X →
7 Y l’ensemble de toutes
les fonctions partielles de X dans Y . Formellement, on a
X →Y = {f : X ↔ Y | ∀ x : X • #({x } C f ) = 1}
X →
7 Y = {f : X ↔ Y | ∀ x : X • #({x } C f ) ≤ 1}
Si (x , y) ∈ f , l’expression f (x ) est égale à y.
Comme chacun le sait probablement, il existe différents types de fonctions. Il y a les
fonctions injectives, surjectives, bijectives, on va même parler de fonctions finies. Il existe
des symboles pour toutes ces sortes de fonctions. Chaque fois (sauf pour le cas de la fonction
bijective), il y a la version fonction partielle et la version fonction totale.

Commençons avec la fonction injective. Une fonction injective est une fonction qui n’a
pas la même image pour deux éléments différents du domaine, en voici une représentation
graphique.

Une définition possible (version totale/partielle) est la suivante.

Définition 3.2.9 (Fonction injective) Soient X et Y des ensembles fixés. On note X 
Y l’ensemble de toutes les fonctions injectives totales de X dans Y . On note X  7 Y
l’ensemble de toutes les fonctions injectives partielles de X dans Y . Formellement, on a
X Y = {f : X → Y | ∀ x1 , x2 : X • x1 6= x2 ⇒ f (x1 ) 6= f (x2 )}
7 Y
X  = {f : X →
7 Y | ∀ x1 , x2 : dom f • x1 6= x2 ⇒ f (x1 ) 6= f (x2 )}
1. Il y a plusieurs définitions équivalentes possibles.

23
 Poursuivons avec la fonction surjective. Une fonction surjective est une fonction dont
tous les éléments de l’image sont atteints, en voici une représentation graphique.

Une définition possible (version totale/partielle) est la suivante.

Définition 3.2.10 (Fonction surjective) Soient X et Y des ensembles fixés. On note
X → → Y l’ensemble de toutes les fonctions surjectives totales de X dans Y . On note X →
→7 Y
l’ensemble de toutes les fonctions surjectives partielles de X dans Y . Formellement, on a
X →
→Y = {f : X → Y | ∀ y : Y • (∃ x : X • f (x ) = y)}
X →
→
7 Y = {f : X →
7 Y | ∀ y : Y • (∃ x : dom f • f (x ) = y)}
On peut mettre injectivité et surjectivité ensemble pour donner naissance aux fonctions
bijectives, voici une représentation graphique.

Une définition possible (version totale seulement 2 ) est la suivante.

Définition 3.2.11 (Fonction bijective) Soient X et Y des ensembles fixés. On note
→ Y l’ensemble de toutes les fonctions bijectives de X dans Y . Formellement, on a
X 
→ Y = {f : X → Y | f ∈ X  Y ∧ f ∈ X →
X  → Y}
2. L’idée de la bijection n’est pas sans rappeler l’idée d’équivalence ou de correspondance très intime entre
deux ensembles. Pour cette raison, le concept de bijection partielle n’existe pas.

24
 Finalement, il existe deux autres symboles pour représenter des ensembles de fonctions en
Z. Ils permettent de représenter deux ensembles de fonctions finies (on entend par fonction
finie, une fonction qui admet un nombre fini d’associations). Pour X et Y deux ensembles
fixés,
X → 77 Y
représente l’ensemble des fonctions partielles finies et

77 Y
X 

représente l’ensemble des fonctions injectives partielles finies.

On peut résumer le tout dans le tableau suivant (pour X et Y des ensembles fixés).

Fonction Contraintes
Nom Symbole dom f ran f
Fonction totale X →Y =X ⊆Y
Fonction partielle X →7 Y ⊆X ⊆Y
Injection totale X Y =X ⊆Y
Injection partielle X  7 Y ⊆X ⊆Y
Surjection totale X →
→Y =X =Y
Surjection partielle X →
→ 7 Y ⊆X =Y
Bijection →Y
X  =X =Y
Fonction partielle finie X → 77 Y ⊆X ⊆Y
Injection partielle finie X 77 Y ⊆X ⊆Y

Remarques:
1. Il ne faut jamais oublier qu’une fonction, c’est avant tout un ensemble d’associations.
On parle donc d’un exemple très particulier de relation (binaire). Conclusion : TOUS
les opérateurs que nous avons vus à la section précédente s’appliquent. Attention ! Ils
s’appliquent, mais rien ne garantit que les ensembles de fonctions que nous avons vues
sont fermés 3 par rapport à tous ces opérateurs. Voici un exemple. Prenons les deux
fonctions suivantes

f = {(1, 3), (2, 5)}

g = {(1, 2)}

7 N. Pourtant, en leur appliquant différents opérateurs

qui sont des fonctions dans N 
on n’obtient pas nécessairement un élément de N  7 N ! En effet, prenons

f ∪ g = {(1, 2), (1, 3), (2, 5)}

3. Ces opérateurs appliqués à des fonctions retournent-ils des fonctions ?

25
 le résultat n’est même pas une fonction, c’est une relation ! Par contre, dans certains
cas, on retombe sur nos pattes.

f ∩ g = {}
f ⊕ g = {(1, 2), (2, 5)}

La morale de cette histoire : il est tout à fait possible d’utiliser tous les opérateurs
disponibles, mais il faut toujours porter attention au type du résultat obtenu.
2. Concernant les fonctions finies et infinies, les opérateurs →, →, 7 , ,7 →→, → →7 et
→ que nous avons rencontrés au début de cette section représentent l’ensemble de
TOUTES les fonctions qui respectent certaines propriétés. Elles contiennent donc les
fonctions finies et les fonctions infinies. En résumé, soient X et Y des ensembles, alors
on a

X →7 Y & X →
77 Y
7 Y
et X  77 Y.
& X 

3.2.5 Suites

Après avoir regardé les relations de plus près, nous avons vu que certaines d’entre elles
méritaient de porter un nom particulier : les fonctions. Certaines de ces fonctions sont mon-
tées en grades portant le titre de fonctions injectives, surjectives ou bijectives. Il y a des
fonctions encore plus “pointues” qui existent, il s’agit des suites 4 . Regardons immédiatement
la définition formelle que nous expliquerons ensuite.

Définition 3.2.12 (Suite) Soit X un ensemble fixé. On note seq X l’ensemble de toutes
les suites finies sur X . Formellement, on a

seq X = {s : N →
7 7 X | dom s = 1..#s}

Soient x1 , x2 , ..., xn ∈ X , la suite {(1, x1 ), (2, x2 ), ..., (n, xn )} peut être notée

hx1 , x2 , x3 , ..., xn i

et la suite vide peut être notée {} ou hi.

Remarques:
1. Qu’est-ce que tout cela signifie ? D’abord, une suite sur X est une fonction partielle
finie dont le domaine est inclus dans N et dont l’image est incluse dans X . Ce n’est
pas tout. Le domaine doit être un intervalle (fini) de nombres naturels et il doit
commencer à 1, la seule exception possible étant la suite vide.
4. Le langage Z nous restreint à l’utilisation des suites finies.

26
 2. Bien que la notation h·i soit disponible, il est toujours permis d’utiliser la notation
où l’on énumère les couples avec (·, ·) ou encore d’utiliser la notation avec la flèche
(· 7→ ·). L’avantage de la notation h·i est d’insister sur le fait que nous manipulons
des suites.
3. La remarque de la fin de la section précédente s’applique ici aussi. C’est-à-dire que
l’on peut utiliser tous les opérateurs qui ont été définis jusqu’à maintenant non seule-
ment sur les relations et sur les fonctions, mais sur les suites aussi. Encore une fois,
mentionnons qu’il faut toujours garder à l’esprit que le résultat de l’opération ne sera
pas nécessairement une suite.
4. Toutefois, certains opérateurs sont définis tout spécialement pour les suites et nous
les présentons à l’instant.
Soit X un ensemble fixé et soient x1 , x2 , ..., xn ∈ X . On a les opérateurs suivants qui se
passent de commentaires (mais pas d’exemples).

Exemple Commentaire
head head hx1 , x2 , ..., xn−1 , xn i = x1 - La suite doit être non vide
last lasthx1 , x2 , ..., xn−1 , xn i = xn - La suite doit être non vide
tail tail hx1 , x2 , ..., xn−1 , xn i = hx2 , ..., xn−1 , xn i - La suite doit être non vide
front fronthx1 , x2 , ..., xn−1 , xn i = hx1 , ..., xn−1 i - La suite doit être non vide
a hx1 , ..., xn i a hy1 , ..., ym i = hx1 , ..., xn , y1 , ..., ym i

Exemples:
1. Prenons

s : seq N
s = h2, 4, 6, 8, 10, 12i

front s = h2, 4, 6, 8, 10i

front s = {(1, 2), (2, 4), (3, 6), (4, 8), (5, 10)}
tail s = h4, 6, 8, 10, 12i
tail s = {(1, 4), (2, 6), (3, 8), (4, 10), (5, 12)}
head s = 2
last s = 12

2. Prenons

COULEUR ::= bleu | blanc | rouge | jaune | noir

27
 s : seq COULEUR
s = hblanc, noir , bleui

front s = hblanc, noir i

front s = {(1, blanc), (2, noir )}
tail s = hnoir , bleui
tail s = {(1, noir ), (2, bleu)}
head s = blanc
last s = bleu

3.
h2, 4, 6, 8, 10, 12i a h1, 3, 5, 7, 9, 11i = h2, 4, 6, 8, 10, 12, 1, 3, 5, 7, 9, 11i

3.3 Schémas

Rappelez-vous ! Ce qui est défini à l’extérieur d’un schéma est considéré en Z comme étant
fixé, constant et ne peut pas être modifié. Ce qu’on veut pouvoir modifier (lors d’opérations
qui modifient l’état du système) doit être défini à l’intérieur d’un schéma, habituellement
dans celui qui représente l’état général du système.
On verra quelques schémas dans l’exemple du dictionnaire (voir Chap. 4). De façon
générale un schéma s’écrit de la façon suivante.

Schema
Declaration
Predicats

On peut aussi le noter de la façon suivante

b [Declarations | Predicats].
Schema =

Nous n’utiliserons pas cette notation, mais nous la présentons pour aider à comprendre
de quelle façon un outil comme Z-eves considère les schémas.

3.3.1 Schéma qui représente l’état général du système (ou d’une

partie du système)

28
 Un état du système est représenté par la valeur de l’ensemble de ses variables à un mo-
ment précis. Quand on spécifie l’état général d’un système et donc ses états possibles, il faut
toujours écrire TOUTES les propriétés que ses états doivent toujours satisfaire (ses inva-
riants). Dans l’exemple du dictionnaire (Chap. 4), l’état général est appelé Dictionnaire, il a
une variable, Paires, et une seule contrainte ou invariant, Paires ⊆ PAIRES CORRECTES .

Il est important de spécifier l’état initial du système. On utilise la notation suivante.

SchemaInit
Schema
Predicats

Notez que cet état initial doit aussi être un état valide du système. Parfois, nous n’avons
que des informations partielles sur l’état initial (on n’a des valeurs que pour certaines des
variables du système). Il ne faut pas faire de suppositions qui n’ont pas été demandées par le
client. Il faut modéliser les informations qui représentent les besoins exprimés par le client,
c’est tout, tout en respectant les invariants, bien sûr. Il peut donc arriver que la valeur de
certains items du système ne soient pas spécifiée, ce n’est absolument pas problématique.

3.3.2 Schéma qui représente une opération

Parlons maintenant des schémas qui représentent des opérations. Typiquement, une opé-
ration fait passer le système (ou une partie du système) d’un état à un autre. Il faut toujours
identifier avec quel(le) (partie du) système une fonction travaille. On utilise les notations
— ΞSysteme pour indiquer que le système doit être inchangé par l’opération (par exemple
pour l’opération de rechercher une traduction dans l’exemple du dictionnaire)
— ∆Systeme pour indiquer qu’il est possible que le système soit changé par la fonction.
Rappelons ces définitions .

∆Schema
Schema
Schema 0

ΞSchema
∆Schema
ΘSchema = ΘSchema 0 5

5. écrire ΘSchema = ΘSchema 0 correspond à écrire variable 0 = variable pour toutes les variables qui
définissent Schema : mais ceci dépasse le niveau du cours.

29
 Dans le cas où on utilise la notation ∆, il faut indiquer la nouvelle valeur de TOUTES
les variables du système, même de celles qui ne changent pas. Ne pas indiquer de nouvelle
valeur correspond à indiquer que la valeur n’est pas importante, ce qui est rarement le cas
quand on définit une opération. NOTEZ LE BIEN, C’EST UNE ERREUR COURANTE.

Écrire ∆Systeme nous donne accès à toutes les variables de Systeme ainsi qu’à toutes les
variables de Systeme décorées de 0 . Les variables primées représentent la valeur de ces va-
riables à l’état suivant, après l’application de la fonction que l’on définit. N’oubliez pas : Un
outil comme Z-eves ne sait pas que les variables primées représentent la valeur des variables
après l’application de la fonction. C’est NOTRE interprétation. C’est à nous de manipuler
ces variables comme tel. Si nous sommes conséquent dans notre utilisation des variables
primées, la théorie des ensembles et la logique du premier ordre nous garantissent que les
conclusions que nous tirerons de nos analyses seront correctes.

3.4 Conclusion

La tâche qui nous attend maintenant est de faire parler tous ces opérateurs afin de mo-
déliser des programmes. La présentation dans ce chapitre était davantage théorique que
pratique, mais nous nous lançons maintenant dans l’étude de plusieurs exemples (en classe,
dans les exercices et dans les laboratoires).

Par la suite, il faudra en arriver à suffisamment bien comprendre ces opérateurs pour
faire de la démonstration de propriétés. On va ainsi déduire des propriétés du programme
qui doit être construit. Nous pourrons donc “calculer” si son comportement est conforme aux
demandes du client.

30
Chapitre 4

Premier exemple : le dictionnaire

Nous introduirons dans ce chapitre plusieurs concepts et principes de base utilisés en Z.

Le but est de voir de quelle façon la théorie des ensembles et la logique mathématique sont
utilisées pour modéliser un programme.

Ce premier exemple nous permettra de voir l’utilité d’utiliser un langage très mathéma-
tique pour représenter fidèlement les propriétés que l’on souhaite modéliser. Il faut rappeler
que le code obtenu est alors extrêmement précis, sans équivoque, mais qu’il n’est pas exécu-
table ! Regardons maintenant le contexte de cette première spécification.

4.1 Description de l’exemple

Supposons que vous étudiez une langue étrangère et que vous désirez conserver une trace
de tous les nouveaux mots que vous apprenez. Pensez à un dictionnaire de poche que vous
remplissez vous-mêmes au fur et à mesure que vous ajoutez de nouveaux mots de vocabu-
laire. Nous simplifierons le problème pour avoir une version qui soit une bonne introduction
au langage Z.

Dans ce dictionnaire, nous voulons avoir la possibilité d’ajouter des traductions de mots.
Nous voulons aussi avoir la possibilité d’avoir la traduction d’un mot qui est dans le diction-
naire (autant de la langue maternelle vers la langue étrangère que de la langue étrangère vers
la langue maternelle). Nous ne ferons pas de supposition sur la langue maternelle ni sur la
langue étrangère. Ce peut tout aussi bien être le français et le russe, l’hébreux et l’allemand
ou encore l’anglais et le morse.

Nous avons dit que ce dictionnaire serait simplifié, tout d’abord le dictionnaire ne contient
que des paires de mots. Par exemple (pour français/anglais) il contient des paires comme
(soleil , sun), (table, table), (signifier , mean), (moyenne, mean), etc. Habituellement, lors-
qu’un mot peut avoir plus d’une signification, un dictionnaire présente les différents contextes

31
dans lesquels ce mot peut se retrouver. Il n’y aura pas cette option dans notre dictionnaire
(qui fait de plus en plus penser à un aide-mémoire). Il n’y aura que des paires de mots. De
même, si l’on traduit une phrase mot à mot, il s’avère souvent que le résultat n’a pas de sens,
tant pis ! Ce dictionnaire ne contient que des paires de mots. Il faut mentionner un dernier
point important sur la façon dont les informations sont enregistrées en mémoire. Certains
ont peut-être déjà en tête une stratégie quant à la structure de données qu’ils utiliseront pour
stocker les données (liste, file, pile, ordre alphabétique, par ordre du plus consulté au moins
consulté, etc.) Vous pourriez avoir l’impression que ce choix est important. Il l’est effective-
ment, mais pas à ce stade-ci. Pour l’étape de la spécification, on ne fait pas d’hypothèses
de ce genre. On ne fait que modéliser le comportement et les propriétés que le programme
devra respecter. Le programmeur qui va écrire le code à partir de notre spécification sera
celui qui fera ces choix. N’oubliez pas : le Z n’est pas un langage de programmation, c’est un
langage de spécification. Autrement dit, c’est un langage qui permet de décrire ce qui doit
être fait sans aucun égard à comment ce doit être fait.

Dans l’éventualité où l’on voudrait par exemple imprimer la liste des mots se trouvant
dans la base données, il serait intéressant de modéliser le processus qui classe en ordre al-
phabétique, mais cette option n’est pas disponible avec notre petit dictionnaire.

On veut quand même imposer un certain réalisme à notre dictionnaire, nous demande-
rons donc que l’orthographe soit correcte. Il y aura donc une distinction entre les mots d’une
langue et les mots correctement orthographiés de cette même langue.

4.2 Analyse de la spécification

Regardons une spécification possible pour ce dictionnaire. Nous noterons au passage

plusieurs points importants, des remarques indispensables à retenir lors de l’écriture d’une
spécification en Z et des remarques importantes pour comprendre les différents aspects de
la présente spécification. Voici donc le code, prenez le temps de le lire attentivement, des
remarques suivront.

[MATERNELLE , ETRANGERE ]

ORTHO MATERNELLE : F MATERNELLE

ORTHO ETRANGERE : F ETRANGERE

PAIRES CORRECTES : F(ORTHO MATERNELLE × ORTHO ETRANGERE )

MESSAGE ::= ErreurMaternelle | ErreurEtrangere | ErreurdAssociation

32
Dictionnaire
Paires : F(MATERNELLE × ETRANGERE )
Paires ⊆ PAIRES CORRECTES

DictionnaireInit
Dictionnaire
Paires = {}

AjouterPaire
∆Dictionnaire
m? : MATERNELLE
e? : ETRANGERE
(m?, e?) ∈ PAIRES CORRECTES
Paires 0 = Paires ∪ {(m?, e?)}

ErreurOrthographeMaternelle
m? : MATERNELLE
rep! : MESSAGE
m? 6∈ ORTHO MATERNELLE
rep! = ErreurMaternelle

ErreurOrthographeEtrangere
e? : ETRANGERE
rep! : MESSAGE
e? 6∈ ORTHO ETRANGERE
rep! = ErreurEtrangere

ErreurAssociation
m? : MATERNELLE
e? : ETRANGERE
rep! : MESSAGE
m? ∈ ORTHO MATERNELLE
e? ∈ ORTHO ETRANGERE
(m?, e?) 6∈ PAIRES CORRECTES
rep! = ErreurdAssociation

33
 AjouterPaireTotale =
b AjouterPaire
∨ ΞDictionnaire ∧ (ErreurOrthographeMaternelle
∨ErreurOrthographeEtrangere
∨ErreurAssociation)

VersLangueEtrangere
ΞDictionnaire
m? : MATERNELLE
traduction! : P ETRANGERE
m? ∈ ORTHO MATERNELLE
∃ e : ETRANGERE • (m?, e) ∈ Paires
traduction! = {e : ETRANGERE | (m?, e) ∈ Paires}

Regardons maintenant cette spécification point par point.

1. Le seul type défini en Z est Z. Cet ensemble représente bien sûr l’ensemble de nombres
bien connu.
Z = {..., −3, −2, −1, 0, 1, 2, 3, ...}
Tous les autres types doivent être définis. Le symbole N est disponible, il représente

N = {0, 1, 2, 3, 4, 5, ...}.

Dans la base de connaissances que Z reconnaît , il y a N == {x : Z | x ≥ 0}. Ce n’est

par contre pas un type. Les types que vous connaissez dans plusieurs langages : char ,
bool , double, etc n’existent pas en Z. Il faut les définir un par un à chaque fois.
Définition 4.2.1 (Type) En Z, un type est un ensemble qui n’est inclus dans aucun
autre (sauf lui-même).
Avec cette définition, on peut voir que Z est un type. De plus, on peut voir que N
n’est pas un type. En effet, N ⊂ Z.

Nous avons mentionné plus tôt qu’il n’y a pas de booléens. Comment les définir ?
Voici des exemples.

ETAT ::= On | Off

ou encore

MESSAGE ::= Ok | ErreurEntree

Cela définit alors les types ETAT et MESSAGE qui sont les ensembles ETAT =
{On, Off } et MESSAGE = {Ok , ErreurEntree}. Avec la même syntaxe, on peut
définir un type qui peut prendre exactement trois valeurs.

PROGRAMME ETUDE ::= Informatique | GenieInformatique | GenieLogiciel

34
 C’est donc dire que tous les autres types doivent être définis. Dans l’exemple qui
nous concerne, nous définissons les types MATERNELLE (pour langue maternelle)
et ETRAN GE RE (pour langue étrangère). Ces types sont manipulés par Z comme
étant des ensembles. On a donc le droit d’effectuer toutes les opérations sur les en-
sembles disponibles en Z (tant que l’on respecte le typage).

Il y a une subtilité à laquelle il faut faire attention. La signification de ces ensembles,

il n’y a que nous qui la connaissons. C’est à nous d’être cohérent lors de leur mani-
pulation. On les utilise pour représenter les différents mots de la langue maternelle
et étrangère écrits avec ou sans fautes d’orthographe. On peut les voir en fait comme
une suite de symboles choisis dans l’alphabet de la langue en question. Par exemple,
si la langue maternelle est le grec, nous avons γα µ µ α ∈ MATERNELLE ou en-
core τ τ τ τ τ τ α ∈ MATERNELLE . Attention ! Un outil comme Z-eves ne sait pas que
γα µ µ α ∈ MATERNELLE et que τ τ τ τ τ τ α ∈ MATERNELLE . Tout ce que nous
lui avons dit c’est que MATERNELLE et ETRANGERE sont des types. Nous ne
lui avons jamais dit ce que ces ensembles contenaient. Il ne peut pas le savoir non
plus (à moins d’avoir défini ces ensembles en décrivant explicitement chacun de ses
éléments.) Le fait de dire γα µ µ α ∈ MATERNELLE et τ τ τ τ τ τ α ∈ MATERNELLE ,
c’est NOTRE façon de comprendre ces ensembles.

2. Nous définissons ensuite trois ensembles. Les ensembles ORTHO MATERNELLE et

ORTHO ETRAN GE RE représentent l’ensemble des mots de chacune des langues
écrits dans un orthographe correct. On doit (et c’est toujours le même principe en
Z) identifier toutes les propriétés connues que ces ensembles satisfont. Puisque les
langues (donc l’alphabet et l’ensemble des symboles nécessaires) ne sont pas connues,
la seule propriété que l’on peut identifier est qu’il s’agit de sous-ensembles des en-
sembles MATERNELLE et ETRANGERE . Il va de soi que l’on ne peut spéculer sur
les règles d’orthographes des langues maternelle et étrangère non plus puisque nous
ne savons pas quelles sont ces langues.

L’ensemble PAIRES CORRECTES représente l’ensemble des paires possibles for-

mées de mots correctement orthographiés et correctement associés (la traduction est
correcte). Encore une fois, parce que l’on ne connaît pas les langues représentées, la
seule propriété connue est qu’il s’agit de paires de mots dans ORTHO MATERNELLE ×
ORTHO ETRANGERE . Il faut bien comprendre que nous manipulerons l’ensemble
PAIRES CORRECTES comme étant l’ensemble des paires de mots correctement as-
sociés, mais que rien dans les propriétés spécifiées (à part le nom) n’indique que c’est
le cas. Disons-le autrement, nous avons déclaré un ensemble
PAIRES CORRECTES : F(ORTHO MATERNELLE × ORTHO ETRANGERE )
Il y a plusieurs ensembles dans
F(ORTHO MATERNELLE × ORTHO ETRANGERE )

35
 mais nous en avons fixé un, nous l’avons appelé PairesCorrectes et nous le manipulons
comme l’ensemble des paires de mots correctement associés (et correctement ortho-
graphiés).

Supposons que l’on connaisse les deux langues. Prenons par exemple le cas français/an-
glais. Nous pourrions être plus précis sur les ensembles ORTHO MATERNELLE
et ORTHO ETRANGERE en précisant l’ensemble des règles d’orthographes pour
chacune des langues, ce qui permettrait de spécifier ces deux ensembles avec plus de
détails. Il faut bien comprendre que ce n’est pas automatiquement nécessaire ! Tout
dépend de la spécification que l’on veut faire, tout dépend du degré de précision voulu.
C’est le client et ses besoins qui déterminent jusqu’à quel point nous raffinerons la
spécification des différents éléments. Dans notre cas, nous supposons que c’est suffisant
de cette façon.
3. Nous désirons modéliser un Dictionnaire. Pour ce faire, nous écrirons les différents
éléments qui s’y retrouve ainsi que l’ensemble de TOUTES les propriétés que ces
éléments doivent satisfaire. Dans notre cas, c’est plutôt simple : notre dictionnaire
contient des paires de mots. Les mots de ces paires doivent être correctement ortho-
graphiés et correctement associés.

La “boîte” dans laquelle nous avons écrit la spécification du dictionnaire s’appelle

un schéma. Par la suite, chaque fois que l’on référera à ce schéma, on aura accès à
l’ensemble Paires et on devra respecter le fait que Paires ⊆ PairesCorrectes, sinon
on risque de tomber sur des contradictions. Comme vous pouvez le constater il y
a plusieurs schémas dans cette spécification et ils ont des utilités différentes. Nous
donnerons plus de détails dans les prochains chapitres.
4. Nous devons définir un état initial (dans notre cas DictionnaireInit) qui représente
l’état dans lequel le système sera la toute première fois qu’il sera mis en marche. Le
dictionnaire initial est vierge, il ne contient aucune paire de mots, l’utilisateur n’a ins-
crit aucune nouvelle traduction pour le moment. Nous l’initialisons donc à l’ensemble
vide.

Remarque intéressante : dans la définition de DictionnaireInit, nous référons au

schéma Dictionnaire, c’est pourquoi nous pouvons utiliser l’ensemble Paires. Re-
marque réellement intéressante : puisque nous référons au schéma Dictionnaire, nous
devrons vérifier que nous respectons le fait que Paires ⊆ PairesCorrectes. Ici, c’est
bien le cas :

Paires = ∅
⊆ PairesCorrectes,

car l’ensemble vide est inclus dans tous les ensembles, quels qu’ils soient.
5. Nous pouvons maintenant regarder les différentes fonctions que notre dictionnaire doit

36
avoir. Pour ce faire, nous verrons d’abord quelques principes.

Une fonction s’applique à un état valide du système. Certaines fonctions laissent

l’état inchangé quand d’autres envoient un état valide du système à un autre état
valide. Dans notre spécification, le système est le Dictionnaire et un état valide est
un état tel que Paires ⊆ PairesCorrectes. Une fonction s’applique à un système ou
à une partie d’un système. Toutefois, il est possible de définir une fonction qui ne
sert qu’à simplifier l’écriture d’une autre fonction (comme on le fait régulièrement en
programmation). De plus, une fonction peut prendre une valeur en entrée (mais pas
nécessairement) et peut retourner une valeur en sortie (mais pas nécessairement).

Pour définir une fonction en Z, on travaille avec les schémas. Le schéma est identifié
par le nom de la fonction. Il faut identifier le système avec lequel on travaille (dans
notre cas, il s’agit de Dictionnaire) ainsi que les variables d’entrée et de sortie. Une va-
riable d’entrée est identifiée par un point d’interrogation ( ?) et une variable de sortie
par un point d’exclamation ( !). Dans la deuxième section du schéma, on identifie les
propriétés que doivent satisfaire le système ainsi que les variables d’entrée et de sortie
pour que cette fonction envoie le système dans un état valide et qu’elle satisfasse les
besoins du client. Autrement dit, on décrit ce que la fonction fait. Mais on ne décrit
pas comment elle le fait !

La notation ∆Dictionnaire (Delta Dictionnaire) indique que le système sera modi-

fié par la fonction et la notation ΞDictionnaire (Xi Dictionnaire) indique qu’il ne
sera pas modifié. On identifie les variables du système avant l’application de la fonc-
tion tout simplement par leur nom. On identifie les variables après l’application de la
fonction par leur nom primé (’). Notez que ceci n’est qu’une convention, une notation.

Prenons dans notre exemple la fonction AjouterPaire. Nous identifions le système

Dictionnaire précédé d’un ∆ pour indiquer que le système est modifié par cette fonc-
tion (techniquement pour déclarer les variables et leur version primée). Il y a deux
variables d’entrée m? et e?. La seule variable du système est Paires. Les propriétés à
respecter par les variables d’entrée sont les règles d’orthographe. La variable Paires
doit satisfaire Paires 0 = Paires ∪ {(m?, e?)}. Donc la variable Paires après l’ap-
plication de la fonction contient les mêmes informations qu’avant en plus de la paire
(m?, e?). On peut refaire la même analyse pour les autres fonctions. Pour quelle raison
avons-nous accès à la variable Paire ? Parce que l’opérateur ∆ se charge de l’importer.

Il y a d’autres remarques importantes à faire. Z-eves ne sait pas que Paires 0 est la
valeur de Paires après l’application de la fonction. C’est NOTRE interprétation. C’est
à nous de manipuler Paires comme tel. Si nous sommes conséquent dans notre utili-
sation des variables primées, la théorie des ensembles et la logique du premier ordre
nous garantissent que nous n’arriverons à aucune contradiction.

37
 On peut préciser de façon rigoureuse ce que signifient ∆Dictionnaire et ΞDictionnaire,
voici les définitions en Z (notez que nous n’avons pas à les définir chaque fois dans
Z-eves puisque les symboles ∆ et Ξ y sont disponibles).

∆Dictionnaire
Dictionnaire
Dictionnaire 0

ΞDictionnaire
∆Dictionnaire
ΘDictionnaire = ΘDictionnaire 0

Ainsi, quand on écrit ∆Dictionnaire, c’est simplement un raccourci pour :

∆Dictionnaire
Paires : F(MATERNELLE × ETRANGERE )
Paires 0 : F(MATERNELLE × ETRANGERE )
Paires ⊆ PAIRES CORRECTES
Paires 0 ⊆ PAIRES CORRECTES

Similairement

ΞDictionnaire
Paires : F(MATERNELLE × ETRANGERE )
Paires 0 : F(MATERNELLE × ETRANGERE )
Paires ⊆ PAIRES CORRECTES
Paires 0 ⊆ PAIRES CORRECTES
Paires = Paires 0

6. Comme la syntaxe le suggère, la notation :

AjouterPaireTotale =
b AjouterPaire
∨ ΞDictionnaire ∧ (ErreurOrthographeMaternelle
∨ErreurOrthographeEtrangere
∨ErreurAssociation)

indique que la version complète (totale) de AjouterPaire se comporte soit comme

AjouterPaire, soit elle ne modifie pas le dictionnaire dans le cas où il y a une erreur
d’orthographe ou une erreur d’association. On doit toujours définir une fonction totale
et expliquer comment elle se comporte, sauf avis contraire du client.

38
7. Remarquez que l’interface n’a pas été spécifiée. C’est-à-dire que tout l’aspect gra-
phique et tout l’aspect interaction avec l’utilisateur n’est pas défini. C’est un choix
qui dépend des besoins du client. Dans le cadre de ce cours, nous ne modéliserons
pratiquement jamais cette interface.
8. Les ensembles définis à l’extérieur d’un schéma sont FIXES et donc CONSTANTS.
Certains sont des types, certains non. Tous les autres ensembles peuvent varier dans le
temps. Les ensembles définis à l’extérieur des schémas (donc les types et les ensembles
constants) doivent toujours être écrits en lettres majuscules. Ce n’est pas une règle
syntaxique, c’est une bonne habitude à prendre... et qui sera pénalisée si elle n’est pas
respectée.

39
Chapitre 5

Théorie du contrat

Dans ce chapitre, nous présentons un très bref survol de quelques concepts de base en
théorie du contrat. Habituellement, la théorie du contrat est étudiée en programmation orien-
tée objets (référence IFT-2005 Programmation orientée objets). Nous verrons que plusieurs
éléments de cette théorie sont en lien direct avec la matière que nous étudions en spécification
formelle, tout particulièrement avec le langage Z. La théorie du contrat nous aidera à regarder
les spécifications écrites en langage Z sous un autre oeil en nous donnant des outils d’analyse.

Une des qualités majeures d’un bon logiciel est sa fiabilité. C’est-à-dire sa capacité à faire
le travail pour lequel il a été conçu (un programme conforme à sa spécification) ainsi que sa
capacité à gérer correctement les situations exceptionnelles. Il s’agit en fait du problème cen-
tral en génie logiciel. La théorie du contrat a été développée dans le but de donner des outils
aux informaticiens pour les aider à développer des systèmes fiables. Elle aide à déterminer
de façon très précise le rôle de chaque composante (classe) et de chacune de leurs méthodes.
Enfin, la théorie du contrat permet de mettre un nom sur plusieurs éléments rencontrés lors
de la programmation. Comme c’est souvent le cas, le fait d’avoir une nomenclature précise
pour nommer quelque chose permet de mieux comprendre et de mieux analyser cette chose.

En théorie du contrat (et en programmation orientée objets), les composantes sont vues
comme des entités communiquant entre elles. Chacune s’attend à ce que l’on communique
avec elle selon des règles bien précises. En retour, elle s’engage à exécuter certaine(s) tâche(s)
sans mettre le système dans un état indésirable. Ce qui fait penser... à un contrat ! Voici les
détails.

5.1 La notion de contrat

Habituellement, un contrat est un document écrit entre deux personnes (parties) où l’un
d’entre eux (contracteur) exécute une tâche pour l’autre (client). Normallement, un contrat
engage les deux parties à certaines obligations, mais leur garantit aussi un certain bénéfice
en retour. Souvent l’engagement d’une partie est un quelconque avantage pour l’autre partie.

40
Un contrat décrit de façon précise les engagements et les bénéfices de chacun. Si l’une des
deux parties ne respecte pas ses engagements, alors l’autre partie ne peut garantir que sa
part du contrat sera respectée.

Par exemple, si vous désirez envoyer une lettre par l’intermédiaire de Postes Canada.
Postes Canada et vous avez des obligations à respecter, mais si chacun remplit sa part du
contrat, chacun en tire des bénéfices.

Partie Obligations Bénéfices

Vous Fournir une lettre pas trop lourde, Votre lettre arrive à destination
pas trop grande et ne contenant pas intacte n’importe où au Canada
de matière dangeureuse ou illégale. dans un temps raisonnable.
Payer 0, 50$ (plus taxes !)

Postes Canada Livrer votre lettre dans un temps N’a pas à manipuler les lettres
raisonnable sans l’abîmer, tout trop lourdes ou trop grosses
en gardant le contenu confidentiel. pour un prix dérisoire.

L’exemple de la poste est une image qu’il ne faut pas prendre au pied de la lettre. On
pourrait questionner certains points en se demandant s’il s’agit réellement d’un bénéfice ou
d’une obligation... gardez à l’esprit l’idée générale.

5.2 Applications en programmation orientée objets

Les principales applications de cette théorie sont en programmation orientée objets. Plu-
sieurs articles ont été écrits sur le sujet. Le langage Eiffel a été conçu pour mettre directement
en pratique cette théorie du contrat. Dans ce langage, en plus d’écrire le code du programme,
on inscrit aussi les obligations et bénéfices de chacun (les préconditions et les postconditions).
L’idée est de développer des techniques ayant pour but d’aider les programmeurs à dévelop-
per des programmes fiables. L’objectif d’Eiffel est d’aider les programmeurs à se vérifier au
fur et à mesure que le projet progresse. De plus, la théorie du contrat offre des outils pour
guider les ingénieurs logiciels lors de l’étape des tests.

On traduit ici “obligations” par préconditions et “bénéfices” par postconditions. On ajoute

aussi la notion d’invariants de classe. Pensons à une classe et à ses méthodes. Les précondi-
tions sont les conditions à satisfaire pour appeler une méthode et s’assurer qu’elle s’exécute
correctement. Aussi banal que cela puisse paraître, on peut d’abord penser à son nom : en
effet, il faut appeler la méthode par son nom sinon elle ne peut pas s’exécuter correctement !
Il y a aussi le nombre, l’ordre et le type de ses paramètres d’entrée. On peut finalement
penser aux conditions particulières que les entrées doivent satisfaire. Par exemple, dans le
cas d’une fonction qui prend un nombre réel en entrée, est-ce que 0 est acceptable ? Quelle
est la plus grande valeur permise ? Y a-t-il un degré de précision à respecter pour que la

41
fonction s’exécute correctement ? Etc.

Pour ce qui est des postconditions, on peut penser à ce que la fonction retourne en sortie.
Quel est son type, quelles propriétés la sortie doit-elle satisfaire ? Est-ce que elle doit être
bleue, rouge, petite, tordue ?

On arrive finalement à la notion d’invariants de classe. Il s’agit de propriétés qui doivent

être satisfaites tout au long de la vie d’un objet, de sa création à sa destruction. Prenons par
exemple une classe Date.

class Date { public:

// ...
private:
int jour;
int mois;
int annee;
};

Il y a une multitude de propriétés que jour , mois et annee doivent satisfaire, en voici
quelques-unes.
— 1 ≤ jour ≤ 31
— 1 ≤ mois ≤ 12
— ? ≤ annee ≤ ? tout dépend du client
— Si mois ∈ {4, 6, 9, 11}, alors 1 ≤ jour ≤ 30.
— Etc.
On doit toujours s’assurer que les méthodes d’une classe vont respecter ces invariants. Si
jamais une méthode modifie un objet en cours d’exécution de telle sorte que les invariants
ne sont pas tous satisfaits, il faut à tout prix que la situation soit rétablie avant la fin de
l’exécution de cette méthode.

En précisant très clairement les préconditions, postconditions et invariants à satisfaire,

on permet au programmeur de minimiser les erreurs. On permet aussi une gestion plus facile
des exceptions. En C++, on peut expérimenter cette théorie à l’aide des assertions. Nous
avons mentionné plus tôt le langage Eiffel qui a été conçu spécialement pour mettre cette
théorie en pratique. Il s’agit d’un espèce de mélange entre le C++ et le Z. Pour parler plus
précisément de tous ces aspects, il faudrait se placer dans le contexte de programmation
orientée objets. Par contre, il n’est pas nécessaire d’en dire davantage pour comprendre les
propos qui suivent.

42
5.3 Applications en Z

Ce que cette théorie nous apporte en Z, c’est une façon de bien comprendre chacun des
éléments d’une spécification. Avec cette notion de contrat en tête, il est plus facile de com-
prendre ce qui doit être spécifié, comment et pourquoi.

En Z, les invariants d’un système sont faciles à détecter. Comme vous pourrez le consta-
ter dans les chapitres qui suivent, il s’agit des propriétés écrites dans la deuxième partie
des schémas. Bien sûr, les schémas qui représentent le (ou une partie du) système, pas les
schémas qui représentent des fonctions. Pour ce qui est des préconditions et des postcondi-
tions, elles sont mélangées dans la deuxième partie des schémas représentant les fonctions.
Les prédicats formés des variables non primées forment habituellement les préconditions et
les prédicats formés des variables primées forment habituellement les postconditions.

Voici l’analyse des préconditions, postconditions et invariants de l’exemple du diction-

naire qui a été présenté un peu plus tôt.

Fonction AjouterPaire
Entrées/Sorties m? : MATERNELLE
e? : ETRANGERE
Préconditions (m?, e?) ∈ PAIRES CORRECTES
Postconditions Paires 0 = Paires ∪ {(m?, e?)}
Invariants Paires ⊆ PAIRES CORRECTES

Fonction ErreurOrthographeMaternelle
Entrées/Sorties m? : MATERNELLE
rep! : MESSAGE
Préconditions m? 6∈ ORTHO MATERNELLE
Postconditions rep! = ErreurMaternelle
Invariants

Fonction ErreurOrthographeEtrangere
Entrées/Sorties e? : ETRANGERE
rep! : MESSAGE
Préconditions e? 6∈ ORTHO ETRANGERE
Postconditions rep! = ErreurEtrangere
Invariants

43
 Fonction ErreurAssociation
Entrées/Sorties m? : MATERNELLE
e? : ETRANGERE
rep! : MESSAGE
Préconditions m? ∈ ORTHO MATERNELLE
e? ∈ ORTHO ETRANGERE
(m?, e?) 6∈ PAIRES CORRECTES
Postconditions rep! = ErreurdAssociation
Invariants

Fonction VersLangueEtrangere
Entrées/Sorties m? : MATERNELLE
traduction! : P ETRANGERE
Préconditions m? ∈ ORTHO MATERNELLE
∃ e : ETRANGERE • (m?, e) ∈ Paires
Postconditions Paires 0 = Paires
traduction! = {e : ETRANGERE | (m?, e) ∈ Paires}
Invariants Paires ⊆ PAIRES CORRECTES

5.4 Conclusion

Il y a deux éléments à retenir de ce chapitre. D’abord, faites le lien entre la théorie du

contrat et votre cours de programmation orientée objets (que vous avez déjà suivi ou que
vous suivrez prochainement). Vous verrez alors plusieurs liens intéressants avec la spécifica-
tion formelle (certains en parlent dès le cours d’algorithmique et programmation IFT-1001).

Ensuite, prenez toujours la peine d’analyser quels sont les préconditions, postconditions
et invariants d’un système. Faites le en Z et dans tous les projets qui vous passent entre les
mains.

44
Chapitre 6

Bibliothèque

Dans ce chapitre, nous étudierons un exemple qui montre comment les opérateurs présen-
tés précédemment peuvent être utilisés pour modéliser un programme. Ce sera une occasion
de revoir les différentes parties d’une spécification formelle en Z aussi en profiterons-nous
pour rappeler certains faits concernant les types, les schémas, etc.

Une spécification formelle commence toujours à partir des besoins d’un client. Supposons
donc que la municipalité de Ste-élisabeth-de-Proulx nous approche pour informatiser le sys-
tème de gestion de leur bibliothèque. Ils nous font la description de leurs besoins que l’on
peut résumer ainsi.
— La Bibliotheque 1 possède un stock de Livre.
— Plusieurs Lecteur visitent cette Bibliotheque, mais seuls les membres peuvent emprunter
des Livres.
— Chaque copie d’un Livre est identifié par une Cote unique.
— La Bibliotheque n’a pratiquement jamais tous ses Livres dans la bâtisse. Certains sont
empruntés et d’autres sont disponibles.
— Un membre ne peut emprunter autant de Livres qu’il le souhaite. Cette limite sera
notée par la constante nb pret max fixée par ceux qui gèrent la bibliothèque. évidem-
ment nb pret max ≥ 1.
Les opérations suivantes doivent être possibles dans cette Bibliotheque.
— Un membre doit pouvoir emprunter un Livre.
— Un membre doit pouvoir retourner un livre à la Bibliotheque.
— Ajouter des Livres à son stock .
— Retirer des Livres de son stock .
— Avoir la liste des Livres empruntés par un membre en particulier.
— Savoir quel membre a emprunté une copie précise d’un Livre.
— Abonner un nouveau membre.
1. Par convention, dans ce cours, nous utilisons l’italique pour indiquer que le mot doit se retrouver
dans la spécification, histoire d’uniformiser les spécifications dans le groupe. La dérivation, l’accord ou la
conjugaison ne sont pas nécessairement distinctifs (emprunt n’est pas nécessairement différent de emprunté
par exemple).

45
 — Mettre un membre à la porte.
— Connaître les Cotes correspondantes à un Livre en particulier. Nous ne voulons que
les cotes des Livres disponibles.

6.1 Une spécification de la bibliothèque

Comment pouvons-nous arriver à traduire cette description en code Z ? Qu’est-ce qui doit
devenir un type ? Qu’est-ce qui doit être un ensemble fixe, sans être un type ? Que met-on
dans l’état initial ? Et dans l’état général ? Allons-y étape par étape.

D’abord, il faut décider quels seront nos types et nos constantes. Rappelez-vous qu’un
type est un ensemble très général, relativement abstrait qui englobe TOUS les éléments d’une
même catégorie. Prenons par exemple les clients de la bibliothèque. Certains sont membres
et d’autres ne le sont pas. Comment pourrions-nous déclarer un type qui les incorpore tous ?
Ce sont tous des lecteurs, nous pourrions déclarer un type LECTEUR. Qu’y a-t-il dans cet
ensemble LECTEUR ? La description faite par le client ne mentionne rien concernant la
gestion des prénoms, noms de famille, numéros de téléphone, etc. On peut s’imaginer qu’un
élément typique de LECTEUR contient de l’information pertinente à propos des coordon-
nées dudit lecteur. C’est une image qui peut nous aider à comprendre le type LECTEUR,
mais notez que la spécification elle-même ne donne aucune information à ce sujet. Il ne
faut pas détailler puisque nous n’avons pas d’indices sur les informaions qui seront enregis-
trées quand un lecteur se présente au comptoir : n’en faites pas plus que le client en demande !

Parlons maintenant des cotes. Tous les livres ont une cote. Quel est le type général qui
pourrait englober toutes les cotes ? Ce pourrait être le type COTE . On peut imaginer qu’il
s’agit de toutes les séquences alpha-numériques permettant d’identifier un livre dans une
bibliothèque. La Bibliotheque identifie ses livres au moyen de ces cotes. Certaines d’entre
elles existent (elles sont éléments de COTE ) sans être utilisées. En effet, la Bibliotheque ne
possède probablement pas autant de livres qu’il existe de cotes différentes dans COTE .

Finalement, les livres pourraient être de type LIVRE ! On peut penser que les éléments
de ce type contiennent des informations sur le titre, l’auteur, l’année de parution, la maison
d’édition, etc. Attention, la cote ne fait sûrement pas partie des informations concernant le
livre ! En effet, plusieurs cotes peuvent être attribuées à un même livre si la bibliothèque en
possède plus d’un exemplaire.

On déclare donc les types suivants.

[COTE , LIVRE , LECTEUR]

Dans la description de la bibliothèque, nous décrivons la constante nb pret max . La des-

cription n’est pas précise, la caractéristique décrite est son utilité : un membre ne peut

46
emprunter autant de Livres qu’il le souhaite. Cette limite sera notée par la constante
nb pret max fixée par ceux qui gèrent la bibliothèque. Nous n’avons aucune idée de sa va-
leur, excepté que nb pret max ≥ 1. La seule propriété que l’on peut modéliser est donc
nb pret max > 0. Certains pourraient être portés à écrire nb pret max > 1 parce qu’il se-
rait surprenant que le bibliothèque limite le nombre d’emprunts pour un membre à un livre.
Nous ne devons pas faire de telle supposition parce que rien de tel n’est mentionné dans la
description. Rappelez-vous, nous devons faire une description suffisament précise pour re-
présenter adéquatement les besoins du client, mais pas trop contraignante pour laisser une
certaine liberté au programmeur. La déclaration idéale de nb pret max est donc la suivante.

nb pret max : N
nb pret max > 0

On définit ensuite un type MESSAGE qui contient les différents messages d’erreurs pos-
sibles qui seront envoyés à l’utilisateur. Bien qu’on écrive ces message au début de la spé-
cification, on ne peut les déterminer avec certitude qu’une fois qu’on a analysé toutes les
opérations. Vous découvrirez plus loin l’utilité exacte de ces messages.

MESSAGE ::= LivreNonDisponible

| NonMembre
| NbPretMaxAtteint
| LivrePasEnStock
| LivreDejaDisponible
| CoteDejaExistante
| DejaMembre
| DoitRetournerSesLivres

On est maintenant prêt à écrire le schéma Bibliotheque. Pour ce schéma, il y a une

multitude de possibilités. Voici une solution possible. Nous déclarerons quatre items qui
contiendront les informations relatives à la bibliothèque, soient stock , emprunt, disponible et
membre. Nous déclarerons stock et emprunt comme des fonctions (observez attentivement
de quelle sorte de fonction il s’agit). Les ensembles disponible et membre sont des sous-
ensembles respectivement de COTE et de LECTEUR. Les choix que nous faisons ici sont
déterminants, mais il y a tout de même plusieurs possibilités. Ce sont les propriétés que nous
imposons au système qui sont cruciales. Par exemple ici, nous demandons que disponible
et dom emprunt soit disjoints mais que leur union donne dom stock . Nous demandons aussi
que les emprunts soient uniquement faits par des membres. Nous imposons finalement que
le nombre d’emprunts maximal soit respecté par tous les emprunteurs.

Pourquoi y a-t-il plusieurs possibilités pour les déclarations de stock , emprunt, disponible
et membre ? Prenons pas exemple membre. Nous aurions pu déclarer que son type est
P LECTEUR et ajouter dans la deuxième partie du schéma que membre doit satisfaire la
propriété F LECTEUR. Bien que les deux soient équivalents, nous préférons habituellement
la première version puisqu’elle est plus concise.

47
 Bibliotheque
stock : COTE → 7 7 LIVRE
emprunt : COTE → 7 7 LECTEUR
disponible : F COTE
membre : F LECTEUR
disponible ∪ dom emprunt = dom stock
disponible ∩ dom emprunt = {}
ran emprunt ⊆ membre
∀ m : membre • #(emprunt B {m}) ≤ nb pret max

Parlons maintenant de l’état initial. Dans l’état initial nous devons décrire (au meilleur
de notre connaissance) l’état dans lequel sera la bibliothèque lors de son ouverture. Ici, plu-
sieurs hypothèses sont possibles. Il serait préférable de demander au client ce qu’il souhaite
avoir, mais profitons-en plutôt pour voir comment nous pouvons modéliser de l’information
partielle.

On suppose donc qu’au départ il n’y a pas encore de membres d’inscrits et qu’aucun
emprunt n’a été effectué. C’est plutôt raisonnable comme hypothèse. Là où différents choix
sont possibles, c’est au niveau du stock. Est-ce que l’on considère que l’ouverture de la
bibliothèque correspond à l’ouverture des locaux, auquel cas il n’y a aucun livre dans le
système ? Considère-t-on plutôt que l’ouverture de la bibliothèque correspond à l’ouverture
des portes aux lecteurs, auquel cas le système est plein de livres ? Nous décidons de ne pas
faire de choix. Voici comment on l’exprime. Nous ne faisons aucune hypothèse sur stock .
Puisque emprunt = {}, on en conclut donc que disponible = dom stock , quel que soit stock .
Nous avons donc donné la valeur de tous les items possibles quand nous ne supposons rien
sur stock .

BibliothequeInit
Bibliotheque
disponible = dom stock
emprunt = {}
membre = {}

La spécification des diverses fonctions ensuite coule de source. Il s’agit de respecter la

notation prescrite par les déclarations précédentes, de respecter les demandes du client et
d’utiliser les opérateurs du langage Z à bon escient. Voici les fonctions demandées.

48
 Emprunter
∆Bibliotheque
c? : COTE
l ? : LECTEUR
c? ∈ disponible
l ? ∈ membre
#(emprunt B {l ?}) < nb pret max
stock 0 = stock
emprunt 0 = emprunt ∪ {(c?, l ?)}
disponible 0 = disponible \ {c?}
membre 0 = membre

LivreNonDisponible
ΞBibliotheque
c? : COTE
rep! : MESSAGE
c? 6∈ disponible
rep! = LivreNonDisponible

NonMembre
ΞBibliotheque
l ? : LECTEUR
rep! : MESSAGE
l ? 6∈ membre
rep! = NonMembre

EmprunterTrop
ΞBibliotheque
c? : COTE
l ? : LECTEUR
rep! : MESSAGE
c? ∈ disponible
l ? ∈ membre
#(emprunt B {l ?}) = nb pret max
rep! = NbPretMaxAtteint

EmprunterTotale =
b Emprunter
∨ LivreNonDisponible
∨ NonMembre
∨ EmprunterTrop

49
 RetournerLivre
∆Bibliotheque
c? : COTE
c? ∈ dom emprunt
stock 0 = stock
emprunt 0 = {c?} − C emprunt
disponible 0 = disponible ∪ {c?}
membre 0 = membre

LivrePasEnStock
ΞBibliotheque
c? : COTE
rep! : MESSAGE
c? 6∈ dom stock
rep! = LivrePasEnStock

LivreDejaDisponible
ΞBibliotheque
c? : COTE
rep! : MESSAGE
c? ∈ disponible
rep! = LivreDejaDisponible

RetournerLivreTotale =
b RetournerLivre
∨ LivrePasEnStock
∨ LivreDejaDisponible

AugmenterStock
∆Bibliotheque
c? : COTE
l ? : LIVRE
c? 6∈ dom stock
stock 0 = stock ∪ {(c?, l ?)}
emprunt 0 = emprunt
disponible 0 = disponible ∪ {c?}
membre 0 = membre

50
 CoteEnStock
ΞBibliotheque
c? : COTE
rep! : MESSAGE
c? ∈ dom stock
rep! = CoteDejaExistante

b AugmenterStock ∨ CoteEnStock
AugmenterStockTotale =

RetirerExemplaire
∆Bibliotheque
c? : COTE
c? ∈ disponible
stock 0 = {c?} −
C stock
emprunt 0 = emprunt
disponible 0 = disponible \ {c?}
membre 0 = membre

RetirerExemplaireTotale =
b RetirerExemplaire
∨ LivreNonDisponible
∨ LivrePasEnStock

ChercherEmpruntsMembre
ΞBibliotheque
l ? : LECTEUR
requete! : F(COTE × LIVRE )
l ? ∈ membre
requete! = dom(emprunt B {l ?}) C stock

ChercherEmpruntsMembreTotale =
b ChercherEmpruntsMembre
∨ NonMembre

ChercherExemplaire
ΞBibliotheque
c? : COTE
requete! : LECTEUR
c? ∈ dom emprunt
requete! = emprunt(c?)

51
ChercherExemplaireTotale =
b ChercherExemplaire
∨ LivreDejaDisponible
∨ LivrePasEnStock

AbonnerNouveauMembre
∆Bibliotheque
l ? : LECTEUR
l ? 6∈ membre
stock 0 = stock
emprunt 0 = emprunt
disponible 0 = disponible
membre 0 = membre ∪ {l ?}

DejaMembre
ΞBibliotheque
l ? : LECTEUR
rep! : MESSAGE
l ? ∈ membre
rep! = DejaMembre

AbonnerNouveauMembreTotale =
b AbonnerNouveauMembre
∨ DejaMembre

ExpulserMembre
∆Bibliotheque
l ? : LECTEUR
l ? ∈ membre
emprunt B {l ?} = {}
stock 0 = stock
emprunt 0 = emprunt
disponible 0 = disponible
membre 0 = membre \ {l ?}

ExpulserMembreAvecEmprunts
ΞBibliotheque
l ? : LECTEUR
rep! : MESSAGE
l ? ∈ membre
emprunt B {l ?} =
6 {}
rep! = DoitRetournerSesLivres

52
 ExpulserMembreTotale =
b ExpulserMembre
∨ NonMembre
∨ ExpulserMembreAvecEmprunts

ChercherLivre
ΞBibliotheque
l ? : LIVRE
requete! : F COTE
l ? ∈ ran stock
requete! = dom(stock B {l ?}) ∩ disponible

b ChercherLivre ∨ LivrePasEnStock
ChercherLivreTotale =

Remarques:
1. Regardez bien les trois cas d’erreur de la fonction Emprunter . Commençons par Em-
prunter Trop. Pour vérifier si quelqu’un peut emprunter un livre de plus (donc pour
s’assurer qu’il n’a pas dépassé le nombre maximal d’emprunts), il faut que la personne
soit membre. Si quelqu’un demande “puis-je prendre un autre livre ?” et qu’il n’est
pas membre, on doit lui répondre : “vous n’êtes pas membre !” Si un membre veut
emprunter un livre de plus, mais que ce livre n’est pas disponible, il ne dépassera pas
la quantité maximale permise, puisqu’il ne pourra pas l’emprunter.

Regardons maintenant NonMembre. On ne vérifie pas la disponibilité du livre, ce n’est

pas nécessaire. À partir du moment où la personne n’est pas membre, elle ne peut
rien emprunter.

C’est un raisonnement semblable pour LivreNonDisponible. On ne vérifie pas si la

personne est membre. Puisque le livre n’est pas disponible, de toutes façons la per-
sonne ne peut pas partir avec ce livre.

Regardez les deux derniers paragraphes, il semble y avoir un problème avec LivreNon-
Disponible et NonMembre. Qu’arrive-t-il si un non-membre demande d’emprunter un
livre qui n’est pas disponible ? Qu’est-ce qui sera retourné par le programme ? Est-ce
LivreNonDisponible, NonMembre ou les deux ? En fait, nous ne savons pas puisque le
programme n’existe pas encore. Rien dans la description initiale ne nous disait quoi
spécifier. Il faudrait alors demander au client ou alors laisser le choix au programmeur
en l’indiquant dans le document de spécification (voir chapitre suivant).
2. En regardant les différents schémas, nous pourrions avoir l’impression que le code
ressemble beaucoup à un langage impératif. Ne vous laissez pas prendre au piège !
Dans ce cas-ci, il est vrai que notre description de ce qui doit être fait laisse croire qu’il

53
 y a aussi de l’information concernant comment ce doit être fait. Voici pourquoi ce n’est
pas exact. D’abord, les différentes informations sont enregistrées dans stock , emprunt,
disponible et membre. Puisqu’il n’y a rien de mentionné concernant la structure de
donnée de chacun de ces items, une expression comme emprunt 0 = emprunt ∪{(c?, l ?)}
ne dit pas comment l’ajout d’information doit être faite. Doit-on faire un ajout dans
une pile, une file, un arbre binaire, un graphe, etc ? Autre question que l’on peut
se poser : À quel endroit de la structure de données (que nous ne connaissons pas)
doit-on faire cet ajout ?

6.2 Tableau des préconditions

Le tableau des préconditions suivants permet, en un coup d’oeil, de nous aider à voir si
tous les cas d’exceptions ont été traités.

Opération Préconditions Exceptions

Emprunter c? ∈  disponible
c? ∈ disponible LivreNonDisponible
=
∧ c? ∈ dom stock LivrePasEnStock
l ? ∈ membre NonMembre
#(emprunter B {l ?})
< nb pret max EmprunterTrop
RetournerLivre c? ∈  dom emprunter
c? ∈ dom stock LivrePasEnStock
=
∧ c? 6∈ disponible LivreDejaDisponible
AugmenterStock c? 6∈ dom stock CoteEnStock
RetirerExemplaire c? ∈  disponible
c? ∈ disponible LivreNonDisponible
=
∧ c? ∈ dom stock LivrePasEnStock
ChercherEmpruntM... l ? ∈ membre NonMembre
ChercherExemplaire c? ∈ dom emprunter ***voir RetournerLivre
Abonner...Membre l ? 6∈ membre DejaMembre
ExpulserMembre l ? ∈ membre NonMembre
emprunter B {l ?} = ∅ Expu...AvecEmprunts
ChercherLivre l ? ∈ ran stock LivrePasEnStock

Pourquoi sépare-t-on la précondition de Emprunter de la façon suivante ?


c? ∈ disponible
c? ∈ disponible =
∧ c? ∈ dom stock

C’est qu’il y a vraiment deux cas. En effet, l’ensemble disponible est inclus dans dom stock
qui est lui-même inclus dans COTE . Ainsi, si c? n’est pas dans disponible, il peut tout de
même être en stock , ou bien il peut ne pas faire partie des livres de la biblothèque.

54
6.3 Conclusion

Vous voyez maintenant à quoi servent les opérateurs présentés aux chapitres 2 et 3. Ces
opérateurs sont très expressifs et permettent de modéliser plus que ce qui est programmable
(par exemple, les ensembles infinis).

Remarquez que plusieurs principes mentionnés depuis le début du cours ne sont pas des
éléments de Z, mais bien des principes utiles en spécification formelle en général. Par exemple,
le fait de décrire correctement les propriétés requises par le système (ou le programme) qui est
modélisé. Nous pouvons aussi penser au principe : on doit faire une description suffisament
précise pour représenter adéquatement les besoins du client, mais pas trop contraignante
pour laisser une certaine liberté au programmeur et sans trop de détails pour qu’elle reste
compréhensible. Le texte d’introduction qui fait référence aux deux articles peut vous aider
à prendre consciences des principes généraux.

Un exemple de concept qui fait surtout référence au langage Z est la façon dont nous
gérons les types. Bien sûr les types existent dans plusieurs contextes différents en informa-
tique, mais la façon dont nous les gérons, plus précisément la définition que nous en avons
donnée est propre au Z. Cette notion précise de type n’en est pas une générale utilisée dans
le monde de la spécification formelle.

55
Chapitre 7

Document de spécification

Comme vous pouvez maintenant vous en douter, une spécification en Z d’un système
complexe peut être difficile à décoder, même pour un fin connaisseur, aussi une spécification
formelle ne vient jamais seule. Elle est toujours accompagnée de commentaires qui en ex-
pliquent les grandes lignes. La différence entre ce document et une spécification informelle
(sous forme d’un texte par exemple) est l’utilisation d’un langage formel (donc ayant des
bases mathématiques) qui enlève toute ambiguïté dans la description du système. La ques-
tion devient donc : une fois la spécification formelle terminée, quelle forme devrait prendre
le document qui sera remis aux ingénieurs logiciels qui vont suivre dans le processus de dé-
veloppement du logiciel ?

7.1 Le document de spécification

D’abord, il faut savoir qu’il n’y a pas de réponse absolue à cette question. Plusieurs façons
de faire sont possibles, plusieurs d’entre elles s’équivalent. Les entreprises ont souvent des
normes maison très adéquates. Pour les besoins de ce cours, on va regarder une approche
basée sur des idées 1 développées dans les laboratoires du IBM Hursley et du Oxford Univer-
sity Programming Research Group. C’est bien sûr que vous n’aurez pas un projet de grande
envergure à remettre lors des travaux pratiques qui viennent mais ce document reste très
utile pour lire une spécification formelle.

Nous suggérons donc que le document qui accompagne la spécification formelle soit formé
des éléments suivants.
1. Introduction. On présente le contexte et les grandes lignes du système spécifié. Les
gens qui consulteront ce document doivent savoir de quoi nous parlons !
1. Il s’agit aussi de la théorie présentée dans Potter, B., Sinclair J., Till, D., An Introduction to Formal
Specification and Z.

56
2. Description des ensembles (types) et des différentes constantes. Dans cette
section du rapport, on fournit d’abord la spécification formelle des différents types
et constantes. On décrit aussi de façon textuelle chacun de ces types et constantes
lorsque nécessaire.

Le but est d’aider le programmeur à comprendre notre spécification et à faire des choix
judicieux qui vont respecter les propriétés spécifiées. Comme nous l’avons vu déjà, cer-
tains types sont parfois extrêmement précis, mais nous ne pouvons pas pour autant
spécifier quelles sont leurs propriétés. C’est le cas par exemple de MATERNELLE
et ETRANGERE dans le Dictionnaire. Il est donc très important de donner tous
les détails. Le programmeur qui va suivre va alors réaliser qu’un ensemble comme
MATERNELLE qui contient tous les mots de la langue maternelle correctement or-
thographiés ne sera probablement pas programmé en tant que tel et il devra faire des
choix à l’implémentation. Dans ce cas-ci, la description de ces ensembles est nécessaire.

De même pour les constantes, on explique ce qu’elles représentent. On doit détailler

toutes les propriétés qui concernent notre spécification, mais il ne s’agit pas pour
autant de TOUTES les propriétés de la constante (ou du type) en question. Il est très
fréquent qu’une spécification force le programmeur qui va suivre à faire des choix. Par
exemple, nous pourrions définir une constante
entier max : N
entier max > 0
en expliquant qu’il s’agit du plus grand entier qui sera manipulé par le programme
et que l’on considère que entier max > 0. Ce n’est probablement pas suffisant pour
le programmeur, il devra prendre des décisions lors l’implémentation. Pourtant, notre
description est complète pour cette constante... notre job est faite !
3. Présentation de toute théorie utile. Par exemple, pour la spécification formelle
d’une centrale nucléaire, il peut être utile de fournir quelques explications pour com-
prendre les détails de la spécification. Entre autres, quelques rappels de lois de phy-
sique nucléaire pourraient s’avérer utiles.
4. Description des états standards du système et des propriétés qu’ils doivent
satisfaire. On fournit ici la spécification formelle d’un état standard valide pour
chacune des composantes du système. Ici aussi, on doit fournir des explications sup-
plémentaires lorsque c’est nécessaire. Bien que le nom des différentes variables utilisées
soit habituellement le plus représentatif possible, il peut toujours rester une ambiguïté
quant à l’utilité précise de chacun de ces éléments.
5. Description d’un état initial. Dans cette partie du rapport, on fournit la spécifica-
tion formelle d’un état initial valide du système. En fait, il peut y en avoir plus d’un
si l’on veut laisser une certaine liberté au programmeur. Si des indications doivent
être données aux ingénieurs logiciels qui vont suivre dans la suite du processus de
développement quant à l’état initial, c’est ici qu’il faut le faire.

57
 6. Description des différentes fonctions. On présente ici la spécification formelle des
différentes fonctions du système. On ne présente que la spécification qui correspond
aux conditions normales d’exécution, c’est-à-dire que l’on ne fait pas mention des cas
d’erreurs ou des cas d’exceptions. Le tout doit toujours être accompagné de toute
explication supplémentaire nécessaire.
7. Préconditions, postconditions et invariants de chacune des fonctions. Pour
chacune des fonctions partielles (c’est-à-dire la version qui correspond aux conditions
normales d’exécution), on présente le tableau que l’on retrouve dans le document sur
la théorie du contrat.
8. Description des fonctions totales. On présente ici la spécification formelle de
la version totale des différentes fonctions. On doit donc présenter ici comment les
fonctions réagissent dans les différents cas d’erreurs ou d’exceptions. Si, pour une
raison ou pour une autre, on décide de ne pas rendre totale une certaine fonction, il
faut expliquer pourquoi.
9. Résumé et index. La spécification formelle d’un système peut rapidement devenir
un très gros document. Il est alors utile d’avoir une liste des variables et des différents
noms de schémas utilisés ainsi que le numéro des pages où ils apparaissent.

7.2 Exemple : la Bibliotheque

Voici à quoi pourrait ressembler le document de spécification formelle dans l’exemple de

la Bibliotheque.

1. Introduction Voici la spécification formelle d’une bibliothèque. Il s’agit d’une bi-

bliothèque très simple, avec peu d’options, mais tout de même fonctionnelle. Voici ses
caractéristiques.

— Plusieurs lecteurs visitent cette bibliothèque, mais seuls les membres peuvent em-
prunter des livres.
— Chaque copie d’un livre est identifié par une cote unique.
— La bibliothèque n’a pratiquement jamais tous ses livres en stock. Certains sont
empruntés et d’autres sont disponibles.
— Un membre ne peut emprunter autant de livres qu’il le désire.
Dans cette bibliothèque, on doit pouvoir gérer correctemement les activités suivantes.
— Prêter un livre à un membre.
— Un membre doit pouvoir retourner un livre à la bibliothèque.
— Ajouter des livres à son stock.
— Retirer des livres de son stock.
— Avoir la liste des livres empruntés par un membre en particulier.
— Savoir quel membre a emprunté une copie précise d’un livre.

58
 — Abonner un nouveau membre.
— Mettre un membre à la porte.
— Connaître les cotes correspondantes à un livre en particulier. Nous ne voulons que
les cotes des livres disponibles.
2. Description des types et des différentes constantes. Le nombre de livre maxi-
mal qu’un membre peut emprunter est noté nb pret max . Il y a les types Cote, Livre
et Lecteur . Le type Cote représente l’ensemble des cotes possibles (utilisées ou non).
Le type Livre représente l’ensemble des livres possibles (peu importe que la biblio-
thèque les possède ou non). On peut penser que chaque élément de type Livre contient
des informations utiles comme l’auteur, le titre, l’année de publication, etc. Le type
Lecteur représente l’ensemble des lecteurs possibles (membres ou non). On peut pen-
ser que chaque élément de type Lecteur contient des informations utiles comme le
nom, l’adresse, le numéro de téléphone, etc.

On a finalement le type Message qui contient les messages possiblement retournés

à l’utilisateur par le système en cas d’erreur. Voici la spécification de ces types et
constantes.

[COTE , LIVRE , LECTEUR]

nb pret max : N
nb pret max > 0

MESSAGE ::= LivreNonDisponible

| NonMembre
| NbPretMaxAtteint
| LivrePasEnStock
| LivreDejaDisponible
| CoteDejaExistante
| DejaMembre
| DoitRetournerSesLivres

3. Présentation de toute théorie utile. Nous parlons d’une bibliothèque. Y a des

questions ?
4. Description des états standards du système. Nous représentons le stock de livre
de la bibliothèque par une fonction partielle finie qui associe une cote à un livre. Nous
représentons les emprunts effectués par les membres par une fonction partielle finie
qui associe une cote à un membre. L’ensemble des livres disponibles sera l’ensemble
(fini) disponible et l’ensemble des membres sera l’ensemble (fini) membre. Voici la
spécification formelle d’un état valide du système.

59
 Bibliotheque
stock : COTE → 7 7 LIVRE
emprunt : COTE → 7 7 LECTEUR
disponible : F COTE
membre : F LECTEUR
disponible ∪ dom emprunt = dom stock
disponible ∩ dom emprunt = {}
ran emprunt ⊆ membre
∀ m : membre • #(emprunt B {m}) ≤ nb pret max

5. Description d’un état initial. Nous ne savons pas si l’état initial correspond à
l’ouverture de la bibliothèque au public (auquel cas elle est pleine de livres) ou si
l’état initial correspond à l’ouverture des locaux et la mise en place du système (au-
quel cas elle ne possède pas de livre pour le moment). Nous laissons donc le choix au
programmeur. Nous obtenons l’état initial suivant.

BibliothequeInit
Bibliotheque
disponible = dom stock
emprunt = {}
membre = {}

6. Description des différentes fonctions.

Cette partie est omise dans les notes. Chaque fonction doit être expliquée, chaque
ligne complexe doit être justifiée.
7. Préconditions, postconditions et invariants de chacune des fonctions. Exer-
cice #2 de la série sur la bibliothèque.
8. Description des fonctions totales. Voici les versions totales des différentes fonc-
tions spécificiées. Il n’y aucun comportement qui soit critique. Chaque cas particulier
ne fait qu’envoyer un message à l’utilisateur lui indiquant que l’opération qu’il veut
effectuer n’est pas conforme ainsi que la raison pour laquelle cette opération n’est pas
conforme.

La fonction

EmprunterTotale =
b Emprunter
∨ LivreNonDisponible
∨ NonMembre
∨ EmprunterTrop

avec

60
 LivreNonDisponible
ΞBibliotheque
c? : COTE
rep! : MESSAGE
c? 6∈ disponible
rep! = LivreNonDisponible

NonMembre
ΞBibliotheque
l ? : LECTEUR
rep! : MESSAGE
l ? 6∈ membre
rep! = NonMembre

EmprunterTrop
ΞBibliotheque
c? : COTE
l ? : LECTEUR
rep! : MESSAGE
c? ∈ disponible
l ? ∈ membre
#(emprunt B {l ?}) = nb pret max
rep! = NbPretMaxAtteint

Notez que nous ne précisons pas ce qui survient si un non-membre demande d’emprun-
ter un livre qui n’est pas disponible. Le message retourné par le programme pourrait
être LivreNonDisponible, NonMembre ou les deux. Le choix devra être fait dans les
étapes qui suivent.

La fonction

RetournerLivreTotale =
b RetournerLivre
∨ LivrePasEnStock
∨ LivreDejaDisponible

avec

61
 LivrePasEnStock
ΞBibliotheque
c? : COTE
rep! : MESSAGE
c? 6∈ dom stock
rep! = LivrePasEnStock

LivreDejaDisponible
ΞBibliotheque
c? : COTE
rep! : MESSAGE
c? ∈ disponible
rep! = LivreDejaDisponible

La fonction
AugmenterStockTotale =
b AugmenterStock
∨ CoteEnStock
avec
CoteEnStock
ΞBibliotheque
c? : COTE
rep! : MESSAGE
c? ∈ dom stock
rep! = CoteDejaExistante

La fonction
RetirerExemplaireTotale =
b RetirerExemplaire
∨ LivreNonDisponible
∨ LivrePasEnStock
La fonction
ChercherEmpruntsMembreTotale =
b ChercherEmpruntsMembre
∨ NonMembre
La fonction
ChercherExemplaireTotale =
b ChercherExemplaire
∨ LivreDejaDisponible
∨ LivrePasEnStock

62
 La fonction
AbonnerNouveauMembreTotale =
b AbonnerNouveauMembre
∨ DejaMembre
avec
DejaMembre
ΞBibliotheque
l ? : LECTEUR
rep! : MESSAGE
l ? ∈ membre
rep! = DejaMembre

La fonction
ExpulserMembreTotale =
b ExpulserMembre
∨ NonMembre
∨ ExpulserMembreAvecEmprunts
avec
ExpulserMembreAvecEmprunts
ΞBibliotheque
l ? : LECTEUR
rep! : MESSAGE
l ? ∈ membre
emprunt B {l ?} =
6 {}
rep! = DoitRetournerSesLivres

La fonction
ChercherLivreTotale =
b ChercherLivre
∨ LivrePasEnStock
9. Résumé et index. Il faudrait écrire ici une liste des types, ensembles, constantes,
schémas et fonctions ainsi que les pages auxquelles nous retrouvons ces items.

7.3 Conclusion

À quoi sert la spécification formelle si, de toutes façons, elle est accompagnée d’un texte ?
En plus de permettre tout ce que nous avons déjà mentionné dans les chapitres précédents,
elle permet de créer un document de spécification dans lequel il n’y a plus d’ambiguïtés. Elle
permet aussi de créer un document de spécification beaucoup plus succint.

63
Chapitre 8

Perfect Developer

Ce chapitre présente une introduction à l’outil Perfect Developer qui vous sera utile dans
votre apprentissage de cet outil. Voici un aperçu du contenu du chapitre (dans l’ordre) :
1. Quelques notations Perfect est une section de notation rapide qui vous permettra
de faciliter la transition entre Z (et Object-Z) et Perfect. Il est bien d’en avoir une
copie près de soi lorsque vous utilisez Perfect Developer !
2. Un aperçu de l’exemple de la bibliothèque est une section qui vous présente
une traduction de l’exemple de la bibliothèque (vu au chapitre 6) en langage Perfect.
Notez cependant qu’avant d’aborder ce chapitre, il est nécessaire de consulter l’extrait
du tutoriel d’un jour (voir en annexe A), Les fondements de Perfect Developer, réalisé
par Escher Technologies (la compagnie qui développe cet outil). Il vous apprendra les bases
de la syntaxe de l’outil et quelques indices sur sa configuration.

8.1 Quelques notations Perfect

Types
La déclaration [ENSTYPE1, ENSTYPE2] est obtenue par class Enstype1 ^= tag ;
class Enstype2 ^= tag ;
Pour définir un type fini NOM : := nom1|nom2|nom3 on déclare class NOM ^= enum nom1,
nom2,nom3 end ; et on l’utilise ainsi nom1@NOM
Si c est de type set of T et p(x ) est une expression booléenne qui contient x :

64
 Expression Type de retour f quivalent Z
forall x::c :- p(x) bool ∀ x : c • p(x )
forall x : T :- p(x) ∀ x : T • p(x )

exists x::c :- p(x) bool ∃ x : c • p(x )

exists x : T :- p(x) ∃ x : T • p(x )

that x::c :- p(x) T ∃ x : C • {x : c | p(x )} = {x } retourne ce x

any x::c :- p(x) ∃ x : C • p(x ), retourne un tel x

those x::c :- p(x) set of T {x : c | p(x )}

for x::c yield v(x) set of type of v {x : c • v (x )}

for those x::c :- p(x) yield v(x) {x : c | p(x ) • v (x )}

Soient A, B : P T , f : A → C , x ∈ A, y ∈ C , p : A×B.
Perfect : A,B: set of T, f: map of (A->C), x: A, y:C, p: pair of (A,B)
Description Perfect Z
Négation ∼ ¬
Différent de ∼= 6=
Cardinalité #A #A
Appartenance x in A x ∈A
Inclusion stricte A<<B A⊆B
Inclusion A<<=B A⊂B
Union (set et map) A++B A∪B
Intersection A**B A∩B
Intersection map f **A ACf
Différence (set) A−−B A\B
Différence (map) f−−A A−Cf
Domaine (pas pour paires) [Link] dom f
Image [Link] ran f

enlever élément (set) [Link](x) A \ {x }

map (aussi pour seq, bag) [Link](x) {x } −
Cf
ajouter élément (set) [Link](x) A ∪ {x }
map (aussi pour seq, bag) [Link](x->y) f ∪ {x → y} attention append a une précondition

fonction vers ensemble [Link] une fonction est déjà un ensemble de paires
1er élément d’une paire p.x first (p)
2e élément d’une paire p.y second (p)
1er,2e,3e élément d’un triplet t.x, t.y, t.z aucun équivalent
Toutes les méthodes reliées aux fonctions (map of (X->Y)), aux ensembles, suites, bags,
etc. sont énumérées dans l’annexe de Language reference manual.

65
8.2 Un aperçu de l’exemple de la bibliothèque
Perfect peut être considéré comme un langage orienté objet, car il dispose des principales
caractéristiques d’un tel langage. On doit tenir compte de cette caractéristique lorsque l’on
part d’une spécification Z pour créer un code équivalent en Perfect.

État général
Un état général d’une spécification Z s’exprime au moyen d’une classe en Perfect. Soit
l’état général suivant :

Bibliotheque
stock : COTE → 7 7 LIVRE
emprunt : COTE → 7 7 LECTEUR
disponible : F COTE
membre : F LECTEUR
disponible ∪ dom emprunt = dom stock
disponible ∩ dom emprunt = {}
ran emprunt ⊆ membre
∀ m : membre • #(emprunt B {m}) ≤ nb pret max

Il correspond au code Perfect suivant :

c l a s s B i b l i o t h e q u e ^=
abstract
var
s t o c k : map of ( Cote −> L i v r e ) ,
emprunt : map of ( Cote −> L e c t e u r ) ,
d i s p o n i b l e : set of ( Cote ) ,
membre : set of ( L e c t e u r ) ;
const
nb_pret_max : i n t ^= ? ;
invariant
d i s p o n i b l e ++ emprunt . dom = s t o c k . dom ,
d i s p o n i b l e ∗∗ emprunt . dom = set of ( Cote ) { } ,
emprunt . ran <<= membre ,
f o r a l l m: : membre :− #(those e : : emprunt . p a i r s :− e . y = m) <= nb_pret_max ;
end ;

La partie entre le mot-clé var et le caractère ’ ;’ correspond à la déclaration en Z. La

partie entre invariant et le caractère ’ ;’ correspond aux prédicats en Z. Le ’ ?’ spécifie que
la valeur est quelconque.

Attention, cela ne compile pas directement ! LECTEUR n’est pas défini, ni COTE, ni
LIVRE. De plus, il manque le constructeur qui, comme on le verra plus loin, correspond à

66
un état initial en Z.

Note : On peut demander à Perfect de générer un squelette de classe qu’il ne reste plus
qu’à remplir. Pour ce faire, sélectionner l’item ’Create file ...’ du menu Project.
Voici ce que contient le fichier Bibliotheque qu’il génère :
// ∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗
// ∗ F i l e : \\ L e D o s s i e r \ B i b l i o t h e q u e . pd
// ∗ Author : A u t o m a t i c a l l y g e n e r a t e d by P e r f e c t D e v e l o p e r
// ∗ Created : 1 1 : 3 2 : 3 9 on F r i d a y May 4 t h 2007 UTC
// ∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗∗

c l a s s B i b l i o t h e q u e ^=
abstract
// Add v a r i a b l e , i n v a r i a n t and p r i v a t e method d e c l a r a t i o n s h e r e . . .
interface
// Add p u b l i c a c c e s s f u n c t i o n , s e l e c t o r and method d e c l a r a t i o n s h e r e . . .
// . . .
build {}
post ? ;
end ;

// End

Créer des types

Pour déclarer un type tel Livre ou Cote, on doit créer une classe. Soit les types Z suivants :

67
 [COTE , LIVRE , LECTEUR]

Le code Perfect correspondant sera :

c l a s s Cote ^= tag ;
c l a s s L i v r e ^= tag ;
c l a s s L e c t e u r ^= tag ;

Il signifie à peu près la même chose qu’en Z : ce sont des ensembles de taille que nous
n’excéderons jamais.

En ce qui concerne l’état initial, il est exprimé sous la forme d’un constructeur.

Soit l’état initial suivant :

BibliothequeInit
Bibliotheque
disponible = dom stock
emprunt = {}
membre = {}

Le code Perfect correspondant sera :

build { s : map of ( Cote −> L i v r e ) }
post
d i s p o n i b l e ! = s t o c k ’ . dom ,
emprunt ! = map of ( Cote −> L e c t e u r ) { } ,
membre ! = set of ( L e c t e u r ) { } ,
stock ! = s ;

Remarquez que pour exprimer que la spécification ne spécifie pas ce que le stock contient
(ou s’il est vide), on passe un stock par paramètre. On ne peut pas simplement omettre de
spécifier stock’ comme en Z.

Variables primés
On utilise variable’ comme en Z, pour exprimer des propriétés d’une variable après l’opé-
ration. Par contre, on doit indiquer explicitement que l’on veut modifier une variable.
change v a r i a b l e s a t i s f y v a r i a b l e ’ = n o u v e l l e _ v a l e u r

Ceci est un peu lourd mais possède un raccourci (utilisé dans le constructeur de la bi-
bliothèque ci-haut). Quand on a la valeur exacte que l’on veut donner à cette variable, on
peut utiliser le raccourci suivant :
variable ! = nouvelle_valeur

68
 Par exemple, on pourrait spécifier l’état initial précédent de la façon suivante :
build { s : map of ( Cote −> L i v r e ) }
post
( change d i s p o n i b l e s a t i s f y d i s p o n i b l e ’ = s t o c k ’ . dom ) ,
emprunt ! = map of ( Cote −> L e c t e u r ) { } ,
membre ! = set of ( L e c t e u r ) { } ,
stock ! = s ;

La plupart du temps, «variable ! = nouvelle valeur» est suffisant. Par contre, pour une
postcondition comme la suivante, on n’a pas le choix d’utiliser l’alternative :
change v a r i a b l e s a t i s f y v a r i a b l e ’ . dom = a u t r e _ v a r i a b l e . ran

Opération n’altérant pas l’état

Soit le schéma suivant :

ChercherLivre
ΞBibliotheque
l ? : LIVRE
requete! : F COTE
l ? ∈ ran stock
requete! = dom(stock B {l ?}) ∩ disponible

Le code Perfect correspondant sera :

schema c h e r c h e r L i v r e ( l : L i v r e , r e q u e t e ! : out set of ( Cote ) )
pre
l in s t o c k . ran

post
r e q u e t e ! = (map of ( Cote −> L i v r e )
{ those s : : s t o c k . p a i r s :− s . y = l } ) . dom ∗∗ d i s p o n i b l e ;

Le point d’exclamation après requête n’est pas une convention pour dire que requete est
une variable de sortie. Il signifie plutôt que requête sera modifié par le schéma. Le mot-
clé out avant le type veut dire que la valeur initiale de requete n’est pas importante :
l’implémentation ne devra pas la considérer.

Opération altérant l’état

Soit le schéma suivant :

69
 AbonnerNouveauMembre
∆Bibliotheque
l ? : LECTEUR
l ? 6∈ membre
stock 0 = stock
emprunt 0 = emprunt
disponible 0 = disponible
membre 0 = membre ∪ {l ?}

Le code Perfect correspondant sera :

schema ! abonnerNouveauMembre ( l : L e c t e u r )
pre
~( l in membre )

post
stock ! = stock ,
emprunt ! = emprunt ,
disponible ! = disponible ,
membre ! = membre . append ( l ) ;

Remarquez le point d’exclamation avant abonnerNouveauMembre. Il signifie que abon-

nerNouveauMembre altérera l’état de la bibliothèque. En fait, les 3 premières post-conditions
sont inutiles en Perfect, contrairement à ce qui doit être fait en Z. En effet, tout variable
modifiée doit l’être de façon explicite, ce qui implique que celles qui ne sont pas mentionnées
ne sont pas modifiées.

Opération totale
On pourrait représenter la fonction totale suivante :

b Emprunter ∨ LivreNonDisponible ∨ NonMembre ∨ EmprunterTrop

EmprunterTotale =

comme ceci :
schema ! EmprunterTotale ( c : Cote , l : L e c t e u r , r e p ! : MESSAGE)

post
(
[ c in d i s p o n i b l e
& l in membre
& #(those e : : emprunts . p a i r s :− e . y = l ) < nb_pret_max ] :
Emprunter ( c , l ) ,
r e p != ok@MESSAGE,
[ c ~in d i s p o n i b l e ] : r e p !=LivreNonDisponible@MESSAGE ,
[ l ~in membre ] : r e p !=NonMembre@MESSAGE,
[ c in d i s p o n i b l e

70
 & l in membre
& #(those e : : emprunts . p a i r s :− e . y = l ) = nb_pret_max ] :
r e p != NbPretMaxAtteint@MESSAGE
);

Perfect générera une obligation de preuve vérifiant qu’au moins une des contitions du
choix est vraie. Ceci vérifie que tous les cas sont effectivement traités. Par contre la première
condition qui est vraie est celle qui est choisie. Si nous voulons vraiment du non-déterminisme
comme en Z, nous devons ajouter opaque avant la première condition et avant schema.
En résumé, le code suivant définit une bibliothèque contenant l’état général, l’état initial
et quelques opérations (voir page suivante) :

71
//−−−−−−−−−Les t y p e s de base−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−
c l a s s Cote ^= tag ;
c l a s s L i v r e ^= tag ;
c l a s s L e c t e u r ^= tag ;

//−−−−−−−−−L ’ é t a t g é n é r a l −−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−
c l a s s B i b l i o t h e q u e ^=
abstract
var
s t o c k : map of ( Cote −> L i v r e ) ,
emprunt : map of ( Cote −> L e c t e u r ) ,
d i s p o n i b l e : set of ( Cote ) ,
membre : set of ( L e c t e u r ) ;

const
nb_pret_max : i n t ^= ? ;

invariant
d i s p o n i b l e ++ emprunt . dom = s t o c k . dom ,
d i s p o n i b l e ∗∗ emprunt . dom = set of ( Cote ) { } ,
emprunt . ran <<= membre ,
f o r a l l m: : membre :− #(those e : : emprunt . p a i r s :− e . y = m) <= nb_pret_max ;

interface
//−−−−−−−L ’ é t a t i n i t i a l −−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−
build { s : map of ( Cote −> L i v r e ) }
post
d i s p o n i b l e ! = s t o c k ’ . dom ,
emprunt ! = map of ( Cote −> L e c t e u r ) { } ,
membre ! = set of ( L e c t e u r ) { } ,
stock ! = s ;

//−−−−−−−Schéma : O b t e n i r l e s d i f f é r e n t e s c o t e s d ’ un l i v r e −−−−−−−−−−−−−−
schema c h e r c h e r L i v r e ( l : L i v r e , r e q u e t e ! : out set of ( Cote ) )
pre
l in s t o c k . ran
post
r e q u e t e ! = (map of ( Cote −> L i v r e )
{ those s : : s t o c k . p a i r s :− s . y = l } ) . dom ∗∗ d i s p o n i b l e ;

//−−−−−−−Schéma : Abonner un nouveau membre −−−−−−−−−−−−−−

schema ! abonnerNouveauMembre ( l : L e c t e u r )
pre
~( l in membre )
post
stock ! = stock ,
emprunt ! = emprunt ,
disponible ! = disponible ,
membre ! = membre . append ( l ) ;

end ;

72
Chapitre 9

Démonstration de propriétés

Le but de la spécification formelle est de minimiser les erreurs commises dans la concep-
tion d’un logiciel et ce, le plus tôt possible dans le processus de développement. Les méthodes
formelles proposent de travailler avec un prototype du logiciel décrit à l’aide d’outils ma-
thématiques. On veut que cette description soit très précise quant aux besoins du client et
qu’elle permette d’éviter toute anomalie. Pour ce faire, nous démontrerons des théorèmes
qui nous aiderons à s’assurer que le logiciel qui sera programmé va satisfaire les besoins du
client et qu’il n’y aura aucune mauvaise surprise.

Quelles sont donc les propriétés (voire les théorèmes) que nous allons démontrer ? Le Z
(et l’outil Z-eves) nous permet de faire la démonstration de plusieurs théorèmes. Quels sont
ceux qui nous intéressent ? On ne peut pas TOUT démontrer. Sur quelles propriétés va-t-on
se concentrer et pourquoi ? Si le but est de minimiser le nombre d’erreurs, n’est-il pas naturel
de croire que plus on démontre de propriétés, plus on minimise le nombre d’erreurs possibles
lors des étapes subséquentes du développement du logiciel en question ?

En fait, nous verrons que trois théorèmes bien précis nous permettent de démontrer que
le système ne sera jamais dans un état indésirable, c’est-à-dire qu’il satisfera toujours les
propriétés pour lesquelles il a été conçu (les invariants du système). Deux de ces théorèmes
doivent être démontrés pour plusieurs déclarations. Il y a donc plusieurs preuves à faire. Un
autre fait référence à l’état initial seulement. Une fois tous ces théorèmes démontrés, on peut
montrer (et nous allons le faire) que le logiciel, du moins son prototype en Z, est à la hauteur
de nos attentes.

Vous allez voir que le démonstrateur semi-automatique de Z-eves est très capricieux.
Dans certains cas, il est très fastidieux d’arriver à démontrer TOUS les théorèmes men-
tionnés précédemment. C’est pourquoi les quelques cas documentés d’utilisation du Z en
industrie expliquent que peu de théorèmes sont démontrés avec l’outil Z-eves (ou avec un
équivalent). La plupart des preuves sont effectuées à la main et il est fréquent qu’elles ne
soient pas toutes complétées.

73
 Dans le cadre de ce cours, nous allons d’abord nous concentrer à comprendre les démons-
trations “à la main” des différents théorèmes. Nous allons ensuite étudier en profrondeur
(du moins autant que possible) le démonstrateur semi-automatique. C’est très instructif de
manipuler un démonstrateur semi-automatique une fois dans sa vie. Notre objectif sera donc
d’arriver à tout démontrer... mission impossible ?

9.1 Vérification de domaine

L’outil Z-eves vérifie la syntaxe ainsi que le typage des différentes déclarations. La pre-
mière colonne qui se trouve à la gauche de la spécification indique un y (pour yes) lorsque
la syntaxe et le typage de votre déclaration sont corrects et un n (pour no) sinon.

Dans la deuxième colonne, Z-eves effectue une vérification de domaine. Il apparaît souvent
un n dans cette colonne parce que le démonstrateur de Z-eves est limité. Cela ne signifie pas
que vous avez une erreur, mais plutôt que Z-eves n’arrive pas à démontrer que vous n’avez pas
d’erreur. C’est le premier endroit où nous devrons aider le démonstrateur semi-automatique
à faire son travail.

Les premiers théorèmes à démontrer concernent donc la vérification de domaine. Mais

qu’entendond-on par vérification de domaine ? On veut tout simplement s’assurer que toutes
les fonctions sont utilisées correctement. Par exemple, pour l’opérateur #, il faut qu’il soit
appliqué sur un ensemble fini. Un autre exemple, supposons que l’on définit deux types
[X , Y ]
et une fonction
f :X →
7 Y.
Si, dans un schéma quelque part dans la spécification, pour une raison ou pour une autre,
il est écrit f (a), alors il faut vérifier que a ∈ dom f . En théorie, c’est une vérification que
l’on doit faire pour toutes les déclarations. En pratique, plusieurs déclarations ne sont pas à
vérifier, pensons par exemple à une déclaration de la forme
[X ]
où il n’y a rien à démontrer puisqu’aucune fonction n’est utilisée ! Prenons aussi l’exemple
suivant.
suppr , fleche gauche, fleche droite, inser : TOUCHE
suppr 6∈ CARACTERE
fleche gauche 6∈ CARACTERE
fleche droite 6∈ CARACTERE
inser 6∈ CARACTERE

74
Il n’y a rien à démontrer non plus. Les opérateurs ∈ et 6∈ s’appliquent sur tout élément et sur
tout ensemble. Z-eves est tout à fait capable de réaliser par lui-même que tous les opérateurs
sont utilisés correctement. Par contre, si l’on écrit

Bibliotheque
stock : COTE → 7 7 LIVRE
emprunt : COTE → 7 7 LECTEUR
disponible : F COTE
membre : F LECTEUR
disponible ∪ dom emprunt = dom stock
disponible ∩ dom emprunt = {}
ran emprunt ⊆ membre
∀ m : membre • #(emprunt B {m}) ≤ nb pret max

il faudrait vérifier que emprunt B{m} est un ensemble fini. En clair, il faut démontrer l’énoncé
suivant (écrit à l’aide de la notation en schémas).

Bibliotheque
stock : COTE → 7 7 LIVRE
emprunt : COTE → 7 7 LECTEUR
disponible : F COTE
membre : F LECTEUR
disponible ∪ dom emprunt = dom stock
disponible ∩ dom emprunt = {}
ran emprunt ⊆ membre
∀ m : membre • #(emprunt B {m}) ≤ nb pret max

⇒ emprunt B {m} ∈ dom #

On appelera ce théorème Bibliotheque$domainCheck . On peut le démontrer de la façon sui-
vante.

Bibliotheque
stock : COTE → 7 7 LIVRE
emprunt : COTE → 7 7 LECTEUR
disponible : F COTE
membre : F LECTEUR
disponible ∪ dom emprunt = dom stock
disponible ∩ dom emprunt = {}
ran emprunt ⊆ membre
∀ m : membre • #(emprunt B {m}) ≤ nb pret max

75
 ⇒ hLogique i
emprunt ∈ COTE → 7 7 membre
⇒ hDéfinition de → 77 i
emprunt ∈ COTE → 7 membre
∧emprunt ∈ F(COTE × membre)
⇒ hDéfinition de F i
emprunt ∈ dom #
⇒ hCar emprunt . {m} ⊆ emprunt i
emprunt . {m} ∈ dom #
Regardons un autre exemple, prenons la fonction suivante.

ChercherExemplaire
ΞBibliotheque
c? : COTE
requete! : LECTEUR
c? ∈ dom emprunt
requete! = emprunt(c?)

Ici, pour vérifier que toutes les fonctions sont utilisées correctement par rapport à leur
domaine, il faut vérifier que c? ∈ dom emprunt. Formellement, il faut démontrer le théorème
suivant que nous appelerons ChercherExemplaire$domainCheck .
ChercherExemplaire
ΞBibliotheque
c? : COTE
requete! : LECTEUR
c? ∈ dom emprunt
requete! = emprunt(c?)

⇒ c? ∈ dom emprunt
C’est très simple à démontrer ! Exactement le genre de théorème que Z-eves arrive à démon-
trer sans aide ! Voici comment y arriver.

ChercherExemplaire
ΞBibliotheque
c? : COTE
requete! : LECTEUR
c? ∈ dom emprunt
requete! = emprunt(c?)

76
 ⇒ hLogique i
c? ∈ dom emprunt

On peut résumer cette section de la façon suivante. Quand on écrit une spécification en
Z, Z-eves crée automatiquement un théorème de $domainCheck pour chacune de nos décla-
rations et essaie de tout démontrer. Le résultat de sa tentative de démonstration appraraît
dans la colonne de droite de chaque déclaration. S’il réussit, il inscrit un y. S’il échoue, il
inscrit plutôt un n. C’est alors que notre travail commence : nous devons aller suggérer des
pistes de preuves au démonstrateur semi-automatique.

Le premier théorème que l’on doit démontrer est donc le théorème de $domainCheck .
Il doit être démontré pour chaque déclaration. Souvent, Z-eves en démontre plusieurs par
lui-même.

9.2 Théorème de l’état initial

Une fois que le domaine a été vérifié pour toutes les fonctions utilisées dans chacune des
déclarations de la spécification, nous savons que cette spécification est mathématiquement
correcte. Il faut maintenant voir si elle décrit des états valides et des fonctions qui n’envoient
le système que sur des états valides. Le premier théorème à démontrer dans ce sens est le
théorème d’initialisation. Par exemple, dans le cas du dictionnaire, nous avons les schémas
suivants.

Dictionnaire
Paires : F(MATERNELLE × ENTRANGERE )
Paires ⊆ PAIRES CORRECTES

et

DictionnaireInit
Dictionnaire
Paires = {}

Le théorème d’initialisation que nous appellerons InitialisationDictionnaire s’énonce com-

me suit.
∃ Dictionnaire • DictionnaireInit
Voici comment nous le démontrons.

77
 ∃ Dictionnaire • DictionnaireInit
⇔ hDéfinition de DictionnaireInit i

DictionnaireInit
∃ Dictionnaire • Dictionnaire
Paires = {}
⇔ hLogique : distributivité de ∧ sur ∃ i
∃ Dictionnaire • Paires = {}
⇔ hDéfinition de Dictionnaire i

∃[Paires : F(MATERNELLE × ENTRANGERE )

| Paires ⊆ PAIRES CORRECTES ] • Paires = {}
⇔ hLogique : transfert i

∃ Paires : F(MATERNELLE × ENTRANGERE )

• Paires ⊆ PAIRES CORRECTES ∧ Paires = {}
⇔ hAxiome du point i

{} ∈ F(MATERNELLE × ENTRANGERE )
∧ {} ⊆ PAIRES CORRECTES
⇔ hThéorie des ensembles i

true

Mais quel est cet axiome du point ? Il s’agit d’un axiome très utile en logique pour se
débarasser du quantificateur ∃ lorsque la valeur est suggérée par le prédicat. Dans la preuve
précédente, le prédicat lui-même suggère que Paires = ∅. De façon générale, on énonce
l’axiome du point par le prédicat suivant.
Théorème 9.2.1 (Axiome du point)

∃ x : E • (p ∧ x = t) ⇔ t ∈ E ∧ p[x := t]

pourvu que x ne soit pas libre dans t.

Remarques
— On doit s’assurer d’une application correcte de la loi de substitution dans p[x := t].
Cette loi (de substitution) ne peut être appliquée que si aucune variable libre de t ne
devient liée dans p[x := t]. Dans les acétates, il y a un exemple où cette condition
n’est pas vérifiée, ce qui nous oblige à renommer la variable y.

78
 — Par contre, si la condition pourvu que x ne soit pas libre dans t n’est pas vérifiée, on
ne peut rien faire pour arranger la situation. Imaginez un exemple où on a

∃x : N • x = x ∗ x
Dans cette situation, t est x ∗ x et la variable x n’y est pas libre. On ne peut pas
renommer pour arranger les choses. Ici l’axiome du point ne s’applique pas. ‚a ne veut
pas dire que l’expression est vraie ou est fausse. Dans ce cas-ci elle est vraie mais si
on avait eu x = x + 1, elle aurait été fausse.

Regardons un autre exemple de théorème d’initialisation, le théorème InitialisationBi -

bliotheque qui s’énonce comme suit.

∃ Bibliotheque • BibliothequeInit

Voyons comment nous le démontrons

∃ Bibliotheque • BibliothequeInit
⇔ hDéfinition de BibliothequeInit i
∃ Bibliotheque•

BibliothequeInit
Bibliotheque
disponible = dom stock
emprunt = {}
membre = {}

⇔ hLogique : distributivité de ∧ sur ∃ i

∃ Bibliotheque
• (disponible = dom stock ∧ emprunt = {} ∧ membre = {})
⇔ hDéfinition de Bibliotheque i
∃ [ stock : COTE → 7 7 LIVRE
emprunt : COTE → 7 7 LECTEUR
disponible : F COTE
membre : F LECTEUR
| disponible ∪ dom emprunt = dom stock
∧ disponible ∩ dom emprunt = {}
∧ ran emprunt ⊆ membre
∧ ∀ m : membre • #(emprunt B {m}) ≤ nb pret max ]
• (disponible = dom stock ∧ emprunt = {} ∧ membre = {})
⇔ hLogique : transfert i

79
 ∃ stock : COTE → 7 7 LIVRE
emprunt : COTE → 7 7 LECTEUR
disponible : F COTE
membre : F LECTEUR
• disponible ∪ dom emprunt = dom stock
∧ disponible ∩ dom emprunt = {}
∧ ran emprunt ⊆ membre
∧ ∀ m : membre • #(emprunt B {m}) ≤ nb pret max
∧ disponible = dom stock
∧ emprunt = {}
∧ membre = {}
⇔ hAxiome du point i
∃ stock : COTE → 7 7 LIVRE
• {} : COTE → 7 7 LECTEUR
∧ dom stock : F COTE
∧ {} : F LECTEUR
∧ dom stock ∪ dom{} = dom stock
∧ dom stock ∩ dom{} = {}
∧ ran{} ⊆ {}
∧ ∀ m : {} • #({} B {m}) ≤ nb pret max
⇔ hLogique et théorie des ensembles i
∃ stock : COTE → 7 7 LIVRE
• true
∧ dom stock : F COTE
∧ true
∧ dom stock = dom stock
∧ true
∧ true
∧ true
⇔ hLogique i
∃ stock : COTE →
7 7 LIVRE • dom stock : F COTE

⇔ hPosons stock = {} i
true

On peut résumer cette section de la façon suivante. Chaque fois que l’on crée une spéci-
fication formelle, il faut spécifier l’état initial du système. Comme nous l’avons mentionné
souvent maintenant, il est possible que cette description de l’état initial soit partielle. Qu’à
cela ne tienne, nous devons démontrer qu’il existe un état du système qui satisfait cet état
initial. Sans quoi, dès le départ, le système est dans un état indésirable ! C’est le théorème
d’initialisation.

80
9.3 Théorème des préconditions

Maintenant que nous savons que le système démarre dans un état valide, il nous reste
à vérifier si les fonctions spécifiées n’envoient pas le système dans des états indésirables.
Nous voulons donc vérifier qu’à partir d’un état valide, si les préconditions d’une fonction
sont satisfaites, alors cette fonction envoie toujours le système dans un état valide. On peut
exprimer le tout à l’aide du prédicat suivant.

∀ Systeme ;Entrees | Proprietes • (∃ Systeme 0 ;sorties! • Fonction)

Dans la dernière partie de ce prédicat se cachent les préconditions de la fonction. Aussi

va-t-on utiliser le raccourci suivant pour noter ce prédicat.

pre Fonction ⇔ ∃ Systeme 0 ;sorties! • Fonction

On peut donc résumer le théorème à démontrer à l’aide du prédicat suivant.

∀ Systeme ;Entrees | Proprietes • pre Fonction

Prenez le temps de comprendre la différence entre les 2 expressions ! ! !

Prenez le temps de connaître leurs noms ! ! !

Pour bien voir que les préconditions d’une fonction se cachent derrière pre Fonction,
commençons par simplifier ce prédicat. D’abord, essayons de voir ce qu’il signifie. Il fait ré-
férence aux préconditions d’une Fonction qui agit sur un Systeme et qui retourne des sorties!.

Par exemple, prenons la fonction AjouterPaire du dictionnaire.

AjouterPaire
∆Dictionnaire
m? : MATERNELLE
e? : ETRANGERE
(m?, e?) ∈ PAIRES CORRECTES
Paires 0 = Paires ∪ {(m?, e?)}

On a alors

pre AjouterPaire
⇔ hDéfinition de pre et de AjouterPaire i

81
 ∃ Dictionnaire 0 •

AjouterPaire
∆Dictionnaire
m? : MATERNELLE
e? : ETRANGERE
(m?, e?) ∈ PAIRES CORRECTES
Paires 0 = Paires ∪ {(m?, e?)}
⇔ hLogique : distributivité de ∧ sur ∃ i

PreAjouterPaire
Dictionnaire
m? : MATERNELLE
e? : ETRANGERE
(m?, e?) ∈ PAIRES CORRECTES
∃ Dictionnaire 0
• Paires 0 = Paires ∪ {(m?, e?)}
⇔ hDéfinition de Dictionnaire 0 i

PreAjouterPaire
Dictionnaire
m? : MATERNELLE
e? : ETRANGERE
(m?, e?) ∈ PAIRES CORRECTES
∃[Paires 0 : F(MATERNELLE × ENTRANGERE )
| Paires 0 ⊆ PAIRES CORRECTES ]
• Paires 0 = Paires ∪ {(m?, e?)}
⇔ hLogique : transfert i

PreAjouterPaire
Dictionnaire
m? : MATERNELLE
e? : ETRANGERE
(m?, e?) ∈ PAIRES CORRECTES
∃ Paires 0 : F(MATERNELLE × ENTRANGERE )
• Paires 0 ⊆ PAIRES CORRECTES
Paires 0 = Paires ∪ {(m?, e?)}
⇔ hAxiome du point i

82
 PreAjouterPaire
Dictionnaire
m? : MATERNELLE
e? : ETRANGERE
(m?, e?) ∈ PAIRES CORRECTES
Paires ∪ {(m?, e?)} ∈ F(MATERNELLE × ENTRANGERE )
Paires ∪ {(m?, e?)} ⊆ PAIRES CORRECTES ]
⇔ hExpansion de Dictionnaire i

PreAjouterPaire
Paires : F(MATERNELLE × ENTRANGERE )
m? : MATERNELLE
e? : ETRANGERE
Paires ⊆ PAIRES CORRECTES
(m?, e?) ∈ PAIRES CORRECTES
Paires ∪ {(m?, e?)} ∈ F(MATERNELLE × ENTRANGERE )
Paires ∪ {(m?, e?)} ⊆ PAIRES CORRECTES ]
⇔ hLogique, théorie des ensembles : car Paires ∈ F(MATERNELLE ×
ENTRANGERE ), m? ∈ MATERNELLE et e? ∈ ENTRANGERE i

PreAjouterPaire
Paires : P(MATERNELLE × ENTRANGERE )
m? : MATERNELLE
e? : ETRANGERE
Paires ⊆ PAIRES CORRECTES
(m?, e?) ∈ PAIRES CORRECTES
true ∧ Paires ∪ {(m?, e?)} ⊆ PAIRES CORRECTES ]
⇔ hLogique, théorie des ensembles et définition de PAI RES CORREC TES
i

PreAjouterPaire
Paires : F(MATERNELLE × ENTRANGERE )
m? : MATERNELLE
e? : ETRANGERE
Paires ⊆ PAIRES CORRECTES
(m?, e?) ∈ PAIRES CORRECTES ∧ true
⇔ hDéfinition de Dictionnaire i

83
 PreAjouterPaire
Dictionnaire
m? : MATERNELLE
e? : ETRANGERE
(m?, e?) ∈ PAIRES CORRECTES

C’est donc beaucoup de travail pour calculer les préconditions de la fonction AjouterPaire
Valide. Nous apprenons alors que cette fonction attend un état qui satisfait Dictionnaire,
qu’elle prend m? ∈ MATERNELLE et e? ∈ ENTRANGERE en entrées et que la propriété
(m?, e?) ∈ PAIRES CORRECTES doit être satisfaite avant l’application de l’opération,
pour que l’état d’arrivée soit correct (respecte les invariants de l’état général).

Ce prédicat pre Fonction sert donc à calculer les préconditions d’une Fonction. Dans
les exemples que nous avons vus, ces préconditions sont toujours très faciles à déduire des
schémas. Ce prédicat est donc plutôt inutile dans ces situations. Par contre, il peut être utile
lorsque les préconditions d’une fonction ne nous semblent pas claires à la lecture d’un schéma.
Il est aussi utile à l’intérieur du théorème suivant (encore une fois : notez la différence entre
le calcul des préconditions et le théorème des préconditions).

On peut maintenant revenir au théorème principal de cette section, le théorème des

préconditions (rappelez-vous le nom et sa différence avec le calcul des préconditions)
qui nous assure qu’une fonction n’a pas de comportement indésirable. De façon générale,
supposons qu’une Fonction avec Entrees agisse sur un Systeme et que certaines Proprietes
doivent être satisfaites pour qu’elle s’exécute correctement. Rappelons le théorème qui a été
présenté au début de cette section.

∀ Systeme ;Entrees | Proprietes • pre Fonction

Nous l’appellerons le théorème PreconditionsFonction et nous devrons le démontrer.

Prenons encore l’exemple de la fonction AjouterPaire. Le théorème que nous appelerons

PreconditionsAjouterPaire s’énonce comme suit

∀ Dictionnaire ; m? : MATERNELLE ;e? : ENTRANGERE

| (m?, e?) ∈ PAIRES CORRECTES
• pre AjouterPaire

autrement dit

∀ Dictionnaire ; m? : MATERNELLE ;e? : ENTRANGERE

| (m?, e?) ∈ PAIRES CORRECTES
• ∃ Dictionnaire 0 • AjouterPaire

84
ce qui représente très bien la propriété que nous souhaitons démontrer (Pour tout Diction-
naire de départ, il existe un Dictionnaire d’arrivée qui respecte les (pré- et post-) conditions
de AjouterPaire). D’ailleurs, on peut le faire assez simplement dans ce cas-ci.

∀ Dictionnaire ;m? : MATERNELLE ;e? : ENTRANGERE

| (m?, e?) ∈ PAIRES CORRECTES
•pre AjouterPaire
⇔ hVoir démonstration précédente i
∀ Dictionnaire ;m? : MATERNELLE ;e? : ENTRANGERE
| (m?, e?) ∈ PAIRES CORRECTES •

PreAjouterPaire
Dictionnaire
m? : MATERNELLE
e? : ETRANGERE
(m?, e?) ∈ PAIRES CORRECTES
⇔ hLogique i
true

Ce théorème de préconditions, une fois démontré, nous assure qu’une fonction n’a pas de
comportement indésirable. Il faut le démontrer pour chacune des fonctions.

9.4 Conclusion

Pourquoi ces théorèmes sont-ils si importants ? Supposons que l’on code un programme
qui respecte parfaitement sa spécification en Z et que nous avons réussi à démontrer tous
ces théorèmes. On peut alors être assuré que le programme ne sera jamais dans un état
indésirable... ou presque. On peut énoncer ce fait dans le théorème suivant.

Théorème 9.4.1 Considérons une spécification en Z d’un système S , avec état initial SInit,
avec les déclarations d1 , d2 , ..., dm et avec les fonctions f1 , f2 , ..., fn . Supposons que l’ensemble
des états possibles du système ne soit pas vide. Soit P , un programme codé de telle sorte qu’il
satisfasse l’ensemble de cette spécification. Supposons de plus que les théorèmes suivants ont
été démontrés.

d1 $domainCheck
d2 $domainCheck
..
.
dm $domainCheck

85
 S $domainCheck
SInit$domainCheck
f1 $domainCheck
f2 $domainCheck
..
.
fn $domainCheck
InitialisationS
Preconditionsf1
Preconditionsf2
..
.
Preconditionsfn
Alors le programme P ne se trouvera jamais dans un état indésirable.
Nous allons démontrer ce théorème et par la suite nous expliquerons pourquoi le résultat est
extraordinaire en théorie, mais qu’en pratique... les choses sont différentes.

Preuve: Les théorèmes d1 $domainCheck , d2 $domainCheck , ..., dm $domainCheck nous as-

surent que la spécification a un sens. Nous allons montrer par induction mathématique
que le programme ne se trouve jamais dans un état indésirable. D’abord, à l’état initial,
le programme est dans un état valide puisque InitialisationS a été démontré. Plaçons-nous
maintenant dans un état valide du système. Peut-on démontrer que le système sera dans un
état valide après l’utilisation de n’importe quelle fonction ? On peut montrer assez simple-
ment que c’est le cas. En effet, si la fonction fi (1 ≤ i ≤ n) est utilisée, alors le système se
retrouve dans un état valide puisque le théorème Preconditionsfi a été démontré. 2

Ce théorème résume bien la façon de penser en Z. Dans un monde parfait, si l’on suit la
démarche proposée (c’est-à-dire la spécification formelle de tout le système, la déclaration
d’un état initial, la définition de fonctions totales, la démonstration des différents théorèmes,
etc.), on obtient toujours un programme parfait ! Malheureusement, le monde est rempli
d’obstacles...

Quelle est l’hypothèse de ce théorème qui flanche en pratique ? C’est l’hypothèse Soit P ,
un programme codé de telle sorte qu’il satisfasse l’ensemble de cette spécification. D’abord,
il faut savoir que dans plusieurs cas, la spécification en Z ne peut même pas être traduite en
un programme de façon exacte. Pensons à une spécification utilisant des nombres réels. On
peut imaginer que le type [REEL] serait défini. Quand viendra le temps de programmer, il
faudra faire des choix quant à la précision de ces nombres “réels”.

De plus, nous avons mentionné à plusieurs reprises qu’une spécification laisse souvent au
programmeur des décisions à prendre. Ces décisions, sans nécessairement contredire la spé-
cification, peuvent impliquer la manipulation d’éléments qui n’apparaissaient pas au départ

86
dans la spécification. Si tel est le cas, aucun théorème ne sera démontré sur ces nouveaux
éléments et l’assurance d’un programme parfait disparaît.

Mentionnons un dernier point concernant cette hypothèse. On pourrait imaginer une si-
tuation où les hypothèses du théorème sont parfaitement satisfaites, mais où le prix à payer
est élevé. Imaginez une situation où l’on doive rendre le programme extrêmement lent 1 .
Qu’allez-vous choisir ? L’assurance d’un programme fiable à 100% qui ne termine jamais ou
un programme qui termine, mais qui n’est fiable qu’à 99% ?

Finalement, même en supposant qu’il soit possible de coder de façon exacte un programme
qui représente la spécification en question et que cette spécification représente parfaitement
les besoins du client et que ce programme s’exécute en un temps raisonnable, les erreurs ou
bogues peuvent provenir de bien d’autres sources : virus, système d’exploitation, variation
de courant (pourquoi pas !), etc...

1. Un temps exponentiel pour ceux qui ont fait analyse d’algorithmes IFT-3001.

87
Chapitre 10

Vérification avec Perfect Developer

Ce chapitre constitue un outil de travail pour vérifier nos spécifications à l’aide de Perfect
Developer (PD en abrégé). Dans la première section, une vue générale de la vérification selon
PD est expliquée, dans la deuxième, on verra deux exemples de preuves non démontrées et
comment les compléter pour prouver que notre spécification est bien valide alors que dans
la dernière section, on trouvera une liste des principaux messages que PD lance lorsqu’il ne
peut démontrer une obligation de preuve.
En PD, il y a deux niveaux de vérification, un qui n’est que syntaxique (la commande
Check) et l’autre qui crée des obligations de preuves et tente de les vérifier (la commande
Verify). C’est la seconde qui est la plus substantielle et dont il est question dans ce document.

10.1 Obligations de preuves

Au chapitre 9, on a discuté de 3 sortes de vérifications : la vérification de domaine,
le théorème de l’état initial et le théorème des préconditions. Avec l’outil Z/Eves dont il
est question dans ce chapitre, seule la première est générée automatiquement (c’est une
obligation de preuve qui est syntaxiquement triviale à générer) : les autres doivent être
définies à la main. En PD ces vérifications sont générés automatiquement, mais pas sous le
même format.

Vérification de domaine en Z Si quelque part dans la spécification il est écrit f (a), alors
il faut vérifier que a ∈ dom(f ) ; c’est aussi le cas en PD : s’il est écrit f[a], il faut vérifier que
a in [Link]. C’est une précondition de []. Il y a beaucoup de fonctions que l’on peut utiliser
en Perfect qui génèrent de telles obligations de preuves. On pense à f!= [Link](a->e)
si f est déclaré comme map of (X,Y) : en effet, append a comme précondition que si a est
dans le domaine de f alors l’image de a par f doit être égale à e, sinon la nouvelle valeur de
f ne serait plus une fonction. Il faut être attentif aux préconditions des opérateurs que l’on
utilise.
Conclusion, la vérification de domaine mentionnée au chapitre 9 n’est qu’une précondition
de l’opérateur [] au même titre que la précondition de append pour une fonction. On pour-
rait penser qu’il y a beaucoup trop d’emphase dans les notes sur la vérification de domaine,

88
mais c’est ainsi parce que c’est la seule qui est générée automatiquement avec l’outil Z/Eves
et parce que les autres préconditions (telles que rencontrées en PD) se retrouvent dans les
invariants de l’état général en Z. En effet, reprenons l’exemple ci-haut, f 0 = f ∪ {a 7→ e}.
Puisque f 0 sera déclarée comme une fonction, la contrainte d’une fonction sera automati-
quement énoncée quand on écrira le théorème des préconditions : elle sera cachée dans le
fragment ∃ f 0 : X →7 Y • . . . f 0 = f ∪ {a 7→ e}.

Théorème de l’état initial et théorème des préconditions En Z, nous séparons ces

deux théorèmes parce que cela nous permet de bien voir comment la vérification du premier
et ensuite du deuxième pour chacune des opérations nous permet de toujours disposer d’un
état général valide. Comment PD atteint-il cet objectif sans que l’on voit explicitement les
énoncés de ces théorèmes ? Pour chaque schéma, PD crée une obligation de preuve pour
chaque invariant. Avec PD, ces deux vérifications sont regroupées puisque dans les deux
cas il s’agit de vérifier que les invariants du systèmes sont valides dans l’état d’arrivée du
constructeur/de l’opération. Dans le premier cas, nous n’avons pas à supposer que l’état de
départ satisfaisait les invariants, dans l’autre on le fait.

En résumé, PD génère une obligation de preuve qu’il essaie ensuite de démontrer pour tous
les cas suivants.
— Une obligation pour chaque utilsation d’une opération (au sens large) qui a une pré-
condition : il vérifie donc que l’appel est légal.
— Pour chaque schéma et pour chaque invariant il génère une obligation de preuve que
l’invariant est vrai à l’état d’arrivée du schéma étant donné que tous les invariants
étaient vrais à l’état de départ.

10.2 Exemples de preuves non réalisées par Perfect De-

veloper
Nous 1 donnons deux exemples de preuves d’énoncés qui sont vrais mais que Perfect
Developer n’arrive pas à démontrer. Le premier exemple représente la deuxième situation la
plus fréquente que vous allez rencontrer : la preuve devrait être possible avec les éléments
que nous avons, mais le démonstrateur automatique de Perfect Developer ne la trouve pas.
(La situation la plus fréquente ? c’est celle où vous avez une faute dans la spécification ! ! !)
Le deuxième exemple est beaucoup plus rare. Il s’agit d’une situation où vous devez utiliser
une sorte de preuve par induction et la sémantique du langage pour bien réaliser la preuve.

10.3 Exemple 1 : une preuve de la banque d’articles

Nous réalisons la preuve d’une des conditions de vérification non démontrées par Perfect
Developer pour la banque d’articles (un des travaux dirigés que nous avons effectués). Pour le
1. Écrit avec la collaboration de Claude Bolduc.

89
schéma choisir, le démonstrateur n’arrive pas à démontrer l’invariant que la liste de choix
est injective. La première étape est bien sûr d’écrire ce qu’il faut montrer :

∀ p :: listeChoix 0 .pairs : − ∀ q :: listeChoix 0 .pairs : −p.x 6= q.x =⇒ p.y 6= q.y

Nous pouvons considérer que les propriétés suivantes sont vraies (tolérons un mélange de
notation Z et Perfect pourvu que ce soit clair et le plus concis possible, ici une fonction est
un ensemble de paires) :
D’abord les invariants :
(i) prof 6∈ inscrits
(ii) listeChoix .dom ⊆ inscrits
(iii) ∀ p : listeChoix • ∀ q : listeChoix : −p.x 6= q.x =⇒ p.y 6= q.y
(iv) [Link] = banque
(v) listeChoix .ran = {p : annotations | p.y = choisi • p.x } ;
ensuite les préconditions de choisir :
(vi) u ∈ inscrits ∨ u = prof
(vii) e ∈ inscrits
(viii) a ∈ banque
(ix) annotations[a] = nonchoisi ;
finalement la postcondition de choisir qui nous intéresse
(x) listeChoix 0 = listeChoix ∪ {e 7→ a}.
Nous les rappelons ici par souci de complétude, mais seules les propriétés (iii), (v), (ix) et
(x) sont nécessaires. Voici une démonstration disons... semi-formelle. Il est primordial que
vos preuves soient claires et concises. Coupez, coupez, polissez.
Nous voulons donc démontrer ceci :

∀ p :: listeChoix 0 • ∀ q : listeChoix 0 : −p.x 6= q.x =⇒ p.y 6= q.y

⇔ (x) Remplaçons listeChoix 0 par sa valeur, listeChoix ∪ {e 7→ a} :

∀ p :: listeChoix ∪ {e 7→ a} • ∀ q :: listeChoix ∪ {e 7→ a} : −p.x 6= q.x =⇒ p.y 6= q.y

⇔ Utilisons la contraposée pour mieux raisonner sur l’implication :

∀ p : listeChoix ∪ {e 7→ a} • ∀ q :: listeChoix ∪ {e 7→ a} : −p.y = q.y =⇒ p.x = q.x

⇔ (iii) implique qu’il ne reste à montrer l’implication que pour p ou q égal à la paire (e, a).
Comme l’énoncé est symétrique, prenons q = (e, a) et montrons donc

∀ p :: listeChoix • p.y = a =⇒ p.x = e

⇔ (v) et (ix) impliquent que a n’est pas dans l’image de listeChoix : il n’existe donc aucun
p tel que p.y = a. L’implication est donc toujours vraie (faux ⇒ vrai est toujours vrai).

VRAI .

90
10.4 Exemple 2 : une preuve du jeu de chiffres
Nous réalisons la preuve de la condition de vérification non démontrée par Perfect Develo-
per pour le jeu de chiffres (un des travaux dirigés que nous avons effectués). Celle-ci est très
simple : pour le schéma remettreEtatInitial, le démonstrateur n’arrive pas à démontrer
que l’invariant :
#nombres’ <= 6
est vrai à la fin de l’exécution du schéma.
Sans surprise, en lisant le fichier [Link], nous remarquons qu’en fait le démons-
trateur n’arrive pas à démontrer que : #nombresInitiaux <= 6 lors de l’appel du schéma
remettreEtatInitial. Cependant, en analysant rapidement le code Perfect développé, nous
remarquons que ceci est vrai en tout temps. Le problème vient donc d’une limitation de
Perfect Developer et non d’une erreur de notre part. Voici une manière de démontrer que
#nombresInitiaux <= 6 est toujours vrai dans tout état possible d’un objet JeuChiffres.
C’est un peu le principe d’induction. Nous le démontrons pour l’état initial et nous démon-
trons ensuite que s’il était vrai avant une opération il est encore vrai après l’opération.
Tout d’abord, dans l’état initial (lors de l’appel du constructeur de la classe), la variable
nombresInitiaux prend la même valeur que nombres et celui-ci respecte #nombres <= 6 par
la précondition. Donc,
nous avons bien #nombresInitiaux <= 6 à l’état initial.
Ensuite, les autres états d’un objet de cette classe ne peut être générés qu’en appelant un
schéma de la classe JeuChiffres. Nous remarquons rapidement qu’aucun schéma (excepté le
constructeur) ne permet de modifier la variable nombresInitiaux. Comme un schéma modifie
une variable seulement si cette
#nombresInitiaux n’est jamais modifiée, donc est toujours <= 6.
C’est donc vrai aussi avant l’appel du schéma remettreEtatInitial. Donc lors de l’ap-
pel, nous obtenons
#nombres’ = nombresInitiaux <= 6
ce qui implique, comme voulu, que #nombres’ <= 6 
Remarquons que notre preuve est valide en autant que nous n’ajoutions pas de schéma à
la classe JeuChiffres. En effet, un nouveau schéma pourrait modifier la valeur de la variable
nombresInitiaux et faire en sorte que celle-ci ne respecte plus la contrainte
#nombresInitiaux <= 6 .
Cependant, nous jouerions au chat et à la souris avec Perfect Developer puisqu’il nous avertira
qu’il se peut que le schéma remettreEtatInitial ne respecte pas les invariants.
Discutons ici d’un point particulier : notre spécification est incomplète. En effet, il y a une
partie non spécifiée (via « ? ») qui est l’implémentation de la fonction resultatsPossibles.

91
Cette partie pourrait faire « échouer » notre preuve si cette fonction modifiait la valeur
de nombresInitiaux. Cependant, il faut comprendre que ceci n’arrivera jamais dans notre
spécification. En effet, les fonctions dans le langage Perfect ont une sémantique pure. En
particulier, une fonction ne peut avoir d’effet de bords (comme modifier la valeur d’une
variable de la classe). Donc, malgré que la fonction resultatsPossibles est non spécifiée,
la preuve est valide tout de même.

10.5 Messages de PD
La structure de cette section suit celle de la section 3 du document Verification Condi-
tions Generated by Perfect Developer 2 . Comme celle-ci, les titres de sous-sections sont les
messages que PD retourne lorsqu’il ne peut démontrer un énoncé. Seuls les plus fréquents
sont commentés ici (vous pouvez me pointer des messages que vous avez obtenus qui ne sont
pas énumérés).

3.1 All qualifying elements in operand of ’that’ are equal Puisque that a comme
précondition que l’élément qui satisfait l’expression doit être unique, PD essaie de démontrer
que tous ceux qui satisfont l’expression sont égaux. L’expression that a::nat :- a<4 n’est
pas définie parce qu’il y a plus d’un naturel qui satisfait a<4.

3.3 Assertion valid Pour chaque assert que vous déclarez, une obligation de preuve est
générée.

3.4 At least one guard is true Quand on utilise le choix conditionel sans utiliser de
else (qui apparaît sous la forme []: instruction), une obligation de preuve est créée pour
démontrer qu’au moins une des gardes est vraie.

3.6 Class invariant satisfied Après chaque schéma et constructeur qui modifie l’état,
les invariants de la classe doivent être vérifiés. Cette obligation est aussi générée quand on
utilise self after....

3.23 Objects modified in parallel are independent Quand plus d’une variable est
modifiée en une expression dans une postcondition, par exemple lorsque les postconditions
sont combinées avec des virgules, & et avec l’utilisation de forall. En modifiant l’état dans
un schéma, on ne peut faire dépendre la nouvelle valeur d’une variable de la nouvelle valeur
d’une autre. Quand on utilise forall avec bag ou seq, cela vérifie aussi que la collection est
unique : cela signifie qu’il vérifie qu’il n’y a pas de répétition dans le bag ou la seq.
2. [Link]/product_documentation/Verification%20Conditions%20Generated%20by%
20Perfect%[Link]

92
3.25 Operand of [that | any] has at least one qualifying element Obligation générée
à chaque expression any et à chaque expression that. Si un prédicat est associé à un that ou
un any, alors l’obligation de preuve est qu’il existe un élément de la collection qui satisfait
le prédicat. S’il n’y a pas de prédicat d’associé au that ou any, alors l’obligation de preuve
est simplement que la collection n’est pas vide.

3.27 Operand of ’over’ has at least one element La collection sur laquelle on applique
over doit être non-vide.

3.38 Post-assertion valid Pour chaque assertion que l’on déclare dans une post condition,
une obligation de preuve est créée.

3.39 Postcondition specifies value for uninitialised data Dans un schéma ou construc-
teur qui contient des paramètres qui sont marqués out, une obligation de preuve est générée
pour vérifier que chaque donnée non initialisée reçoit une valeur avant d’être utilisée.

3.41 Precondition of ... satisfied Au moment de l’appel d’une fonction, opérateur,

sélecteur, constructeur ou schéma avec une précondition.

3.43 Property satisfied Une obligation de preuve pour chaque propriété créée.

93
Chapitre 11

Exemple de l’éditeur

Dans ce document, nous présentons deux solutions possibles de la spécification d’un

éditeur dont la description est la suivante :

Vous devez spécifier un éditeur de texte. Bien sûr, il s’agira d’une version simplifiée.
Pensez à un bloc-notes que l’on spécifie partiellement.
— Les touches du clavier permettent différentes commandes. On se concentre seulement
sur quelques-unes d’entre elles. D’abord, il y a les caractères qui correspondent à ce
qui peut être affiché à l’écran. On peut penser aux lettres, à la barre d’espace, au
point, etc. Parmi les autres touches, on retrouve la touche suppr (del), la touche
fleche gauche qui permet de déplacer le curseur à gauche et la touche fleche droite
qui permet de déplacer le curseur à droite et la touche inser .
— L’éditeur a deux mode ecriture. Le mode Ecrit qui permet d’écrire normalement et
le mode Ecrase qui supprime le caractère à la droite du curseur et le remplace par le
caractère entré par l’utilisateur.
— Quel que soit le texte écrit par l’utilisateur, il ne doit jamais contenir plus de taille max
caractères. On va convenir que taille max est un entier qui n’excède pas 65535.
— Il doit y avoir une fonction qui permet d’insérer un caractère entré par l’utilisateur là
où le curseur se trouve (attention aux mode ecriture !).
— Il doit y avoir une fonction qui permet d’avancer le curseur lorsque l’utilisateur appuie
sur fleche droite.
— Il doit y avoir une fonction qui permet de reculer le curseur lorsque l’utilisateur appuie
sur fleche gauche.
— Il doit y avoir une fonction qui permet de supprimer le caractère à droite du curseur
lorsque l’utilisateur appuie sur suppr .
— Il doit y avoir une fonction qui permet de changer le mode ecriture de l’éditeur.
— Pour chacune de ces fonctions, vous devez gérer tous les cas d’erreurs possibles.
— Vous devez spécifier un état initial.
— On ne spécifie rien d’autre. Plusieurs autres touches du clavier ont des propriétés qui
seraient pertinentes à spécifier, mais nous nous limitons à celles mentionnées ici. On
ne spécifie pas non plus l’environnement graphique de cet éditeur.

94
11.1 Première solution
Nous présentons la première solution tout d’un bloc puis les remarques suivront.
[TOUCHE ]

CARACTERE : F TOUCHE

suppr , fleche gauche, fleche droite, inser : TOUCHE

suppr 6∈ CARACTERE
fleche gauche 6∈ CARACTERE
fleche droite 6∈ CARACTERE
inser 6∈ CARACTERE
suppr 6= fleche gauche
suppr 6= fleche droite
suppr 6= inser
fleche gauche 6= fleche droite
fleche gauche 6= inser
fleche droite 6= inser

MODE ::= Ecrit | Ecrase

MESSAGE ::= TexteTropLong

taille max : N
taille max ≤ 65535

Editeur
texte : seq CARACTERE
curseur : N
mode ecriture : MODE
#texte ≤ taille max
curseur ≤ #texte

EditeurInit
Editeur
texte = hi
mode ecriture = Ecrit
curseur = 0

95
InsererModeEcrit
∆Editeur
c? : TOUCHE
c? ∈ CARACTERE
mode ecriture = Ecrit
#texte < taille max
texte 0 = (1..curseur ) C texte a hc?i
a {n : N ;car : CARACTERE | n > 0 ∧ (n + curseur , car ) ∈ texte}
0
curseur = curseur + 1
mode ecriture 0 = mode ecriture

InsererFinModeEcrase
∆Editeur
c? : TOUCHE
c? ∈ CARACTERE
mode ecriture = Ecrase
curseur = #texte
#texte < taille max
texte 0 = texte a hc?i
curseur 0 = curseur + 1
mode ecriture 0 = mode ecriture

InsererMilieuModeEcrase
∆Editeur
c? : TOUCHE
c? ∈ CARACTERE
mode ecriture = Ecrase
curseur < #texte
#texte ≤ taille max
texte 0 = (1..curseur ) C texte a hc?i
a {n : N ;car : CARACTERE | n > 0 ∧ (n + curseur + 1, car ) ∈ texte}
curseur 0 = curseur + 1
mode ecriture 0 = mode ecriture

96
 InsererErreur
ΞEditeur
c? : TOUCHE
rep! : MESSAGE
c? ∈ CARACTERE
(mode ecriture = Ecrit ∧ #texte = taille max )
∨ (mode ecriture = Ecrase ∧ curseur = #texte ∧ #texte = taille max )
rep! = TexteTropLong

InsererTotale =
b InsererModeEcrit
∨ InsererFinModeEcrase
∨ InsererMilieuModeEcrase
∨ InsererErreur

AvancerCurseur
∆Editeur
t? : TOUCHE
t? = fleche droite
curseur < #texte
texte 0 = texte
curseur 0 = curseur + 1
mode ecriture 0 = mode ecriture

AvancerCurseurFin
ΞEditeur
t? : TOUCHE
t? = fleche droite
curseur = #texte

AvancerCurseurTotale =
b AvancerCurseur
∨ AvancerCurseurFin

ReculerCurseur
∆Editeur
t? : TOUCHE
t? = fleche gauche
curseur > 0
texte 0 = texte
curseur 0 = curseur − 1
mode ecriture 0 = mode ecriture

97
 ReculerCurseurDebut
ΞEditeur
t? : TOUCHE
t? = fleche gauche
curseur = 0

ReculerCurseurTotale =
b ReculerCurseur
∨ ReculerCurseurDebut

Supprimer
∆Editeur
t? : TOUCHE
t? = suppr
curseur < #texte
texte 0 = (1..curseur ) C texte
a {n : N ;car : CARACTERE | n > 0 ∧ (n + curseur + 1, car ) ∈ texte}
curseur 0 = curseur
mode ecriture 0 = mode ecriture

SupprimerFin
ΞEditeur
t? : TOUCHE
t? = suppr
curseur = #texte

SupprimerTotale =
b Supprimer
∨ SupprimerFin

ChangerModeEcriture
∆Editeur
t? : TOUCHE
t? = inser
texte 0 = texte
curseur 0 = curseur
mode ecriture 0 6= mode ecriture

98
11.1.1 Commentaires

Cette solution est la première à laquelle on pense en lisant la description de l’éditeur. Il

y a différent commentaires à faire.
1. Les touches suppr , fleche gauche, fleche droite, inser ne sont pas des caractères.
2. Il y a un seul message d’erreur possible, soit TexteTropLong.
3. À propos du curseur, si ce dernier vaut n, c’est qu’il y a n caractères à sa gauche
et #texte − n caractères à sa droite. Le curseur ne peut pas aller plus loin que la
longueur du texte. En effet, la barre d’espace est considérée comme un caractère qui
peut être affiché.
4. À propos de l’état initial, nous aurions tout aussi bien pu ne rien écrire pour mo-
de ecriture. En effet, rien dans la description ne mentionne que l’éditeur doit démarrer
dans un mode ou dans un autre. De plus, le fait de laisser le choix au programmeur ne
causerait aucune erreur. C’est-à-dire que cela ne contribuerait pas à mettre l’éditeur
dans un état indésirable.
5. Voici maintenant un commentaire sur la fonction InsererModeEcrit. Pourquoi ne pas
avoir écrit le code suivant ?

texte 0 = (1..curseur ) C texte a hc?i a (curseur + 1..#texte) C texte

Ne serait-ce pas plus simple ?

Ce serait bien plus simple, mais malheureusement il y a erreur sur le domaine d’uti-
lisation de l’opérateur a. D’abord, rappelez-vous que l’opérateur a s’applique uni-
quement à des suites et que le résultat est une suite. Ensuite, pensez que l’opéra-
teur C s’applique à tout ensemble de couples. Le problème est que le résultat de
(curseur + 1..#texte) C texte n’est pas une suite de façon générale.

En effet, voici un exemple. Prenons texte = hB , o, j , o, u, r i et curseur = 2. En

appelant la fonction InsererModeEcrit avec c? = n, on obtiendrait ce qui suit. D’abord

(1..curseur ) C texte = (1..2) C hB , o, j , o, u, r i

= (1..2) C {(1, B ), (2, o), (3, j ), (4, o), (5, u), (6, r )}
= {(1, B ), (2, o)}
= hB , oi

qui est une suite. Ensuite, hc?i est bien évidemment une suite. Finalement,

(curseur + 1..#texte) C texte = (3..6) C hB , o, j , o, u, r i

= (3..6) C {(1, B ), (2, o), (3, j ), (4, o), (5, u), (6, r )}
= {(3, j ), (4, o), (5, u), (6, r )}

99
 qui n’est pas une suite puisque le domaine n’est pas un intervalle qui commence à 1.
On ne peut donc pas appliquer l’opérateur de contaténation.

Pour quelle raison utilise-t-on le détour suggéré dans la solution ? Pour s’assurer que
l’opérateur a n’est utilisé que sur des suites.

Y a-t-il moyen de faire autrement ?

6. Oui, il y a moyen de faire autrement. Nous pourrions définir une fonction à l’extérieur
du schéma qui permet de faire ce travaille d’extraction d’une partie de la suite. Nous
pourrions ensuite appeler la fonction au besoin. Voici comment il faudrait faire.

Extract Fin Suite : seq CARACTERE × N →

→
7 seq CARACTERE
dom Extract Fin Suite = {s : seq CARACTERE ;n : N | n ≥ 1 ∧ n ≤ #s}
∀ s : seq CARACTERE • ∀ n : 1..#s
• Extract Fin Suite(s, n) = {i ;j : N | j − i = n − 1} o9 (n..#s) C s

Rappelez-vous que tout ce qui est défini à l’extérieur d’un schéma est fixe. Y a-t-il un
problème avec le fait que cette fois-ci, c’est une fonction ? Il n’y a pas de contradiction,
la fonction Extract Fin Suite est un objet mathématique qui n’est as constant, mais
vu comme élément de cette spécification, c’est un élément constant. C’est-à-dire que
son comportement sera toujours le même.

Puisque le schéma Editeur n’est mentionné nul part, il peut arriver n’importe quoi
au système durant l’utilisation de cette fonction. Ce n’est pas un problème : il ne
s’agit que d’une fonction que nous utilisons pour raccourcir le code. Ce n’est pas une
fonction qui intervient sur le système lui-même.
7. Plusieurs des fonctions définies peuvent sembler ne pas être totales. Par exemple, pre-
nez la fonction ChangerModeEcriture. Il y a une précondition dans cette fonction :
t? = inser . Pourquoi n’y a-t-il pas de fonction ChangerModeEcritureTotale où l’on
gère le cas t? 6= inser ? On pourrait penser qu’il s’agit d’une erreur ou d’un oubli,
mais il n’en est rien.

En fait, toutes ces fonctions qui ne semblent pas totales ont une variable d’entrée de
type TOUCHE . Elles se complètent donc l’une l’autre. L’idéal serait d’ajouter une
dernière fonction à cette spécification.

AppuyerToucheTotale =
b InsererTotale
∨ AvancerCurseurTotale
∨ ReculerCurseurTotale
∨ SupprimerTotale
∨ ChangerModeEcriture

100
11.2 Deuxième solution

[TOUCHE ]

CARACTERE : F TOUCHE

suppr , fleche gauche, fleche droite, inser : TOUCHE

suppr 6∈ CARACTERE
fleche gauche 6∈ CARACTERE
fleche droite 6∈ CARACTERE
inser 6∈ CARACTERE
suppr 6= fleche gauche
suppr 6= fleche droite
suppr 6= inser
fleche gauche 6= fleche droite
fleche gauche 6= inser
fleche droite 6= inser

TEXTE == seq CARACTERE

MODE ::= Ecrit | Ecrase

MESSAGE ::= TexteTropLong

taille max : N
taille max ≤ 65535

Editeur
gauche, droit : TEXTE
mode ecriture : MODE

#(gauche a droite) ≤ taille max

EditeurInit
Editeur
gauche = hi
droit = hi

101
InsererModeEcrit
∆Editeur
c? : TOUCHE
c? ∈ CARACTERE
mode ecriture = Ecrit
#(gauche a droite) < taille max
gauche 0 = gauche a hc?i
droit 0 = droit
mode ecriture 0 = mode ecriture

InsererFinModeEcrase
∆Editeur
c? : TOUCHE
c? ∈ CARACTERE
mode ecriture = Ecrase
#(gauche a droite) < taille max
droit = hi
gauche 0 = gauche a hc?i
droit 0 = droit
mode ecriture 0 = mode ecriture

InsererMilieuModeEcrase
∆Editeur
c? : TOUCHE
c? ∈ CARACTERE
mode ecriture = Ecrase
#(gauche a droite) ≤ taille max
droit 6= hi
gauche 0 = gauche a hc?i
droit 0 = tail droit
mode ecriture 0 = mode ecriture

102
 InsererErreur
ΞEditeur
c? : TOUCHE
rep! : MESSAGE
c? ∈ CARACTERE
(mode ecriture = Ecrit ∧ #(gauche a droit) = taille max )
∨ (mode ecriture = Ecrase ∧ droit = hi ∧ #(gauche a droit) = taille max )
rep! = TexteTropLong

InsererTotale =
b InsererModeEcrit
∨ InsererFinModeEcrase
∨ InsererMilieuModeEcrase
∨ InsererErreur

AvancerCurseur
∆Editeur
c? : TOUCHE
c? = fleche droite
droit 6= hi
gauche 0 = gauche a hhead droiti
droit 0 = tail droit
mode ecriture 0 = mode ecriture

AvancerCurseurFin
ΞEditeur
c? : TOUCHE
c? = fleche droite
droit = hi

AvancerCurseurTotale =
b AvancerCurseur
∨ AvancerCurseurFin

103
 ReculerCurseur
∆Editeur
c? : TOUCHE
c? = fleche gauche
gauche 6= hi
gauche 0 = front gauche
droit 0 = hlast gauchei a droit
mode ecriture 0 = mode ecriture

ReculerCurseurDebut
ΞEditeur
c? : TOUCHE
c? = fleche gauche
gauche = hi

ReculerCurseurTotale =
b ReculerCurseur
∨ ReculerCurseurDebut

Supprimer
∆Editeur
c? : TOUCHE
c? = suppr
droit 6= hi
gauche 0 = gauche
droit 0 = tail droit
mode ecriture 0 = mode ecriture

SupprimerFin
ΞEditeur
c? : TOUCHE
c? = suppr
droit = hi

SupprimerTotale =
b Supprimer
∨ SupprimerFin

104
 ChangerModeEcriture
∆Editeur
c? : TOUCHE
c? = inser
gauche 0 = gauche
droit 0 = droit
mode ecriture 0 6= mode ecriture

11.2.1 Commentaires

L’astuce derrière cette solution est de ne pas manipuler directement le curseur. Il y a

toujours toujours deux textes. Le texte gauche correspond à ce qui est à gauche du curseur
et le texte droit correspond à ce qui est à droite du curseur. Tout le reste en découle.

Le dernier commentaire de la section précédente s’applique ici aussi.

11.3 Troisième solution

Cette dernière solution est une variation de la deuxième où les schémas sont utilisés diffé-
remments, notamment à l’aide de schémas qui peuvent être réutilisés comme EntreeCaractere
ou FinFichier. De plus, la sous-spécification du message rep! est corrigée.

[TOUCHE ]

CARACTERE : F TOUCHE

suppr , fleche gauche, fleche droite, inser : TOUCHE

{suppr , fleche gauche, fleche droite, inser } ∩ CARACTERE = ∅
#{suppr , fleche gauche, fleche droite, inser } = 4

TEXTE == seq CARACTERE

MODE ::= Ecrit | Ecrase

MESSAGE ::= TexteTropLong | nil

105
taille max : N
taille max ≤ 65535

Editeur
gauche, droit : TEXTE
mode ecriture : MODE

#(gauche a droite) ≤ taille max

EditeurInit
Editeur
gauche = hi
droit = hi

EntreeCaractere
c? : TOUCHE
c? ∈ CARACTERE

EntreeFlecheDroite
c? : TOUCHE
c? = fleche droite

EntreeFlecheGauche
c? : TOUCHE
c? = fleche gauche

EntreeSuppr
c? : TOUCHE
c? = suppr

EntreeInser
c? : TOUCHE
c? = inser

106
InsererModeEcrit
∆Editeur
EntreeCaractere
mode ecriture = Ecrit
#(gauche a droite) < taille max
gauche 0 = gauche a hc?i
droit 0 = droit
mode ecriture 0 = mode ecriture

InsererFinModeEcrase
∆Editeur
EntreeCaractere
mode ecriture = Ecrase
#(gauche a droite) < taille max
droit = hi
gauche 0 = gauche a hc?i
droit 0 = droit
mode ecriture 0 = mode ecriture

InsererMilieuModeEcrase
∆Editeur
EntreeCaractere
mode ecriture = Ecrase
#(gauche a droite) ≤ taille max
droit 6= hi
gauche 0 = gauche a hc?i
droit 0 = tail droit
mode ecriture 0 = mode ecriture

InsererTropLong
ΞEditeur
EntreeCaractere
rep! : MESSAGE

(mode ecriture = Ecrit ∧ #(gauche a droit) = taille max )

∨ (mode ecriture = Ecrase ∧ droit = hi ∧ #(gauche a droit) = taille max )
rep! = TexteTropLong

107
 b (InsererModeEcrit ∨ InsererFinModeEcrase ∨ InsererMilieuModeEcrase)
InsererTotale =
∧[rep! : MESSAGE | rep! = nil ]
∨ InsererTropLong

AvancerCurseur
∆Editeur
droit 6= hi
gauche 0 = gauche a hhead droiti
droit 0 = tail droit
mode ecriture 0 = mode ecriture

FinFichier
Editeur
droit = hi

b EntreeFlecheDroite ∧ (AvancerCurseur
AvancerCurseurTotale =
∨ FinFichier ∧ ΞEditeur )

ReculerCurseur
∆Editeur
gauche 6= hi
gauche 0 = front gauche
droit 0 = hlast gauchei a droit
mode ecriture 0 = mode ecriture

DebutFichier
Editeur
gauche = hi

b EntreeFlecheGauche ∧ (ReculerCurseur
ReculerCurseurTotale =
∨ DebutFichier ∧ ΞEditeur )

Supprimer
∆Editeur
EntreeSuppr
droit 6= hi
gauche 0 = gauche
droit 0 = tail droit
mode ecriture 0 = mode ecriture

108
 SupprimerTotale =
b Supprimer
∨ (EntreeSuppr ∧ FinFichier ∧ ΞEditeur )

ChangerModeEcriture
∆Editeur
c? : TOUCHE
c? = inser
gauche 0 = gauche
droit 0 = droit
mode ecriture 0 6= mode ecriture

Tableau des préconditions En général, le tableau des préconditions permet, en un coup

d’oeil, de nous aider à voir si tous les cas d’exceptions ont été traités. Ici, il nous permet de
voir que toutes les entrées possibles de touches sont traitées.

Opération Préconditions Exceptions

InsererModeEcrit c? ∈ CARACTERE
mode ecriture = Ecrit InsererModeEcrase
#(gauche a droite) < taille max InsererTropLong
InsererFin... c? ∈ CARACTERE
ModeEcrase mode ecriture = Ecrase InsererModeEcrit
droit = hi InsererMilieuModeEcrase
#(gauche a droite) < taille max InsererTropLong
InsererMilieu... c? ∈ CARACTERE
ModeEcrase mode ecriture = Ecrase InsererModeEcrit
droit 6= hi InsererFinModeEcrase
#(gauche a droite) ≤ taille max
AvancerCurseur c? = fleche droite cf. version totale
droit 6= hi FinFichier
ReculerCurseur c? = fleche gauche cf. version totale
gauche 6= hi DebutFichier
Supprimer c? = suppr cf. version totale
droit 6= hi FinFichier
Changer... c? = inser
ModeEcriture

11.4 Conclusion
On peut souvent trouver plusieurs (plus d’une) façons différentes de faire une spéci-
fication formelle pour un même problème donné. Plus tard, nous aurons à travailler avec le

109
démonstrateur semi-automatique de Z-eves pour démontrer des théorèmes et des propriétés.
Il n’y a pas de lien (que ce soit proportionnel ou inversement proportionnel) entre la simpli-
cité d’une spécification formelle et la complexité de l’utilisation du démonstrateur. Ce n’est
que l’expérience qui vous guidera...

110
Chapitre 12

Machine de radiothérapie

Suite à tous ces exercices et exemples, nous pourrions nous demander : c’est bien beau
tout ça, mais est-ce vraiment utilisé ? Nous avons débattu de ce point dans le module 1
d’introduction. Les deux côtés de la médaille sont bien expliqués dans l’article de Hall ainsi
que dans celui de Wing. Ce qui vous manque maintenant, c’est un cas réel de l’industrie,
un exemple documenté où le langage Z a été utilisé pour le développement d’un système
informatique. Quels sont les choix des développeurs, quels commentaires ont-ils à formuler,
jusqu’à quel point le Z a-t-il été utile ?

Nous avons brièvement parlé de la machine de radiothérapie Therac-25 dans le module 1.

Ce que nous présentons dans ce chapitre est le développement d’un système informatique qui
permet l’opération d’une machine de radiothérapie, mais pas la Therac-25. Il s’agit plutôt de
la machine du centre médical de l’université de Washington à Seattle. Nous n’entrerons pas
dans les détails techniques de ce cyclotron utilisé en médecine nuclélaire. Nous allons nous
concentrer sur les aspects touchant au génie logiciel présentés dans les nombreux documents
se trouvant à l’adresse suivante.

http ://[Link]/∼jon/z/[Link]

D’ailleurs, ces documents touchent à tous les aspects du génie logiciel et constituent une
lecture extrêmement intéressante pour ceux qui voudraient avoir une vision un peu moins
scolaire de cette science en perpétuel développement. On trouve à cette adresse une multitude
de documents relatifs à ce projet et nous ne ferons qu’un survol rapide afin de vous donner
un aperçu du projet, mais surtout la place que le langage Z a prise.

111
12.1 Présentation du projet

La machine de radiothérapie est le cyclotron du CNTS (Clinical Neutron Therapy Sys-

tem). L’accélérateur de particules permet de prodiguer des traitements de médecine nucléaire,
la production d’isotopes médicaux ainsi que de faire des expérimentations en physique nu-
cléaire et en radiobiologie. Le système de contrôle comprend six processeurs et gère plus de
mille signaux d’entrées/sorties à la fois. Il doit rencontrer des critères de disponibilité, de
protection d’équipement et de sécurité pour les utilisateurs. De plus, puisque la machine est
unique et qu’elle doit être gérée par une équipe interne d’ingénieurs, il doit être facile et
économique d’effectuer les mises à jour et la maintenance. Les appareils contrôlés par les
systèmes informatiques incluent un électroaimant de neuf cent ampères ainsi qu’une partie
rotative de trente-neuf tonnes. On ne parle pas de la gestion d’une bibliothèque !

Le système est en opération depuis 1984. Au début des années 90, Jacky et son équipe
travaillent à développer un nouveau système de contrôle de tout cet appareillage qui sera
installé à la fin des années 90. Parmi les décisions qu’il ont eu à prendre, il a fallu choisir
quelles parties du système déjà existentes il était préférable de conserver et lesquelles de-
vaient être modifiées.

Vous pouvez trouver la spécification informelle (écrite en anglais) de ce système toujours

sur le même site. La description complète du système couvre presque cinq cent pages. Nous
avons beaucoup parlé des erreurs possibles d’interprétation d’un document de spécification
informelle. Dans ce cas-ci, le nombre de pages n’aide pas à simplifier la tâche. L’autre pro-
blème est qu’une erreur peut entraîner non seulement d’importantes pertes monétaires, mais
surtout détériorer considérablement la qualité de vie de personnes humaines, voire causer
leur mort.

Leur objectif principal est celui de la sécurité. L’énoncé exact est le suivant.

“The therapy beam can only turn on or remain on when the actual setup of the machine
matches a stored prescription that the operator has selected and approved.”

Dans les objectifs secondaires, on retrouve les deux que voici.

— Rendre les traitements plus efficaces en rendant automatique certaines manipulations
internes comme par exemple le système de dosimétrie.
— Enregistrer de façon automatique les informations pertinentes lues par le système du-
rant le traitement pour aider au contrôle de qualité ainsi qu’à la maintenance.

Un tel système de contrôle est complexe. C’est pourquoi il est très difficile d’en concevoir
un qui soit correct et sécuritaire. Si on fait le choix qu’un tel système soit informatique, ce
doit être parce qu’il est impossible ou hautement improbable qu’un système non automatisé
puisse offrir une fiabilité comparable.

112
 Dans les documents présentés sur le site internet, on retrouve plusieurs autres objectifs
secondaires ainsi que quelques astuces générales pour y parvenir.

12.2 Architecture du réseau et architecture du programme

La complexité et les coûts reliés à un tel développement font que l’on ne peut pas se
permettre de recommencer tout le travail régulièrement. Les choix qui sont faits doivent être
viables à long terme. C’est le premier critère qui a guidé l’équipe lors des prises de décisions
pour l’architecture du réseau et pour le choix des pièces à utiliser.

Ils ont choisi une architecture composée de plusieurs ordinateurs connectés sur un réseau.
Cette architecture comporte plusieurs avantages : elle facilite le développement ainsi que la
maintenance parce la machine peut être utilisée même si l’un des ordinateurs est absent du
réseau. Il offre plus de flexibilité pour la localisation des différents appareils. Les mises à
jour sont plus faciles à effectuer puisque les composantes peuvent être remplacées une à la
fois, dans certains cas même si la machine est en marche. Il y a un réseau local strictement
réservé au fonctionnement de la machine. Cela minimise les risques de congestion de réseau.
Un seul ordinateur est branché sur le réseau principal de l’hôpital et agit comme médium.

Chaque ordinateur est autonome et peut continuer à exécuter ses tâches même si le
contact avec les autres est rompu. L’attente d’un message ne peut pas compromettre la
sécurité, et ce même si le message n’arrivait jamais.

12.3 Logiciels et pièces utilisés

Une fois l’architecture décidée, il faut choisir le matériel et les produits logiciels qui seront
utilisés. Pour éviter que le matériel ne devienne désuet trop rapidement, il faut choisir des
produits qui sont utilisés à grande échelle, qui ont une longue durée de vie et qui pourront
facilement être remplacés par des produits compatibles. Les produits choisis sont utilisés
dans l’industrie depuis plusieurs années, si bien que les défauts et les limitations sont bien
documentés.

Les détails sont dans le document A Control System for a Radiation Therapy Machine
écrit par Jacky, Risler, Reid, Emery, Unger et Patrick (d’ailleurs, ce document est proba-
blement le meilleur qui puisse servir de conclusion à ce module. De plus, on y retrouve de
nombreux aspects de génie logiciel fort intéressants pour vous).

À propos des langages utilisés, le langage de programmation utilisé est le C (sauf pour
certaines composantes qui devaient préférablement utiliser le langage fourni par le manufac-

113
turier) et n’utilise que des librairies universellement reconnues (à quelques exceptions près).
Le système d’exploitation n’est pas un système comme Unix ou Windows, mais plutôt un
plus petit et plus simple qui permet de manipuler les fonctionnalités nécessaires pour le pro-
jet (voir le même document pour plus de détails).

Le code a été écrit à la main. Il n’y a pas eu d’utilisation d’un générateur semi-au-
tomatique de code. Il n’y a pas eu d’utilisation de base de données ou de produits pour
manipulation de graphiques. Tout a été réduit au plus simple. L’analyse et la maintenance
est alors beaucoup plus simple.

12.4 Méthode de développement

Dans l’article A Control System for a Radiation Therapy Machine mentionné plus tôt,
une section est intitulée “Development method”. Nous allons nous y attarder plus sérieuse-
ment. Nous présentons ici le détail de chacune des sous-sections. C’est la partie du texte qui
est la plus près des objectifs du cours.

Dans cette partie de l’article, les auteurs décrivent la méthode de développement utilisée
pour faire le design, écrire le code, analyser et tester le programme.

C’est bien connu, la programmation est faillible. Il arrive souvent que des erreurs ma-
jeures échappent à l’attention des ingénieurs logiciels et des programmeurs sur l’équipe de
développement. Dans le contexte d’une machine de radiothérapie, ces erreurs peuvent entraî-
ner des conséquences fatales. Selon les auteurs, “Finding better methods for preventing and
detecting errors is an active area of research and controversy.” Ils ont donc décidé d’essayer
les méthodes formelles. Elles sont utilisées dans l’industrie sous diverses formes, mais en
médecine nucléaire, il semble que ce soit la première fois.

Rappelez-vous l’objectif principal mentionné plus tôt : “the beam can only turn on (or
remain on) when the actual setup of the machine conforms to the stored prescription selected
by the operator.”

12.4.1 Écrire les besoins

Les besoins, nous le savons, décrivent les propriétés que le système doit satisfaire afin
d’être acceptable pour les utilisateurs. Ils doivent être décrits par un texte appuyé de dia-
grammes lorsque nécessaire afin d’être compris par tout le monde.

Dans ce cas-ci, les auteurs du document des besoins incluent le physicien qui a décrit les
besoins pour le système initial, les ingénieurs qui ont installé la machine et qui assurent sa

114
maintenance puis les utilisateurs de cette machine (le personnel médical). Il semble qu’écrire
les besoins fut une partie très prenante du projet, pas seulement une étape préliminaire

12.4.2 Écrire la spécification formelle

La spécification formelle, comme chacun s’en doute, est une collection de formules ma-
thématiques qui modélise les besoins et les contraintes sur un ensemble de variables d’états.
Les gens de l’équipe ont choisi le Z !

L’ensemble des variables d’états représente tous les aspects importants de la machine et
d’une séance de traitement. Il s’agit de variables d’états qui représentent chaque configura-
tion possible du système, l’état du système, les opérations en cours, le patient, les champs
d’identification pour accéder aux différentes prescriptions, etc. Leur spécification compte 410
variables d’état. Selon les auteurs, le Z permet de manipuler adéquatement un très grand
nombre de variables.

Comme nous l’avons expliqué plus d’une fois depuis le début de la session, ils ont dû écrire
des formules qui représentent les propriétés et les contraintes qui doivent être respectées par
le système à tout moment 1 . Il s’agit des invariants ! Toutes les contraintes de sécurité dans
ce cas-ci se transforment en invariants. Si l’un des invariants s’évaluait à faux durant l’uti-
lisation de la machine, violant ainsi les contraintes de sécurité, et que la machine continuait
à fonctionner, les conséquences pourraient être jusqu’à létales.

Autrement dit, dans cet exemple, les invariants représentent exactement ce que signifie
“être dans un état sécuritaire”. Plusieurs variables ajoutées au projet par la spécification
formelle prennent naissance dans les invariants parce qu’elles modélisent des informations
qui sont absentes du programme en tant que tel. Le programme est en fait un ensemble
(très grand) de transitions. Avec beaucoup de travail, on pourrait analyser le code et ainsi
déterminer l’ensemble des états atteignables. Cependant, cela ne nous dirait pas si ces états
atteignables sont sécuritaires. Une analyse de sûreté correspond en fait à déterminer si l’en-
semble des états atteignables par le système est un sous-ensemble des états sécuritaires. On
a donc besoin d’avoir une description précise des états sécuritaires du système et c’est jus-
tement ce que nous donne la spécification formelle.

En plus des invariants, il faut aussi écrire des formules qui représentent les transitions
entre les états. Ce travail est beaucoup plus près du code qui sera écrit par les programmeur.
Ces formules sont tout de même écrites avec le même langage mathématique. Elle sont
plus concices que le code parce qu’elles représentent uniquement l’effet de la transition et
non pas comment comment s’effectue cette transition. Chaque opération se résume en une
précondition qui décrit les états à partir desquels la transition peut s’effectuer ainsi qu’en
1. Sauf lorsqu’il est éteint ? ;)

115
une postcondition qui décrit l’état dans lequel la transition envoie le système. Pour décrire
ce système de gestion de la machine de radiothérapie, il a fallu 105 transitions et 2103 lignes
de code Z.

12.4.3 Analyse de la spécification formelle

Vous vous souvenez ce que nous avons vu en classe concernant les théorèmes à démon-
trer ? Lisez attentivement les mots des auteurs : “First, show that the initial states are safe.
Then, for each state transition, show that if its starting state is safe, then its ending state
is safe also. That’s all.” Laissons parler les auteurs encore une fois, c’est instructif : “This is
usually a straightforward exercise in the simplification of logical expressions.” Ont-ils utilisé
le démonstrateur semi-automatique pour leurs 2103 lignes de code Z ? Non, ils ont utilisé
“inspection (by eye) and a few pencil-and-paper calculations.” Puisque l’analyse n’a pas été
automatisée, elle est sujette à des erreurs comme on s’en doute. Bien sûr, ils ont tout de
même utilisé la démonstration semi-automatique pour vérifier que la syntaxe était bonne
et aussi pour démontrer les théorèmes de domain$Check . Repensez au démonstrateur semi-
automatique et je vous laisse tirer vos conclusions.

Dans le projet qui nous intéresse présentement, il y a un aspect temporel dont nous
n’avons pas encore parlé (ni dans le cours ni dans ce document). Pour analyser les contraintes
temporelles, l’équipe a utilisé une techinique de simulation appelée la “vérification de mo-
dèles”. Pour ce faire, ils ont exprimé certaines parties du programme en un langage de
programmation utilisé par le vérificateur. Ils ont ainsi obtenu une version simplifiée de leur
programme qui permettait tout de même de vérifier des propriétés temporelles. Les propriétés
à vérifier, elles, ont été écrites dans un langage formel appelé CTL.

12.4.4 Coder le programme

La spécification formelle a aussi servi de design détaillé pour une grande partie du code.
Mis à part l’anglais, aucun autre langage n’a été utilisé pour le design. En moyenne chaque
paragraphe de Z a pu être traduit en moins d’une page de code C. Il a donc été facile de
vérifier que le programme final était conforme à la spécification.

Le groupe n’avait qu’un accès restreint à la macine qui était en opération à l’aide du
système de contrôle original. Il a donc fallu développer des versions du programme qui
n’exigeaient pas d’être connectées à la machine réelle. Les versions de test roulaient sur un
ordinateur standard. Les entrées/sorties étaient simulées par une sous-routine qui lisait et
écrivait plutôt dans un fichier. Vers la fin, des tests ont été effectués sur la machine réelle.
Le code n’a pas beaucoup changé de version en version.

116
 Le programme a été construit de façon incrémentale et a été en constante révision. Tous
les changements, révisions, corrections ont été enregistrés.

12.4.5 Tester et évaluer le programme

Les analyses formelles décrites précédemment ont été effectuées sur la spécification for-
melle, pas sur le code. Elles avaient pour but de déceler des erreurs dans le design. Elles
n’ont rien à voir avec le code en tant que tel. Ils ont utilisé l’inspection de code pour détecter
les erreurs de code.

L’équipe a fait une distinction entre le test et l’évaluation. Selon les auteurs, le test sert
à détecter des erreurs qui font que le programme viole la spécification. L’évaluation quant à
elle, sert à clarifier les besoins, voir quelle est l’acceptation des clients ou encore entendre des
suggestions pour amélioration. Ils ont surtout fait de l’évaluation durant le développement,
pas du test. La plupart des changements ont été des ajouts et des améliorations, pas des
corrections d’erreurs.

Aux étapes de démonstration et de simulation, la plupart des tests ont été effectués
automatiquement en exécutant des scripts de test. Dans la phase d’évaluation et d’accepta-
tion, le programme a été utilisé avec la machine de la même façon qu’il serait utilisé par le
médecin lors d’un traitement sur un patient. Certains essais ont été faits simulant des bris
d’équipement ou des bogues de programme.

12.5 Conclusion

Ce que vous avez lu dans ce chapitre concerne un projet bien précis. Chaque programme
à développer amène ses contraintes et ses décisions à prendre. Certains cas sont bien docu-
mentés parce qu’ils ont souvent été étudiés. D’autre cas, comme celui-ci, sont moins courants.
On ne crée pas un système de contrôle de machine de radiothérapie tous les jours !

Chaque décision est toujours prise en rapport avec les besoins. Toujours dans l’optique
de satisfaire les attentes du client ou des utilisateurs. Dans ce cas-ci, tout est fait de façon à
assurer la sécurité.

Toutes les questions abordées dans ce chapitre relèvent du génie logiciel. Dans certains
projets, on se concentre sur une phase du développement ou sur un ensemble. Dans ce cas-ci,
on a choisi d’utiliser les méthodes formelles.

117
Annexe A

Les fondements de Perfect Developer

118