Précédent Suivant Index

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

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 xx=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

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 :

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È{nEND
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](¬[I1Inv2)

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](¬[I1Inv2)
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))))


Précédent Suivant Index