Le processus de raffinement
❑ Idée :
❑ Spécification : ce que fait le logiciel (Le quoi?)
❑ Programme : comment fait le logiciel (Le comment?)
❑ Raffinement : passage du quoi au comment
❑ Implémentation : raffinement traduisible en un programme Ada, C, C++,
etc ...
❑ Définition :
❑ Une technique de transformation du modèle abstrait d’un logiciel (la
spécification) en un modèle plus concret (le raffinement) mais ayant le
même comportement observable
❑ Notation :
❑ M2 raffine M1 est notée M1 ⊆ M2
Le processus de raffinement
Machine abstraite M
Raffinement Preuve du raffinement
Raffinement 1: M1 Preuve PR1
Raffinement 2: M2 Preuve PR2
… … 3éme…ième raffinement
Raffinement n-1: Mn-1
Raffinement n: Mn
⇒ l’implémentation
est le dernier
raffinement de la
Implémentation
machine abstraite PA: propriété abstraite
PR: propriété de raffinement remplaçant PA
Le processus de raffinement
❑ Le modèle plus concret :
❑ contient plus de détails sur la spécification
❑ est plus proche d’une implantation
❑ réduit l’indéterminisme
❑ Construction progressive d’une implémentation à partir d’un
modèle abstrait
❑ Modèle abstrait → raffinement 1→ ... → Implémentation
❑ Obligations de preuve à chaque étape :
❑ Prouver que le raffinement est correct
❑ Raffinement i+1 préserve le comportement du Raffinement i
Le processus de raffinement
❑ MACHINE:
❑ décrit un comportement de manière abstraite par son état et ses
opérations;
❑ REFINEMENT (raffinement)
❑ est une étape du développement d’une machine; détaille la
structure et les opérations de la machine.
❑ IMPLEMENTATION:
❑ le dernier maillon du développement d’une machine, le plus
proche du codage.
❑ Le dernier raffinement pouvant utiliser des composants logiciels
existants (ou développés indépendamment).
Le processus de raffinement
❏ Lors d'un raffinement,
❏ Une machine M est remplacée par une autre machine M1 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.
❏ 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 op1 est un raffinement d'une opération op alors
toute utilisation de op doit pouvoir être remplacée par une
utilisation de op, sans casser le fonctionnement du
programme.
Le processus de raffinement
Raffinement
Syntaxe: REFINEMENT Implémentation :
Machine abstraite MM_R1
dernier raffinement
MACHINE REFINES
MM MM
SETS SETS
C D
VARIABLES VARIABLES
a b IMPLEMENTATION
INVARIANT INVARIANT MM_I1
I J REFINES
INITIALIZATION INITIALIZATION MM_R1
INIT INITR ...
OPERATIONS OPERATIONS END
u 🡨 nomO (w)= PRE Q u 🡨 nomO (w)= PRE QR
THEN V THEN VR
END END
… …
END END
Le processus de raffinement
Raffinement
Syntaxe:
REFINEMENT
Machine abstraite MM_R1
MACHINE REFINES
MM MM
SETS ● Les ensembles abstraits
SETS
C C sont implicitement
D
VARIABLES présents dans MM_R1
VARIABLES
a b
INVARIANT INVARIANT
I J
INITIALIZATION INITIALIZATION
INIT INITR
OPERATIONS OPERATIONS
u 🡨 nomO (w)= PRE Q u 🡨 nomO (w)= PRE QR
THEN V THEN VR
END END
… …
END END
Le processus de raffinement
Raffinement
Syntaxe:
REFINEMENT
Machine abstraite MM_R1
MACHINE REFINES
MM ● Les variables abstraites a MM
SETS sont raffinées par les SETS
C variables concrètes b D
VARIABLES VARIABLES
● Les variables concrètes
a b
b contiennent :
INVARIANT INVARIANT
I ○ les variables J
INITIALIZATION abstraites INITIALIZATION
INIT conservées par le INITR
OPERATIONS raffinement OPERATIONS
u 🡨 nomO (w)= PRE Q ○ des variables u 🡨 nomO (w)= PRE QR
THEN V concrètes THEN VR
END introduites par le END
… raffinement …
END END
Le processus de raffinement
Raffinement
Syntaxe:
REFINEMENT
Machine abstraite MM_R1
MACHINE ● L’invariant de collage J REFINES
MM permet de : MM
SETS ○ typer les variables SETS
C concrètes introduites D
VARIABLES par le raffinement VARIABLES
a ○ exprimer des b
INVARIANT propriétés sur les INVARIANT
I variables concrètes J
INITIALIZATION ○ exprimer la relation INITIALIZATION
INIT reliant les variables INITR
OPERATIONS concrètes aux OPERATIONS
u 🡨 nomO (w)= PRE Q variables abstraites u 🡨 nomO (w)= PRE QR
THEN V (d’où le nom d’invariant THEN VR
END de collage ou de END
… liaison) …
END END
Le processus de raffinement
Raffinement
Syntaxe:
REFINEMENT
Machine abstraite MM_R1
MACHINE REFINES
MM MM
SETS SETS
C D
VARIABLES VARIABLES
a ● L’initialisation concrète b
INVARIANT INITR est un raffinement INVARIANT
I de INIT J
INITIALIZATION INITIALIZATION
INIT INITR
OPERATIONS OPERATIONS
u 🡨 nomO (w)= PRE Q u 🡨 nomO (w)= PRE QR
THEN V THEN VR
END END
… …
END END
Le processus de raffinement
Raffinement
Syntaxe:
REFINEMENT
Machine abstraite MM_R1
MACHINE REFINES
MM MM
SETS SETS
C ● L’opération abstraite D
VARIABLES nomO est raffinée par VARIABLES
a une opération concrète de b
INVARIANT même signature INVARIANT
I J
INITIALIZATION ○ La substitution
INITIALIZATION
INIT concrète VR raffine
INITR
OPERATIONS la substitution V en
OPERATIONS
u 🡨 nomO (w)= PRE Q affaiblissant la
u 🡨 nomO (w)= PRE QR
THEN V précondition Q par
THEN VR
END QR et en réduisant
END
… l’indéterminisme
…
END END
Le processus de raffinement
❑ Raffinement des données
❑ Raffinement de contrôle
❑ Raffinement algorithmique
Le processus de raffinement
❑ Raffinement des données
❑ Choix de l’implantation :
❑ Introduction de variables et d’ensembles concrets
❑ Définition des opérations sur l’implantation :
❑ Réécriture des opérations en utilisant les variables concrètes
❑ Toute opération spécifiée dans la machine abstraite doit être raffinée
avec la même signature dans l’implantation (ou le raffinement)
❑ Définition d’une relation d’abstraction entre l’espace d’état concret
et l’espace d’état abstrait
🡨 l’invariant de collage ou de liaison
Le processus de raffinement
Le processus de raffinement
Le processus de raffinement
Le processus de raffinement
❑ Exemple 1: Remplacer les variables abstraites par des variables concrètes
MACHINE Team
REFINEMENT TeamR
SETS ANSWER = {in, out}
REFINES Team
VARIABLES team
VARIABLES teamr
INVARIANT team <: 0..21 & card(team) = 11
INVARIANT teamr : 0..10 >-> 0..21
INITIALISATION team := 0..10
& ran(teamr) = team
OPERATIONS
INITIALISATION
substitute(pp,rr) =
teamr := % nn . (nn : 0..10 | nn)
PRE
OPERATIONS
pp : team & rr : 0..21 & rr /: team
substitute(pp , rr) =
THEN team := (team \/ {rr}) - {pp}
teamr(teamr~(pp)) := rr;
END;
aa <-- query(pp) =
aa <-- query(pp) =
IF pp : ran(teamr)
PRE pp : 0..21
THEN aa := in
THEN IF pp : team
ELSE aa := out
THEN aa := in
END
ELSE aa := out
END
END
END END
Le processus de raffinement
❑ Exemple 2:Remplacer les variables abstraites par des tableaux
MACHINE Team REFINEMENT TeamR2
SETS ANSWER = {in, out} REFINES Team
VARIABLES team VARIABLES teama
INVARIANT team <: 0..21 & card(team) = 11 INVARIANT teama : 0..21 -->ANSWER
INITIALISATION team := 0..10 & team = dom(teama |> {in})
OPERATIONS INITIALISATION
substitute(pp,rr) = teama := (0..10)*{in} \/ (11..21)*{out}
PRE OPERATIONS
pp : team & rr : 0..21 & rr /: team substitute(pp , rr) =
THEN team := (team \/ {rr}) - {pp} BEGIN
END; teama (pp):= out; teama (rr):=in
aa <-- query(pp) = END;
PRE pp : 0..21 aa <-- query(pp) =
THEN IF pp : team aa:=teama(pp)
THEN aa := in END
ELSE aa := out
END
Le processus de raffinement
❑ Exemple 3: Remplacer les variables abstraites par des tableaux de booléens
MACHINE Team REFINEMENT TeamR3
SETS ANSWER = {in, out} REFINES Team
VARIABLES team VARIABLES teamb
INVARIANT team <: 0..21 & card(team) = 11 INVARIANT teamb : 0..21 -->BOOL
INITIALISATION team := 0..10 & team = dom(teamb |> {TRUE})
OPERATIONS INITIALISATION
substitute(pp,rr) = teamb := (0..10)*{TRUE} \/ (11..21)*{FALSE}
PRE OPERATIONS
pp : team & rr : 0..21 & rr /: team substitute(pp , rr) =
THEN team := (team \/ {rr}) - {pp} BEGIN
END; teamb (pp):= FALSE; teamb (rr):=TRUE
aa <-- query(pp) = END;
PRE pp : 0..21 aa <-- query(pp) =
THEN IF pp : team VAR bb IN /*introduction de variable locale*/
THEN aa := in bb := teamb(pp);
ELSE aa := out IF bb = TRUE
END THEN aa := in
ELSE aa := out END END END
Le processus de raffinement
❑ Raffinement de contrôle:
❑ Les opérations conservent la même signature
❑ Affaiblissement des préconditions jusqu’à les faire disparaître
❑ qui peut le plus, peut le moins
❑ EtatsPre(V) ⊆ EtatsPre(VR)
❑ Réduction de l’indéterminisme :
❑ choix de solutions ou d’options
❑ PrePost(VR) ⊆ PrePost(V)
❑ PrePost(X) représente l’ensemble des couples d’états Pre et Post
possibles d’une substitution X
❑ Dans une implémentation, PrePost(X) doit être une fonction (au plus un
état final)
Le processus de raffinement
❑ Raffinement de contrôle:
❑ VR peut être utilisé à la place de V sans que l’utilisateur de la machine
puisse s’en rendre compte.
❑ Pour cela, il faut que la précondition de VR soit plus faible que celle de V, VR
soit plus déterministe que V, ce qui revient à renforcer la post-condition
❑ Exemple:
○ V est raffiné par VR ?
V= x>5 | (x:=0 [] x:=x-1)
VR = x>0 | x:=x-1
🡨 VR remplit les mêmes services que V en tout point d’exécution prévu par V
EtatsPre(V)={6,7,8…} ⊆ EtatsPre(VR)={1,2,3…}
PrePost(VR)={(x,x’)∈ZxZ|x’=x-1} ⊆ PrePost(V)={(0,0)}∪{(x,x’)
∈ZxZ|x’=x-1}
Le processus de raffinement
❑ Réduction de l’indéterminisme: Exemple 1
❑ Une substitution V raffine une substitution VR (notée V ⊆ VR) 🡨 il faut VR soit plus
déterministe que V.
MACHINE MaisonAbstraite
SETS REFINEMENT MaisonRaff
TYPE _TOIT = {ardoises, tuiles} REFINES MaisonAbstraite
VARIABLES VARIABLES
toit letoit
INVARIANT INVARIANT
toit ϵ TYPE_TOIT letoit = toit
INITIALISATION INITIALISATION
toit :: TYPE_TOIT letoit := ardoises
OPERATIONS OPERATIONS
Choix_toit = Choix_toit =
CHOICE toit := ardoises letoit := tuiles
OR toit := tuiles END
END
END
Le processus de raffinement
❑ Raffinement algorithmique:
❑ Expliciter les algorithmes
❑ Utilisation de structures de contrôle des langages de programmation
❑ séquence à la place des substitutions simultanées: S;T
Le processus de raffinement
❑ Raffinement algorithmique:
❑ Expliciter les algorithmes
❑ Utilisation de structures de contrôle des langages de programmation
❑ séquence à la place des substitutions simultanées: S;T
❑ itération WHILE (implémentation): w(P, S, I, V)
Le processus de raffinement
❑ Les obligations de preuve du raffinement:
❑ Un raffinement est correct ssi l’effet de la spécification concrète ne
contredit pas l’effet de la spécification abstraite OU
❑ Un raffinement est correct ssi à chaque effet de la spécification concrète
correspond un effet de la spécification abstraite
❑ Il faut vérifier cette définition pour :
❑ 1/ l’initialisation
❑ 2/ chaque opération de la spécification abstraite
Le processus de raffinement
❑ Les obligations de preuve du raffinement:
REFINEMENT
MACHINE MM_R1
1/Pour l’initialisation:
MM REFINES
🡨 Le but à démontrer est :
SETS MM L’initialisation de MM _R1 doit
C SETS établir qu’il est impossible que
VARIABLES D l’initialisation de MM établisse
a VARIABLES la négation du changement de
INVARIANT b variable:
I INVARIANT
INITIALIZATION J [INITR] ¬ [INIT] ¬ J
INIT INITIALIZATION
🡨 INITR est correcte
OPERATIONS INITR
lorsqu’elle établit J sans
u 🡨 nomO (w)= PRE Q OPERATIONS contredire INIT
THEN V u 🡨 nomO (w)= PRE QR
END THEN VR
… END
END …
END
Le processus de raffinement
❑ Les obligations de preuve du raffinement:
MACHINE EX1 REFINEMENT EX2
VARIABLES
y REFINES EX1
INVARIANT VARIABLES
y ∈ F(NAT1) z
INITIALISATION INVARIANT
y := Φ [INITR] ¬ [INIT] ¬ J
OPERATIONS z = max (y ∪ {0})
entrer (n) = INITIALISATION
PRE n ∈ NAT1 z := 0 Exemple:
THEN 1. [z := 0] ¬ [ y := ∅] ¬ (z = max (y ∪
OPERATIONS
y := y ∪ {n} {0}))
entrer (n) = ⬄
END ; PRE n ∈ NAT1 2. [z := 0] ( z = max (∅ ∪ {0}))
m ‹ — maxi THEN ⬄
PRE y ≠ Φ z := max ({z, n}) 3. 0 = 0
THEN END ;
m := max (y)
END ; m ‹ — maxi =
END PRE z ≠ 0
THEN
m := z
END ;
END
Le processus de raffinement
❑ Les obligations de preuve du raffinement:
REFINEMENT 2/Pour chaque opération:
MACHINE MM_R1
MM REFINES Invariant de la spécification I
SETS MM ∧
C SETS Invariant du raffinement J
VARIABLES D ∧
a VARIABLES Pré-condition de la spécification
INVARIANT b Q
I INVARIANT ∧
INITIALIZATION ⇒
J
Pré-condition du raffinement QR
INIT INITIALIZATION
OPERATIONS
∧
INITR [Action du raffinement VR]
u 🡨 nomO (w)= PRE Q OPERATIONS ¬ [Action de la spécification V]
THEN V u 🡨 nomO (w)= PRE QR ¬ Changement de variable du
END THEN VR raffinement J
… END
END … I ∧J∧Q => QR∧[VR]¬[V]
END
Le processus de raffinement
❑ Les obligations de preuve du raffinement:
❑ Si :
❑ les valeurs des variables des deux composants (abstrait et raffiné) avant
l’opération respectent les invariants I et J
❑ Et si :
❑ on est dans les conditions Q d’exécution de l’opération abstraite
❑ Alors :
❑ On doit être dans les conditions QR d’exécution de l’opération raffinée
❑ Quelque soit les nouvelles valeurs prises par les variables parmi celles
définies par la substitution VR de la machine raffinée, elles doivent
correspondre par la transformation J à l’une des valeurs définies par la
substitution S de la machine abstraite
I ∧J∧ Q => QR∧[VR]¬[V]¬J
Le processus de raffinement
❑ Les obligations de preuve du raffinement: Exemple obligation de
preuve de raffinement de l’opération entrer (n)
1. y ∈ F(NAT1) ∧ z = max (y ∪ {0}) ∧ n ∈ NAT1
⇒ n ∈ NAT1 ∧ [z := max ({z, n})] ¬ [y := y ∪ {n}] ¬ (z = max (y ∪ {0}))
⬄
2. y ∈ F(NAT1) ∧ z = max (y ∪ {0}) ∧ n ∈ NAT1
⇒ n ∈ NAT1 ∧ [z := max ({z, n})] (z = max (y ∪ {n} ∪ {0}))
⬄
3. y ∈ F(NAT1) ∧ z = max (y ∪ {0}) ∧ n ∈ NAT1
⇒ n ∈ NAT1 ∧ (max ({z, n}) = max (y ∪ {n} ∪ {0})).
⬄
4. y ∈ F(NAT1) ∧ z = max (y ∪ {0}) ∧ n ∈ NAT1
⇒ n ∈ NAT1 ∧ (max ({z, n}) = max ({max(y), n})
⬄
5. y ∈ F(NAT1) ∧ z = max (y ∪ {0}) ∧ n ∈ NAT1
⇒ n ∈ NAT1 ∧(max ({max(y∪ {0}), n}) = max ({max(y), n})
Le processus de raffinement
❑ Les obligations de preuve du raffinement: Exemple obligation de
preuve de raffinement de m 🡨 maxi
I ∧ J∧ Q => Q R ∧ [[m := m']VR] ¬ [V] ¬ (J ∧ m = m')
1. y ∈ F(NAT1) ∧ z = max (y ∪ {0}) ∧ y ≠ Φ
⇒
z ≠ 0 ∧ [m' := z] ¬ [m := max (y)] ¬ (z = max (y ∪ {0}) ∧ m =m')
⬄
2. y ∈ F(NAT1) ∧ z = max (y ∪ {0}) ∧ y ≠ Φ
⇒
z ≠ 0 ∧ [m' := z] (z = max (y ∪ {0}) ∧ max (y) = m')
⬄
3. y ∈ F(NAT1) ∧ z = max (y ∪ {0}) ∧ y ≠ Φ
⇒
z ≠ 0 ∧ (z = max (y ∪ {0}) ∧ max (y) = z)
Le processus de raffinement
❑ Les obligations de preuve du raffinement: Exercice d’application
MACHINE OP1
VARIABLES Calculer l’obligation de preuve de l’initialisation du raffinement?
v1 La contraposée de l'invariant est :
INVARIANT v2 ≠ 2 * v1
v1∈ 0..10
INITIALISATION L'initialisation du composant raffiné, appliquée a ce prédicat:
ANY valeur WHERE [ANY valeur WHERE valeur ∈ 1..5 THEN v1:=valeur END] (v2≠ 2*v1)
valeur ∈ 1..5
THEN v1 := valeur Ce qui devient, par définition de la substitution ANY :
END ∀ valeur (valeur ∈ 1..5 ⇒ v2 ≠ 2 * valeur)
END
La contraposée de ce dernier prédicat est:
REFINEMENT OP1_1
∃ valeur (valeur ∈ 1..5 ∧ v2 = 2 * valeur)
REFINES OP1
VARIABLES
L'application de l'initialisation du raffinement nous permet d'instancier v2 par 2, nous
v2
obtenons alors:
INVARIANT
∃ valeur (valeur ∈ 1..5 ∧ 2 = 2 * valeur)
v2 = 2 * v1
qui est vrai
INITIALISATION
v2 := 2
END