4 Raffinement
4.1 Introduction
Le raffinement est une technique utilisée au cours du processus de
développement logiciel pour transformer un modèle abstrait d'un
système logiciel (la spécification) en un modèle plus
concret, c'est-à-dire qui contient plus de détails sur la
spécification ou bien qui est plus près d'une implémentation.
Lors d'un raffinement, une machine M1 est remplacée par une autre
machine M2 qui va fournir des opérations de même nom et de même
signature mais qui seront implantées à l'aide de variables
d'états différentes ou qui satisferont une spécification plus forte.
On dira que deux opérations ont la même signature s'ils ont le même
nombre de paramètres d'entrée et de sortie et que ces paramètres sont
contraints à habiter les mêmes univers.
Si une opération op2 est un raffinement d'une opération
op1 alors toute utilisation de op1 doit
pouvoir être remplacée par une utilisation de op2, sans
casser le fonctionnement du programme.
4.2 Substitution et programme
Nous avons dit que les substitutions représentaient des
programmes. Cependant les substitutions sont définies par leur action
sur des prédicats [S]P. Nous allons préciser le lien entre les
substitutions et les relations de transformation sur la mémoire
(représentée par les valeurs des variables manipulées dans la
substitution).
4.2.1 Terminaison
L'interprétation de [S]P est la plus faible condition telle que si
elle est vérifiée alors toute exécution de S termine dans un état qui
vérifie P.
Une substitution S correspond donc à un programme qui termine
lorsque l'on peut démontrer [S](x=x). On pourrait en fait remplacer la
formule x=x par n'importe qu'elle formule toujours vraie.
Exemples
-
P|S termine lorsque [P|S](x=x) est vérifié, ie lorsque
P Ù [S](x=x) c'est-à-dire lorsque P est vrai et que S
termine.
- P ==> S termine lorsqu'on peut montrer que S termine sous
la condition que P est vrai (donc si P est faux on peut montrer
que P ==> S termine).
- S1[]S2 termine lorsque S1 et S2 terminent.
4.2.2 Substitutions comme des relations
Soit S une substitution portant sur une variable x, nous voulons
définir la relation rel(S)(a,a') qui dit que la
substitution S sur une entrée x où x=a peut s'exécuter et
terminera dans un état où x=a'.
Une première idée serait de prendre x=a Þ [S](x=a') .
Cependant, certaines des substitutions que nous définissons sont non
déterministes ou correspondent à des programmes qui ne terminent pas.
La formule x=a Þ [S](x=a') signifie que pour toute exécution de
S, cette exécution termine sur un état où x=a'. Nous sommes
intéressés par une relation plus faible de correction partielle qui
sera notée rel(S)(a,a') et qui signifie qu'il existe une
exécution de S partant d'un état où x=a qui soit ne termine pas
soit termine dans un état où x=a'.
Pour montrer cela il suffit d'établir qu'aucune exécution de S ne
termine à coup sûr dans un état où x¹a'. La propriété
[S]x¹a' représente la plus faible condition telle que si elle
est vérifiée alors après toute exécution de S, on peut établir
x¹a'. Donc cela signifie qu'aucune exécution de S n'aboutit à
x=a'. La condition qui nous intéresse qui dit qu'une exécution de
S ne termine pas ou conduit à x=a' est donc exactement la négation
de cette propriété. On définit donc :
rel(S)(a,a') ºx=a Þ¬([S](x¹a')) |
Lorsqu'on prend a=x, on obtient la formule équivalente
¬([S](x¹x')).
Exemples
-
rel(P|S)(x,x') est équivalent à P Þ
rel(S)(x,x')
- rel(P ==> S)(x,x') est équivalent à P Ù
rel(S)(x,x')
- rel(S1[]S2)(x,x') est équivalent à
rel(S1)(x,x') Ú rel(S2)(x,x').
4.3 Raffiner une substitution
4.3.1 Définition du raffinement
On suppose que l'on se donne deux substitutions S1 et S2 qui
transforment une variable x. Alors S2 est un raffinement de S1
si S2 termine lorsque S1 termine et si la relation
entrées-sorties définie par S2 est incluse dans la relation
entrées-sorties de S1, ce qui nous donne les deux conditions :
[S1](x=x) Þ [S2](x=x)
¬([S2](x¹x')) Þ ¬([S1](x¹x'))
Lorsque cette condition est vérifiée, on écrira S1 Í
S2 et on dira
que S1 est raffiné par S2.
On remarque que la seconde condition peut s'écrire de manière équivalente :
[S1](x¹x') Þ [S2](x¹x')
4.3.2 Propriétés du raffinement
La relation de raffinement satisfait des bonnes propriétés, elle est
réflexive, transitive. Elle est monotone par rapport aux opérations de
construction des substitutions.
Exercice
Montrer les propriétés suivantes :
-
S Í S
- si S1 Í S2 et S2 Í S3 alors S1
Í S3
- si S1 Í S2 alors
-
P|S1 Í P|S2
- P==> S1 Í P ==> S2
- S1 Í S1 [] S2
4.4 Raffiner une machine abstraite
Nous nous intéressons à la relation de raffinement entre deux machines
M1 et M2. L'idée est que les deux machines implantent les mêmes
opérations mais en utilisant des variables d'états différentes.
4.4.1 Exemple
On peut se donner une première machine Ens1 qui
a pour variable d'état, un ensemble fini ens
d'entiers et une opération d'ajout d'un entier à cet ensemble.
Un raffinement de cette machine consiste à vouloir représenter cet
ensemble par un tableau, en introduisant un index pour la dernière
case occupée dans le tableau.
La machine Ens1 s'écrit donc :
|
MACHINE Ens1(maxe) |
CONSTRAINTS maxe Î N1 |
VARIABLES ens |
INVARIANT ensÍ N Ù card(ens) £ maxe |
INITIALISATION ens:=Ø |
OPERATIONS |
ajout(n) = |
PRE nÎN-ens
Ù card(ens)<maxe |
THEN ens:=ensÈ{n} END |
END |
|
Une machine effectuant les mêmes tâches que Ens1 mais utilisant un tableau aura
la forme suivante :
|
MACHINE Ens2(maxe) |
CONSTRAINTS maxe Î N1 |
VARIABLES tab, index |
INVARIANT index Î 0..maxe Ù
tabÎ 1..index >-> N |
INITIALISATION index,tab:= 0,Ø |
OPERATIONS |
ajout(n) = |
PRE nÎN-ran(tab)
Ù index<maxe |
THEN index:=index+1 ||
tab(index+1):=n END |
END |
|
On rappelle que la formule tabÎ 1..index >->
N signifie que tab est une injection
(cf A.4.2).
Pour montrer que Ens2 est un raffinement de Ens1 il
faut établir un lien entre les variables d'état des deux machines. Ici
on va demander que l'image de la fonction tab soit égale à
l'ensemble ens.
En pratique, la machine Ens2 va explicitement être introduite
comme un raffinement de Ens1 avec un invariant qui contraint
les variables de Ens2 et qui de plus établit le
lien entre les deux états.
|
REFINEMENT Ens2 |
REFINES Ens1 |
VARIABLES tab, index |
INVARIANT index Î 0..maxe Ù
tabÎ 1..index >-> N
Ù ran(tab)=ens |
INITIALISATION index,tab:=0,Ø |
OPERATIONS |
ajout(n) = |
PRE nÎN-ran(tab)
Ù index<maxe |
THEN index:=index+1 ||
tab(index+1):=n END |
END |
|
La machine raffinée Ens2 récupère les paramètres, ensembles,
constantes contraintes et propriétés de la machine qui est raffinée.
Toutes les variables de la machine Ens1 sont visibles dans
l'invariant de Ens2 mais ne peuvent être utilisées dans les
substitutions.
Les obligations de preuves
Les obligations de preuve doivent établir que l'initialisation et les opérations de
Ens2 préservent l'invariant en ce qui concerne la partie
concernant les variables de Ens2 et que si on fait les
opérations qui se correspondent dans Ens1 et Ens2
alors les résultats obtenus par l'opération Ens2 seront un
cas particulier des résultats attendus dans Ens1.
Pour l'initialisation, on doit assurer que l'initialisation I2 de
Ens2 correspond à un cas particulier d'initialisation I1 de
Ens1 et établit l'invariant de Ens2.
Comme il peut y avoir plus d'initialisation dans Ens1 que
dans Ens2 au lieu d'établir [I2]([I1]Inv2) qui
dirait que toutes les exécutions de I1 établissent Inv2 on
établit qu'il existe une exécution de I1 qui établit
Inv2, ou encore qu'il n'est pas possible que toutes les exécutions de I1
établissent ¬ Inv2.
La condition est donc :
[I2](¬[I1]¬Inv2)
Dans le cas de l'opération ajout on peut supposer qu'elle va
être appelée dans les conditions requises par Ens1 et que de
plus les invariants de Ens1 et Ens2 seront
vérifiés.
Il faut vérifier qu'alors la précondition de ajout dans
Ens2 est vérifiée et que, après l'exécution de la substitution
associée dans Ens2, on peut trouver une exécution de
ajout dans Ens1 qui validera Inv2.
En supposant que ajout
s'écrit PRE P1 THEN S1 END dans
Ens1 et PRE P2 THEN S2 END dans
Ens2, on obtient l'obligation de preuve
Inv1 Ù Inv2 Ù P1 Þ (P2 Ù
[S2](¬ [S1] ¬ Inv2))
4.4.2 Cas général
On suppose que M1 a une variable d'état e1, un
invariant Inv1, une initialisation I1 et contient une
opération op1 de la forme :
y1¬¾op(x1)
= PRE P1 THEN S1 END
Dans l'opération de raffinement, on introduit
une machine M2 avec une nouvelle variable d'état e2 (distincte de e1), un
invariant Inv2, une initialisation I2 et contient une opération
op2 de la forme :
y2¬¾op(x2)
= PRE P2 THEN S2 END
Quitte à renommer les paramètres, on peut toujours supposer qu'ils sont
différents dans les deux opérations.
On veut montrer que le comportement de op2 est un cas
particulier de celui attendu de op1.
On demande que, à chaque état de M2 corresponde au moins un état de
M1.
Invariant combiné
Ceci nous amène à introduire un nouvel invariant portant sur les
variables de M2 :
Invº $ e1. Inv1 Ù
Inv2
Nous allons établir les propriétés portant sur Inv1 et
Inv2 pour
que Inv soit un invariant de la machine M2 et que l'opération
op2 soit un raffinement de op1.
Initialisation
On retrouve la formule :
" e1,e2.[I2](¬[I1]¬Inv2)
Opération
Contrairement au cas précédent, nos opérations ont un paramètre de
sortie, il faut donc établir qu'à entrées égales, la sortie de
op2 est un cas particulier de sortie attendue par
op1 ce qui donne :
" e1,e2.
Inv1 Ù Inv2 Þ (" x1,x2. x1=x2 Ù P1 Þ (P2 Ù
[S2](¬ [S1] ¬ (y1=y2 Ù Inv2))))