3.4.

Techniques formelles de spécification

(Rappel) Techniques semi-formelles:
- Spec formelle des aspects globaux (souvent: langage graphique)
= partie "déclaration"
−> vue d'ensemble du système
- Spec informelle des détails
= partie "assertion"
−> annotations informelles précisant concepts déclarés
⇒ communicabilité
⇒ formes limitées de vérification automatisée (sémantique statique)
MAIS: beaucoup de problèmes dûs au langage naturel subsistent
Techniques formelles:
spécification de la partie "déclaration" et de la partie "assertion"
dans un langage formel (syntaxe, sémantique, théorie de la preuve)
Avantages
• Règles précises d'interprétation des assertions (sémantique)
⇒ - précision, non-ambiguité
- questions se posant lors de la formalisation, à fixer
• Analyse formelle possible, plus sophistiquée, par outils
⇒ - calcul de conséquences logiques
(théorèmes à ratifier par l'utilisateur)
- détectiond'inconsistances logiques
- model checking, analyse d'accessibilité d'états
- génération de maquettes exécutables, de simulations
- génération de jeux de test
- génération de contre-exemples
- raffinement formel vers des programmes
- réutilisation de specs formelles par "pattern matching"
Domaine actif de recherche en génie logiciel
Utilisation industrielle croissante, surtout secteurs critiques
Transport ferroviaire, aérien, automobile; énergie, médical, ...
cf. RATP/RER, métro parisien ligne 14: 200.000 théorèmes!

3.1
Beaucoup de langages formels de spécification sont basés sur
extensions / variantes de la logique des prédicats 1er ordre

Bref rappel (cfr. INGI2101 pour détails)

SYNTAXE
Assertions = formules prédicatives
<terme> ::= <constante> | <variable> |
<symb-fonction> '(' <terme>* ')'
Les termes représentent des objets
[Link]. a, b, ...., x, y, ..., f(t1, ..., tn), ...
f : #, ∪, fonctions d'accès aux objets, ...
<formule-atomique> ::= true | false |
<symb-prédicat> '(' <term>* ')'
<assertion> ::= <formule-atomique> | '(' ¬ <assertion> ')'
| '(' <assertion> '∧' <assertion> ')'
| '(' <assertion> '∨' <assertion> ')'
| '(' <assertion> '⇒' <assertion> ')'
| '(' <assertion> '≡' <assertion> ')'
| '(' '∀' <variable> ')' '(' <assertion> ')'
| '(' '∃' <variable> ')' '(' <assertion> ')'

Les formules atomiques représentent des relations entre objets

P(t1, ..., tn) [Link]. P : =, ≤, ∈, ...

3.2
SEMANTIQUE
Règles sémantiques pour définir les valeurs de vérité VALI (ass)
d'une assertion ass dans une interprétation d’intérêt I
I: interprétation pour {P, Q} P, Q: assertions
−> fonction de représentation valI sur domaine d'interprétation DI

VALI (x) = valI (x) , VALI (a) = valI (a)

VALI (f(t1, ..., tn)) = (valI (f)) (VALI (t1), ..., VALI (tn))

VALI (true) = V , VALI (false) = F

VALI (P(t1, ..., tn)) = (valI (P)) (VALI (t1), ..., VALI (tn))
VALI (¬P) = V ssi VALI (P) = F
VALI (¬P) = F ssi VALI (P) = V
VALI (P ∧ Q) = V ssi VALI (P) = V et VALI (Q) = V
F sinon
VALI (P ∨ Q) = V ssi VALI (P) = V ou VALI (Q) = V
F sinon
VALI (P ⇒ Q) = V ssi VALI (P) = F or VALI (Q) = V
F sinon
VALI (P ≡ Q) = V ssi VALI (P) = VALI (Q)
F sinon
VALI ( (∀x) P ) = V ssi VAL{x ← d} o I ( P ) = V
pour chaque d ∈ DI
VALI ( (∀x) P ) = F ssi VAL{x ← d} o I ( P ) = F
pour au moins un d ∈ DI
VALI ( (∃x) P ) = V ssi VAL{x ← d} o I ( P ) = V
pour au moins un d ∈ DI
VALI ( (∃x) P ) = F ssi VAL{x ← d} o I ( P ) = F
pour chaque d ∈ DI
3.3
Dans le contexte des spécifications formelles:
- assertion <−> axiome
- spécification d'un (sous-)système <−> théorie
- spécification...
• inconsistante <−> pas de modèle
• ambigue ou incomplète <−> plusieurs modèles dans le
domaine d'interprétation d'intérêt
(manquent des axiomes/spécifications pour restreindre l'ensemble des modèles)
• adéquate: le modèle représente
les propriétés, le comportement souhaité du système

THEORIE DE LA PREUVE
Règles d'inférence pour dériver de nouvelles assertions, [Link].

P ⇒ Q, P
-------------------- modus ponens
Q
P ⇒ Q, Q ⇒ R
------------------------- chaînage
P⇒R
(∀x) (P(x))
-------------------- instanciation
P(x/a)
L+ ∨ C1 , L- ∨ C2
-------------------------------- résolution
(C1 ∨ C2 ).µ
avec P, Q: assertions; x: variable; a: constante;
C1, C2 : formes clausales;
L+, L- : litéraux positifs/negatifs
à même symbole de prédicat & unificateur le plus général µ

3.4
 Z: une technique de spécification formelle
basée sur les états
cf. Book, Section 4.4.3
[Abrial], [Sufrin], [Oxford & IBM/UK]

J.M. Spivey, The Z Notation, 2nd edition, Prentice Hall, 1989

[manuel de référence du langage]
B. Potter, J. Sinclair & D. Till,
An Introduction to Formal Spécification and Z, Prentice Hall, 1991
[aspects plus méthodologiques]

Principe général d'une technique de spécification basée sur états:

• Spécification des fonctionnalités
• Unité de spécification: opération ou type de données
- Pour une opération, on spécifie:
• ses entrées / sorties & leurs types respectifs
• la classe d'états initiaux admissibles
(plus faible précondition)
• la classe d'états finals désirés
(plus forte postcondition)
- Pour un type de données, on spécifie:
• ses attributs & leurs types respectifs
• la classe des états à maintenir
par n'importe quelle opération sur le type
(invariant)
"Type" = ensemble de valeurs possibles
"Etat" = { (nom-variable, valeur) }* = “snapshot state”
=> spécification d'un instantané du système

3.5
Autre technique "classique" basée sur les états: VDM
C. Jones, Systematic Software Development Using VDM, Prentice Hall, 1990

Autres techniques de spécification formelle:

• Basées sur les histoires du système:
possibilité de références au passé, au futur
(impossible avec une technique basée sur les états)
−> logiques temporelles
Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent
Systems. Springer-Verlag, 1992
A. Dardenne, A. van Lamsweerde and S. Fickas, "Goal-directed Requirements
Acquisition", Science of Computer Programming, Vol. 20, 1993

• Basées sur les lois de composition algébriques

des opérations définissant un type abstrait
−> logiques équationnelles, algèbres universelles
(technique de déduction/calcul efficaces: réécriture)
J.V. Guttag and J.J. Horning, LARCH: Languages and Tools for Formal
Spécification, Springer-Verlag, 1993
M.C. Gaudel, “Towards Structured Algebraic Spécifications”, ESPRIT'85
Status RAPPORT, North Holland, 1986, 493-510.

• Basées sur un modèle opérationnel du système

−> spécification exécutable
R.M. Balzer, N.M. Goldman, and D.S. Wile, “Opérational Spécification as the
Basis for Rapid Prototyping”, ACM SIGSOFT Software
Engineering Notes Vol. 7 No. 5, Dec. 1982
P. Zave, “An Opérational Approach to Requirements Spécification for Embedded
Systems”, IEEE Transactions on Software Engineering, vol. 8
no. 3, May 1982

3.6
Z: survol des caractéristiques principales
(i) Base formelle:
- ensembles & n-uples
=> relations, fonctions, ... au-dessus de cette "couche"
langage relationnel
- logique des prédicats 1er ordre typée
pour écrire assertions sur ensembles, fonctions, etc
(ii) Pouvoir d'expression:
- limité aux specs fonctionnelles
- pas de référence possible au passé, futur
=> "codage" nécessaire d'événements passés/futurs
par variables auxiliaires, artificielles
[Link]. variable Booléenne
pour "mémoriser" si un livre a été demandé par un emprunteur
variable Booléenne
pour "mémoriser" si 2 téléphones sont connectés
A METTRE A JOUR PAR TOUTES LES OPERATIONS CONCERNEES!!!
(devient une activité de programmation)

(iii) Communicabilité:
- relativement bonne, à cause de la simplicité du langage:
bases mathématiques classiques, bien connues
(ensembles, relations & fonctions)
=> Z et VDM de plus en plus utilisés en pratique

(iv) Constructibilité & pouvoir de structuration:

- unité de spécification = schéma (pour un type ou une opération)
- mécanismes de combinaison de schémas:
- inclusion de schéma ( => ± héritage de caractéristiques)
- composition/décomposition logique (ET/OU) de schémas
+ librairie de schémas prédéfinis
(= boîte à outils comprenant opérations sur relations, fonctions, séquences, ...)

3.7
1. LES SCHÉMAS Z
• Spécification = collection de schémas + définitions textuelles

• Un schéma definit un type ou une opération

(type = ensemble de valeurs possibles;
un schéma definit des classes d'états admissibles)

• Structure générale d'un schéma:

NomSchéma____________________
partie déclaration
partie assertion

(i) Pour une définition de type :

NomType______________________
déclaration des "attributs" du type
invariants sur attributs déclarés

Une déclaration d'attribut a la forme: Attribi: Typei

(signifie: "les valeurs possibles de Attribi appartiennent à l'ensemble Typei")

Un attribut peut être simple ou composé:

n-uple, ensemble, relation, fonction, séquence, ...
[Link] capacité: Νat simple
switch: {off, on} simple, type énuméré
date: JOUR × MOIS n-uple
_ ×_ : produit cartésien
disponible: PEXEMPLAIRE-LIVRE ensemble
P _ : ensemble des parties d'un ensemble
répertoire: PLIVRE × EXEMPLAIRE-LIVRE relation
"P _ × _ " noté "_ ↔ _": ensemble des relations binaires
QuelLivre: EXEMPLAIRE-LIVRE ↔ LIVRE
exemplaire d'un seul livre => relation est une fonction:
QuelLivre: EXEMPLAIRE-LIVRE → LIVRE
_ → _: ensemble des fonctions

3.8
Les déclarations de fonctions spécifient donc plus que du typage:
• contrainte qu'un élément a une seule image par la relation
=> expression de certaines contraintes de cardinalité
• fonction partielle -|->
ou totale -->
• fonction injective > >-|-> , >-->
surjective -|-» , --»
ou bijective >--»

Exemple de définition de type:

Agenda ____________________________
AvecQui: PNOM
RendezVous: PLAGE-HORAIRE -|-> NOM
------------------------------------------------------------
AvecQui = ran RendezVous
∀d1,d2 ∈ dom RendezVous • |d2 - d1| ≥ 2h

dom: domaine de
ran: codomaine de ("range")
|→ : couplage fonctionnel
• : séparation quantification-prédicat (pour éviter sur-parenthésage)

Une définition de type spécifie l'espace des états admissibles

pour les instances de ce type
Exemple d'état admissible:
AvecQui = {bernard, michel, robert}
RendezVous = {7/11-9h |→ michel, 7/11-11h |→ robert, 9/11-18h |→ bernard}
NB1 Spécification de rendez-vous individuels (RendezVous est une fonction)
Pour rendez-vous avec groupes: déclarer RendezVous comme une relation:
RendezVous: PLAGE-HORAIRE × NOM
NB2 Les assertions sur lignes séparées sont implicitement connectées par ' ∧ '

3.9
(ii) Pour une définition d'opération:
NomOpération_____________________
déclaration d'information d'entrée/sortie
pré- & post-conditions de l' opération

L'information d'entrée/sortie peut comporter:

• un nom de schéma
=> déclaration: <genre d'opération> NomSchéma
genre d'opération: Ξ (inspection), ∆ (modification)
• des variables d'entrée ou de sortie
=> déclaration: vari <décoration de variable>: Typei
décoration de variable: ? (entrée), ! (sortie)

Exemples
• Opération de consultation
Quand____________________________________________
Ξ Agenda
n? : NOM
d! : PPLAGE-HORAIRE
--------------------------------------------------------------------------------------------
n? ∈ AvecQui
d! = {t: PLAGE-HORAIRE | RendezVous (t) = n?}
ou, de manière alternative,
d! = RendezVous -1 (| {n?} |) */ image relationnelle d'un ensemble /*

NB Precondition implicite: assertion sur var?

Postcondition implicite: assertion sur var! ou var’

3.10
• Opération de création
PrendreRendezVous______________________________
∆ Agenda
n? : NOM
t? : PLAGE-HORAIRE
-------------------------------------------------------------------------------------------------------------------------------
¬∃ d: PLAGE-HORAIRE, m: AvecQui •
d |→ m ∈ RendezVous ∧ | d - t?| < 2h
RendezVous' = RendezVous ∪ {t? |→ n?}
AvecQui' = AvecQui ∪ {n?}

∆: pour distinguer états initial & final de x dans même assertion

x, x' dans schémas-∆
Ξ Agenda" permet d'éviter d'écrire
- Ecrire "Ξ
AvecQui' = AvecQui, RendezVous' = RendezVous
dans la postcondition de Quand.
Utilisé pour opérations de consultation pour dire "rien ne change"
- RendezVous, AvecQui sont des noms locaux à Agenda,
importés par Quand et PrendreRendezVous par l'inclusion de Ξ/∆
∆ Agenda
- ? , ! , ' sont des "décoration de schéma " en jargon Z

• Opération de mise à jour

DéplacerRendezVous_______________________________
∆ Agenda
n? : NOM
To?, From?: PLAGE-HORAIRE
----------------------------------------------------------------------------------------------------------------------
¬∃ d: PLAGE-HORAIRE, m: AvecQui •
| d - To?| < 2h ∧ d |→ m ∈ RendezVous
From? |→ n? ∈ RendezVous
RendezVous' = RendezVous ∪ {To? |→ n?} \ {From? |→ n?}
AvecQui' = AvecQui

f ⊕ g: "surimpression" fonctionnelle de f par g:

- fonction definie sur (dom f ∪ dom g)
- s'accorde avec: g sur dom g
f ailleurs

3.11
• Etat initial du système (nécessaire pour raisonnements par induction):
doit être specifié par spécialisation des schémas de type
avec assertion supplémentaire particularisant l'état initial
Exemple:
AgendaInit_____________________
Agenda */inclusion de schéma/*
AvecQui = ∅

inclusion de schéma =>

copie, dans schéma incluant, des déclarations & assertions du schéma inclus

• Les types donnés doivent être explicités ("given types")

= liste des types "de base", non spécifiés,
sur lesquels reposent les définitions de schéma
Exemple:
[NOM, PLAGE-HORAIRE]

Définitions génériques
But: rendre les définitions paramétrées
(occurrences de paramètres formels)
=> réutilisation dans contextes multiples par instanciation
(= substitution des paramètres formels par des paramètres effectifs)

2 sortes de définitions génériques:

(i) Attributs génériques:
spécification d'attributs en termes de types-paramètre
Forme:
[...liste de paramètres formels...] ________________________
Déclaration d'attributs en termes de types-paramètre
-----------------------------------------------------------------------------------------------------------------------------------------
Définition non-ambiguë des attributs déclarés
(toute instanciation doit determiner des valeurs de manière unique)

= mécanisme de base pour définir la boîte-à-outils Z

3.12
Exemples:
[X, Y] ___________________________________
first: X × Y → X
second: X × Y → Y
------------------------------------------------------------------------------------------------------------------
(∀x: X, y:Y) (first (x, y) = x)
(∀x: X, y:Y) (second (x, y) = y)

=> réutilisation dans contextes multiples par instanciation, [Link]

date: JOUR × MOIS
second (date)

[X, Y] _____________________________________
dom: (X ↔ Y) → PX
ran: (X ↔ Y) → PY
-------------------------------------------------------------------------------------------------------------------------
(∀ R: X ↔ Y) (dom (R) = {x: X | ∃ y: Y ∧ x |→ y ∈ R})
(∀ R: X ↔ Y) (ran (R) = {y: Y | ∃ x: X ∧ x |→ y ∈ R})

(ii) Schémas génériques:

définitions de schéma en termes de types-paramètre
Forme:
NomSchéma [...liste de paramètres formels...] _________
déclarations en termes de types-paramètre
invariants sur les attributs paramétrés

Exemple:
Dépôt [RESSOURCE] ___________________________
UtiliséPar: RESSOURCE -|-> UTILISATEUR
Libre: PRESOURCE
------------------------------------------------------------------------------------------------------------------
(dom UtiliséPar) ∪ Libre = RESSOURCE
(dom UtiliséPar) ∩ Libre = ∅

=> réutilisation dans contextes multiples par instanciation, [Link]

Bibliothèque = Dépôt [EXEMPLAIRE-LIVRE] (définition textuelle)

3.13
2. COMBINAISON DE SCHÉMAS
• Inclusion de schémas
SchémaSpecifique_______________
SchémaInclus1
...
SchémaInclusn
Déclarations spécifiques
---------------------------------------------------------------------------
Assertions spécifiques

Effet: SchémaSpecifique "hérite"

des déclarations & assertions de SchémaInclusi (1≤i≤n)
revient à une copie des déclarations & assertions
@! compatibilité de type requise pour variables communes!

Exemple
AgendaProfessionnel_________________
Agenda
∀ d ∈ dom RendezVous • 9 ≤ [Link] ≤ 18

• Composition logique de schémas

Un schéma peut être defini en termes d'autres schémas
à l'aide de connecteurs logiques:
NouveauSchéma = Sch1 <cl> Sch2 <cl> ... <cl> Schn
avec <cl> ::= '∧' | '∨' | '¬' | '⇒'
Effet: - l'ensemble des déclarations de NouveauSchéma =
union des ensembles de déclarations des Schi
@! compatibilité de type requise pour variables communes!
- assertion de NouveauSchéma =
composition des assertions des Schi à l'aide des <cl> correspondants
(possibilité d'inhiber des noms de Schi à l'aide de l'opérateur '\')

3.14
Exemple
PrendreRendezVous-Robuste = (PrendreRendezVous ∧ Succès) ∨ PasLibre
avec
PrendreRendezVous ______________________________
∆ Agenda
n? : NOM, t? : PLAGE-HORAIRE
--------------------------------------------------------------------------------------------------------------------------------------------
¬∃ d: PLAGE-HORAIRE, m: AvecQui •
d |→ m ∈ RendezVous ∧ | d - t?| < 2h
RendezVous' = RendezVous ∪ {t? |→ n?}
AvecQui' = AvecQui ∪ {n?}
Succès ______________________________________________
résultat! : MESSAGE
résultat! = 'ok'

PasLibre______________________________________________
Ξ Agenda
n? : NOM ; t? : PLAGE-HORAIRE
résultat! : MESSAGE
----------------------------------------------------------------------------------------------------------------------------------------------
∃ d: PLAGE-HORAIRE, m: AvecQui •
d |→ m ∈ RendezVous ∧ | d - t?| < 2h
resultat! = 'pas libre'

MESSAGE ::= {'ok', 'pas libre', 'libre', ...} définition de type libre
Cette spécification par morceaux est équivalente à:
PrendreRendezVous-Robuste ______________________________
∆ Agenda
n? : NOM; t? : PLAGE-HORAIRE
resultat! : MESSAGE
¬∃ d: PLAGE-HORAIRE, m: AvecQui •
d |→ m ∈ RendezVous ∧ | d - t?| < 2h
∧ RendezVous' = RendezVous ∪ {t? |→ n?}
∧ AvecQui' = AvecQui ∪ {n?} ∧ resultat! = 'ok'
∨ ∃ d: PLAGE-HORAIRE, m: AvecQui •
d |→ m ∈ RendezVous ∧ | d - t?| < 2h
∧ RendezVous' = RendezVous
∧ AvecQui' = AvecQui ∧ resultat! = 'pas libre'

3.15
=> Spécification "modulaire":
- élaboration incrémentale de schémas (morceaux assemblables)
- schémas peuvent être réutilisés dans d'autres contextes
(cfr. Succès, PasLibre)
−> procédé général pour l'introduction incrémentale d'exceptions

• Règles de visibilité (portée des noms)

- Variables quantifiées dans les assertions:
règles usuelles de la logique des prédicats: (∀/∃ x: X) (← ...→)
+ portées imbriquées (∀/∃ x: X) (← ... (∀/∃ y: Y) (← ...→) ... →)
- Les noms declarés dans un schéma sont locaux à ce schéma
(càd portée = schéma)
Les noms declarés dans un schéma reférencé dans d'autres schémasvia
Ξ, ∆, inclusion de schéma, composition logique
sont exportés vers les schémas incluant/combinant
(=> peuvent y être référencés)
−> portées imbriquées entre schémas
- Les paramètres formels sont locaux aux définitions génériques
- Les noms de schéma, attributs génériques, et types donnés sont globaux

- Possibilité d'introduire des variables globales à l'aide de schémas anonymes:

déclaration de variable globale
invariant sur variable globale
[Link].
limite: Νat
limite ≤ 999
utilisable dans
Compteur__________________________
valeur : Νat
valeur ≤ limite

(Les schémas anonymes sont donc implicitement inclus partout)

3.16
3. LA BOITE A OUTILS Z
Les types composés en Z forment une hiérarchie de spécialisation:
ensemble n-uple

relation

fonction

injection surjection multi-ensemble séquence

bijection
=> héritage / polyporphisme des opérateurs
de super-type vers sous-types

Sommaire des notations Z de base ("cablées" dans le langage)

type notation sémantique [Spivey 89] p.

ensemble {e1, e2, ...} formation d'un ensemble 58

PS ensemble des parties d'un ensemble S 59

("power set")
S1 × S2 produit cartésien 59

e∈ S appartenance à un ensemble 69

n-uple (e1, e2, ...) formation d'un n-uple 58

schéma type T. a référence à l'attribut a du type T

éléments de =,≠ égalité, inégalité 69, 89
même type

Opérateurs de la boîte à outils

définis comme attributs génériques du type correspondant,
en termes des notations de base => boîte à outils extensible !!

3.17
Principaux opérateurs de la boîte à outils:
type notation sémantique [Spivey 89] p.

ensemble e∉ S non-appartenance 89

∅ , #S ensemble vide, nombre d'éléments de S 90

⊂,⊆ inclusion d'ensembles 90

∪ ,∩ ,\ union, intersection, différence 91

n-uple first , second projection de couples ordonnés 93

relation S1 ↔ S2 ensemble des relations entre S1 et S2 95

e1 |→ e2 formation d'un couple ordonné 95

dom R domaine, codomaine d'une relation R 96
ran R
R1 R2 composition relationnelle: 97
R2 o R1 gauche-droite, droite-gauche
S
R restriction du domaine de R à l'ensemble S 98
R S restriction du codomaine de R à S
S
R anti-restriction du domaine, codomaine 99
R S (càd restriction au complément de S)
R -1 inverse de la relation R 100
R (| S |) image relationnelle de l'ensemble S par R 101

fonction S1 -|-> S2 ensemble des fonctions partielles/totales 105

S1 --> S2 de S1 vers S2

>-|-> , >--> ensemble des injections partielles/totales 106

-|-» , --» ensemble des surjections partielles/totales 107
>--» ensemble des bijections 107
f⊕g surimpression fonctionnelle de f par g 108

séquence seq S ensemble des suites sur S (⊂ Νat -|-> S) 118

〈e1, e2, ... 〉 formation d'une suite 118
s 1^ s 2 concaténation de suites s1, s2 119
head, last décomposition de suites 120
tail, front

3.18
4. ETUDE DE CAS: système de gestion de bibliothèque
Enoncé informel du problème

On considère un système bibliothécaire devant gérer les

transactions suivantes:
1. Emprunter un exemplaire de livre de la bibliothèque / restituer
un exemplaire.
2. Ajouter un exemplaire à la bibliothèque / retirer un exemplaire.
3. Obtenir la liste des livres pour un auteur donné ou sur un sujet
donné.
4. Obtenir la liste des ouvrages actuellement empruntés par un
emprunteur donné.
5. Retrouver l'emprunteur ayant en dernier lieu emprunté un
exemplaire donné.
Il y a deux types d'utilisateur: les membres du staff et les
emprunteurs ordinaires. Les transactions 1, 2, 4 et 5 sont réservées
aux membres du staff; les emprunteurs ordinaires peuvent
cependant effectuer la transaction 4 pour obtenir la liste des
ouvrages actuellement empruntés par eux-mêmes.
Le système doit en outre obéir aux contraintes suivantes:
• Chaque exemplaire de la bibliothèque est disponible pour
emprunt ou emprunté.
• Aucun exemplaire ne peut être à la fois disponible et emprunté.
• Un emprunteur ne peut avoir plus d'un nombre prédéfini
d'ouvrages empruntés en même temps.
("benchmark" en spécification)
J. Wing, A Study of 12 Specifications of the Library Problem,
IEEE Software, July 1988

3.19
Formalization en Z
(i) Types donnés
[ LIVRE, EXEMPLAIRE-LIVRE, AUTEUR, SUJET, PERSONNE]
avec LIVRE: ensemble de tous les livres possibles
EXEMPLAIRE-LIVRE: ensemble de tous les exemplaires possibles
AUTEUR: ensemble de tous les auteurs possibles
SUJET: ensemble de tous les sujets possibles
PERSONNE: ensemble de toutes les personnes possibles
NB1 "tous les ... possibles": pour permettre l'incorporation dans le futur
de n'importe quel livre, exemplaire, etc.
NB2 Les "types donnés" pourraient être spécifiés par la suite...

(ii) Schémas de type

Répertoire_________________________________________
QuelLivre: EXEMPLAIRE-LIVRE -|-> LIVRE
EcritPar: LIVRE -|-> P AUTEUR */ vu les fonctionnalités demandées /*
TraiteDe: LIVRE -|-> P1 SUJET */ vu les fonctionnalités demandées /*
*/ pas d'informations sur livres pas en bibliothèque
dom EcritPar ⊆ ran QuelLivre
dom TraiteDe ⊆ ran QuelLivre

• -|-> : car bib ne couvre pas l'ensemble de tous les livres/exemplaires possibles
• QuelLivre : toute instance est une fonction (relation) , ≠ association!!
(ensemble de couples, ≠ couple)
• ran QuelLivre: ensemble de tous les livres en bibliothèque
• Déclaration de EcritPar =>
l'ensemble des auteurs d'un livre peut être vide ([Link]. actes congrès, ...)
• P1S: ensemble des parties non-vides de S

Z encourage l'introduction de relations/fonctions comme attributs

=> notations ensemblistes, de plus haut niveau

3.20
Autres schémas de type: ("modules" de spécification)

AgentsBibliothèque_________________________________
EmprunteursOrdinaires: PPERSONNE
Staff: PPERSONNE
-------------------------------------------------------------------------------------------------
EmprunteursOrdinaires ∩ Staff = { }

BD-Bibliothèque__________________________________
AgentsBibliothèque
Disponibles, Empruntés: PEXEMPLAIRE-LIVRE
EmpruntéPar: EXEMPLAIRE-LIVRE -|-> PERSONNE
EmpruntPrécédent: EXEMPLAIRE-LIVRE -|-> PERSONNE
--------------------------------------------------------------------------------------------------
Disponibles ∩ Empruntés = { }
Empruntés = dom EmpruntéPar
ran EmpruntéPar ⊆ EmprunteursOrdinaires ∪ Staff
dom EmpruntPrécédent ⊆ Disponibles ∪ Empruntés
ran EmpruntPrécédent ⊆ EmprunteursOrdinaires ∪ Staff
∀ p: PERSONNE • p ∈ EmprunteursOrdinaires ∪ Staff ⇒
# EmpruntéPar- 1 (| {p} |) ≤ NbreMaxExemplaires

SystèmeBibliothèque________________________________
Répertoire
BD-Bibliothèque
---------------------------------------------------------------------------------------------
dom QuelLivre = Disponibles ∪ Empruntés

NbreMaxExemplaires: Νat
1 ≤ NbreMaxExemplaires ≤ ...

Exercice: Traduire les assertions formelles en Français "le plus naturel",

puis les reformaliser en Z, et comparer avec ces formalisations

3.21
Etat initial:
un schéma initial par schéma de type,
puis combiner le tout en un schéma global

RépertoireInit_______________________________________
Répertoire

QuelLivre = { } ∧ EcritPar = { } ∧ TraiteDe = { }

AgentsBibliothèqueInit________________________________
AgentsBibliothèque

EmprunteursOrdinaires = { } ∧ Staff = { }

BD-BibliothèqueInit__________________________________
BD-Bibliothèque
-----------------------------------------------------------------------------------------------------
Disponibles = { } ∧ Empruntés = { }
EmpruntéPar = { } ∧ EmpruntPrécédent = { }

SystèmeBibliothèqueInit =
RépertoireInit ∧ AgentsBibliothèqueInit ∧ BD-BibliothèqueInit

3.22
(iii) Schémas d'opération
• Emprunter un exemplaire
CAS NORMAL:
EmpruntNormal__________________________________
∆ SystèmeBibliothèque
Ξ Répertoire
Ξ AgentsBibliothèque
p? : PERSONNE
bc? : EXEMPLAIRE-LIVRE
--------------------------------------------------------------------------------------------
p? ∈ EmprunteursOrdinaires ∪ Staff ∧ bc? ∈ Disponibles
# EmpruntéPar -1 (| {p?} |) < NbreMaxExemplaires
Disponibles' = Disponibles \ {bc?}
Empruntés' = Empruntés ∪ {bc?}
EmpruntéPar' = EmpruntéPar ∪ {bc? |→ p?}
EmpruntPrécédent' = EmpruntPrécédent

AgentAutorisé______________________________________
Ξ AgentsBibliothèque
AgentDemandant? : PERSONNE
-----------------------------------------------------------------------------------------
AgentDemandant? ∈ Staff

EXCEPTIONS:
identifier cas où préconditions d'opérations normales sont non satisfaites
(+ autres éventuelles)
AgentNonAutorisé____________________________________
Ξ AgentsBibliothèque
AgentDemandant? : PERSONNE
mess! : RAPPORT
--------------------------------------------------------------------------------------------
AgentDemandant? ∉ Staff
mess! = 'opérateur non autorisé'

3.23
 NonInscrit_________________________________________
Ξ AgentsBibliothèque
p? : PERSONNE
mess! : RAPPORT
------------------------------------------------------------------------------------
p? ∉ EmprunteursOrdinaires ∪ Staff
mess! = 'personne non inscrite'

ExemplaireInexistant______________________________
Ξ SystèmeBibliothèque
bc? : EXEMPLAIRE-LIVRE
mess! : RAPPORT
--------------------------------------------------------------------------------------------
bc? ∉ Disponibles ∪ Empruntés
mess! = 'cet exemplaire n'est pas repris en bibliothèque'

ActuellementEmprunté_____________________________
Ξ SystèmeBibliothèque
bc? : EXEMPLAIRE-LIVRE
mess! : RAPPORT
------------------------------------------------------------------------------------------------
bc? ∈ Empruntés
mess! = 'cet exemplaire est actuellement emprunté'

QuotaAtteint________________________________________
Ξ SystèmeBibliothèque
p? : PERSONNE
mess! : RAPPORT
------------------------------------------------------------------------------------------------
p? ∈ EmprunteursOrdinaires ∪ Staff
# EmpruntéPar-1 (| {p?} |) = NbreMaxExemplaires
mess! = 'ne peut emprunter davantage d'exemplaires'

OPERATION D'EMPRUNT COMPLETE / ROBUSTE:

EmpruntComplet =
AgentAutorisé ∧ EmpruntNormal ∧ Succès
∨ AgentNonAutorisé ∨ NonInscrit ∨ ExemplaireInexistant
∨ ActuellementEmprunté ∨ QuotaAtteint

3.24
 Succès____________________________________________
mess! : RAPPORT
mess! = 'OK'

RAPPORT ::= {..., 'OK', ..., 'personne non inscrite', ...}

• Restituer un exemplaire
RestitutionNormale________________________________
∆ SystèmeBibliothèque
Ξ Répertoire
Ξ AgentsBibliothèque
bc? : EXEMPLAIRE-LIVRE
--------------------------------------------------------------------------------------------
bc? ∈ Empruntés
Disponibles' = Disponibles ∪ {bc?}
Empruntés' = Empruntés \ {bc?}
EmpruntéPar' = {bc?}
EmpruntéPar */ anti-restriction /*
EmpruntPrécédent' =
EmpruntPrécédent ⊕ { bc? |→ EmpruntéPar (bc?) }

ExemplaireDisponible________________________________
Ξ SystèmeBibliothèque
bc? : EXEMPLAIRE-LIVRE
mess! : RAPPORT
-------------------------------------------------------------------------------------------------
bc? ∈ Disponibles
mess! = 'cet exemplaire n'est pas emprunté'

RestitutionComplète =
AgentAutorisé ∧ RestitutionNormale ∧ Succès
∨ AgentNonAutorisé ∨ ExemplaireInexistant ∨ ExemplaireDisponible

(Noter la réutilisation de schémas d'exception définis dans d'autres contextes)

3.25
• Interroger la base de données
- Livres sur un sujet donné?
SurCeSujet_______________________________________
Ξ SystèmeBibliothèque
s? : SUJET
réponse! : PLIVRE
--------------------------------------------------------------------------------------------
réponse! = {x: LIVRE | s? ∈ TraiteDe (x)}

NB ... d'où l'introduction de la fonction TraiteDe comme attribut de Répertoire...

- Qui a emprunté quoi?

ExemplairesEmpruntésPar____________________________
Ξ SystèmeBibliothèque
p? : PERSONNE
réponse! : PEXEMPLAIRE-LIVRE
-----------------------------------------------------------------------------------------------
p? ∈ EmprunteursOrdinaires ∪ Staff
réponse! = EmpruntéPar -1 (| {p?} |)

SelfRequête________________________________________
Ξ AgentsBibliothèque
p? , demandeur? : PERSONNE
------------------------------------------------------------------------------------------------
p? = demandeur?

DemandeurNonAutorisé______________________________
Ξ AgentsBibliothèque
p?, demandeur? : PERSONNE
mess! : RAPPORT
-------------------------------------------------------------------------------------------
p? ≠ demandeur? ∧ demandeur? ∉ Staff
mess! = 'requête indiscrète'

3.26
 EmprunteurInconnu_______________________________
Ξ AgentsBibliothèque
p? : PERSONNE
mess! : RAPPORT
-----------------------------------------------------------------------------------------------
p? ∉ EmprunteursOrdinaires ∪ Staff
mess! = 'emprunteur inconnu'

ExemplairesEmpruntésPar-Robuste =
AgentAutorisé ∧ ExemplairesEmpruntésPar ∧ Succès
∨ SelfRequête ∧ ExemplairesEmpruntésPar ∧ Succès
∨ DemandeurNonAutorisé ∨ EmprunteurInconnu

- Qui a emprunté cet exemplaire en dernier lieu?

DernierEmprunteur_______________________________
Ξ SystèmeBibliothèque
bc? : EXEMPLAIRE-LIVRE
p! : PERSONNE
------------------------------------------------------------------------------------------
bc? ∈ Disponibles ∪ Empruntés
{bc? |→ p!} ∈ EmpruntPrécédent

PasPrécédemmentEmrunté____________________________
Ξ SystèmeBibliothèque
bc? : EXEMPLAIRE-LIVRE
mess! : RAPPORT
------------------------------------------------------------------------------------------------
bc? ∉ dom EmpruntPrécédent
mess! = 'cet exemplaire n'a pas été précédemment emprunté'

DernierEmprunteur-Robuste =
AgentAutorisé ∧ DernierEmprunteur ∧ Succès
∨ AgentNonAutorisé ∨ ExemplaireInexistant
∨ PasPrécédemmentEmrunté

3.27
NB1 A cause de l'impossibilité de spécifier en Z des références au passé, il a fallu
- introduire un "indicateur" EmpruntPrécédent
dans le schéma de type SystèmeBibliothèque
pour "mémoriser" le passé
- spécifier les mises à jour de cette variable
dans chaque schéma d'opération-∆ ∆ correspondant
−−> très lourd, ressemble à de la programmation!!!
Il existe des langages de spécification permettant d'éviter ces inconvénients:
supportent les références au présent / futur
(basés sur logiques temporelles)

NB2 Deux styles de spécification en Z:

- constructif (ou explicite):
prédicats d'égalité pour lier les résultats aux arguments dans la post
[Link]. EmpruntNormal, RestitutionNormale
- non-constructif (ou implicite):
autres prédicats pour écrire la post
[Link]. DernierEmprunteur

NB3 Noter encore l'intérêt du mécanisme de combinaison de schéma pour

- construire incrémentalement une spec
- réutiliser des morceaux précédemment spécifiés

3.28
5. RAISONNEMENT FORMEL SUR LES ASSERTIONS
La spécification du système forme une théorie
(ensemble d'axiomes sur vocabulaire restreint, en Z)
−> application de règles d'inférence pour deriver
- théorèmes / conséquences logiques à soumettre pour approbation
- inconsistances
- preuves d'invariance
- ...
• Règles classiques d'inférence de la logique des prédicats
(modus ponens, chaînage, instanciation universelle, résolution, ....)

• Règles de réécriture des théories avec égalité

- Substitutabilité fonctionnelle: pour ui , vi : termes,
u1 = v1 ∧ ... ∧ un = vn
f (u1, ..., un) = f (v1, ..., vn)
- Substitutabilité prédicative: pour ui , vi : termes,
u1 = v1 ∧ ... ∧ un = vn
P (u1, ..., un) ≡ P (v1, ..., vn)
• Règle d'inférence spécifique à Z
Prop [s] : "la propriété Prop est satisfaite dans l'état s"
s0 : état initial
{P} Op {Q} : si l'opération Op est appliquée dans un état qcq satisfaisant P,
son application résulte en un état satisfaisant Q

−> Règle d'invariance: (cfr. principe d'induction )

Prop [s0] , {Prop} Op {Prop} pour chaque opération-∆∆ Op

Prop [s] pour tout état s

3.29
Exemples de raisonnement formel sur le système bibliothécaire
1. Preuve d'invariance:
L'invariant
Disponibles ∩ Empruntés = ∅
du schéma BD-Bibliothèque est dérivable de la spécification des
opérations EmpruntComplet et RestitutionComplète.
Preuve. Soit Prop: Disponibles ∩ Empruntés = ∅
• Prop [s0] découle de la spec de l'état initial:
Disponibles = { }, Empruntés = { }
• {Prop} EmpruntComplet {Prop}:
- les exceptions AgentNonAutorisé, NonInscrit, ActuellementEmprunté, ...
ne modifient pas la valeur de Disponibles, Empruntés
- Soit l'opération-∆∆ EmpruntNormal appliquée dans un état satisfaisant Prop:
dans l'état final correspondant on aura:
Disponibles' ∩ Empruntés' = Disponibles \ {bc?} ∩ Empruntés ∪ {bc?}
[par modus ponens & substituabilité fonctionnelle]
avec bc? ∈ Disponibles (cfr. précond)
= ∅
[par théorème de la théorie des ensembles:
a ∈ A, A ∩ B = ∅ ⇒ A \ {a} ∩ B ∪ {a} = ∅ ]

• {Prop} RestitutionComplète {Prop}: la preuve est similaire

• D'où l'on dérive, par application de la règle d'invariance,

Disponibles ∩ Empruntés = ∅ pour tout état s Q.E.D.

3.30
2. Preuve de redondance:
La postcondition
Empruntés' = Empruntés ∪ {bc?}
dans le schéma EmpruntNormal est dérivable de la spécification
du type BD-Bibliothèque.
Preuve. De la spec de BD-Bibliothèque on dérive (par modus ponens):
Empruntés = dom EmpruntéPar dans tout état
Dès lors, dans les états finals résultant d'applications de EmpruntNormal, on a:
Empruntés' = dom EmpruntéPar'
= dom (EmpruntéPar ∪ {bc? |→ p?}) [substituabilité fonctionnelle]
= dom EmpruntéPar ∪ dom {bc? |→ p?} [theorème sur domaines]
= Empruntés ∪ {bc?} [substituabilité fonctionnelle & déf de dom]
Q.E.D.

3. Preuve d'inconsistance:
Une postcondition telle que
Empruntés' = Empruntés \ {bc?}
dans le schéma EmpruntNormal mènerait à une inconsistance
avec la spécification du type BD-Bibliothèque.
Preuve. Une dérivation similaire à 2 ci-dessus produit
Empruntés' = Empruntés ∪{bc?}
ce qui, conjointement à la postcondition supposée, produit
Empruntés \ {bc?} = Empruntés ∪ {bc?}
ce qui est inconsistant en théorie des ensembles. Q.E.D

3.31
Preuve d'inconsistance pour le système de gestion d'agenda:

Une postcondition telle que

AvecQui' = AvecQui
dans les schémas PrendreRendezVous, DéplacerRendezVous
mènerait à une spécification inconsistante.

Preuve. Par la spécification de l'état initial, on a:

AvecQui = ∅ dans l'état initial
A cause des postconditions supposées, on déduit dès lors, par application de la règle
d'invariance:
AvecQui = ∅ dans tout état,
ce qui produit
RendezVous = ∅ dans tout état,
par l'invariant AvecQui = ran RendezVous attaché au type Agenda.
Or, après la première application de l'opération PrendreRendezVous on obtiendra
un état dans lequel
RendezVous = { t? |→ n?}, [cfr. postcondition]
d'où l'inconsistance.

3.32