Précédent Suivant Index

3   Machines abstraites

3.1   Introduction

La notion centrale de la méthode B est la notion de machine abstraite. Afin de modulariser les développements, les programmes sont décomposés en unités qui ont un rôle analogue à celui des objets. Chaque machine déclare ses propres variables et opérations. Les variables ne peuvent être modifiées que par les opérations de la machine.

Dans la méthode B, les machines comportent également des assertions logiques qui permettent de préciser des propriétés qui seront satisfaites par les variables et les opérations. Dans un premier temps les opérations sont spécifiées par leurs propriétés et non par la manière dont elles seront implémentées.

Les machines abstraites sont décrites à partir de substitutions que nous décrivons dans le paragraphe 3.2. Nous décrirons ensuite la structure d'une machine abstraite et les propriétés qui doivent être vérifiées pour assurer que la machine abstraite est bien construite. Finalement, nous indiquons les principales opérations de composition des machines abstraites. Dans les sections suivantes, nous décrirons les opérations de raffinement et d'implantation.

3.2   Les substitutions

Le langage de la méthode B permet de manipuler des programmes, c'est-à-dire des transformations (éventuellement non-déterministes) de la mémoire.

3.2.1   Substitutions de base

Les programmes sont mathématiquement représentés par des substitutions généralisées qui sont définies par leur action sur les prédicats. Une substitution généralisée S est complètement déterminée par la définition de la formule [S]P pour une formule P arbitraire.

Si on interprète S comme un programme alors [S]P représente la plus faible précondition pour que après n'importe quelle exécution de S, la propriété P soit vérifiée.

Les substitutions généralisées sont formées à partir des substitutions élémentaires que nous avons introduites dans le paragraphe 2.3. Les substitutions élémentaires représentent l'affectation dans les programmes.

Dans le tableau suivant qui définit des substitutions généralisées de base, P et Q représentent des formules et S, S1 et S2 des substitutions généralisées.

math ASCII [S]P  
S1;S2 S1;S2 [S1;S2]P Û [S1][S2]P Séquencement
skip skip [skip]P Û P instruction nulle
Q ==> S Q ==> S [Q ==> S]P Û (Q Þ [S]P) Substitution gardée par Q
Q | S Q | S [Q | S]P Û Q Ù [S]P Substitution préconditionnée, assertion de Q
S1[]S2 S1[]S2 [S1[]S2]P Û [S1]P Ù [S2]P Choix non-déterministe
@z.S @z.S [@z.S]P Û " z.[S]P Choix non borné

3.2.2   Q|S versus Q==> S

Il est parfois délicat de comprendre la différence entre les substitutions Q | S et Q ==> S.

La substitution Q | S correspond à affirmer que Q est vrai avant l'exécution de la substitution S. D'un point de vue programme, la propriété Q n'est pas retestée, on fait confiance au programmeur pour n'exécuter la substitution S que lorsque l'état vérifie Q.

La substitution Q ==> S par contre peut être utilisée dans n'importe quel état. D'un point de vue programmation, la propriété Q est d'abord vérifiée avant d'exécuter S.

Supposons que Q soit faux alors on ne peut rien dire sur l'état de la mémoire après l'exécution de Q|S en effet il ne sera jamais possible de valider la plus faible précondition.

Dans le cas de Q ==> S si Q est faux alors on peut montrer (par l'absurde) que [Q ==> S]P est vrai et cela pour tout P donc on peut établir que toute propriété P est vérifiée après l'exécution de ce programme, en particulier la propriété absurde. Cela signifie que le programme correspondant à S n'est jamais exécuté.

3.2.3   Construction de programmes

Des notations sont introduites pour représenter des substitutions correspondant à des programmes usuels.

PRE Q THEN S END Q | S
SELECT Q THEN S END Q ==> S
IF Q THEN S1 ELSE S2 END (Q ==> S1)[] (¬ Q ==> S2)
IF Q THEN S END (Q ==> S)[] (¬ Q ==> skip)
CHOICE S1 OR S2...OR Sn END S1 [] S2 [] ... [] Sn

Exercice
Calculer [IF Q THEN S1 ELSE S2 END]P et [IF Q THEN S END]P.

Choix non borné
Une opération importante sur les substitutions est le choix non borné. Il permet de choisir arbitrairement un objet et sera utile pour spécifier des opérations de création d'objet ou d'initialisation.

VAR x IN S END @ x. S
ANY x WHERE Q THEN S END @ x. (Q ==> S)
x:Î E @ y. (y Î E ==> x:=y)
  n'importe quel objet dans l'ensemble E
x: P @ y. ([x:=y]P ==> x:=y)
  n'importe quel objet qui vérifie P
Restrictions
La substitution VAR ne peut être utilisée dans une machine abstraite de spécification. La variable introduite par ANY ne peut apparaître en partie gauche d'une substitution.

Mise à jour de fonctions
Une fonction est un ensemble de couples de la forme x|® y, où on a au plus une valeur associée à chaque entrée x. Une opération utile est celle de mise à jour. Soit f une variable représentant une fonction, on écrira
f(e1):=e2
pour représenter la substitution f:={x|® y | (x¹ e1 Ù x|® y Î f) Ú (x=e1 Ù y=e2)}

Choix booléen
BOOL est un ensemble prédéfini qui comprend les deux valeurs true et false.

Si P est une formule, la substitution
x:=bool(P)
représente la substitution
IF P THEN x:=true ELSE x:=false END
Cette substitution ne correspond pas forcément à un programme exécutable car rien n'assure que la condition P puisse être calculée par un ordinateur, elle peut être de la forme " n.f(n)=0 avec f une fonction quelconque.

3.2.4   Opérations

Dans la construction des machines abstraites qui forment le coeur du langage B, on sera amené à définir de nouvelles substitutions généralisées et à leur donner des noms, ce sont les opérations. Ces opérations peuvent être paramétriques c'est-à-dire dépendre de variables. En général on distingue dans un programme les variables correspondant aux entrées que l'on instancie au moment de l'appel de celles correspondant aux sorties dans lesquelles on récupère les résultats. Les opérations correspondent aux procédures et fonctions des langages de programmation.

Si S est une substitution généralisée et var, var1 et var2 des listes de variables alors une opération opn du langage B est introduite par une des déclarations suivantes :
  1. routines : opn = S
  2. procédures : opn(var) = S
  3. fonction sans paramètre : var ¬¾ opn = S
  4. fonction avec paramètres : var1 ¬¾ opn(var2) = S
On pourra ensuite utiliser opn à la place de S dans de nouvelles substitutions. L'appel se fera de manière correspondante à la définition :
  1. opn est équivalent à S
  2. opn(e1,...,en) est équivalent à S dans laquelle les variables de var ont été remplacées par (e1,...,en)
  3. var' ¬¾ opn est équivalent à S dans laquelle les variables de var ont été remplacées par les variables de var'.
  4. var ¬¾ opn(e1,...,en) est équivalent à S dans laquelle les variables de var1 ont été remplacées par les variables de var et les variables var2 ont été remplacées par (e1,...,en)
Exemple
On peut par exemple définir une opération moyenne qui calcule dans la variable m la moyenne des variables a et b. Cette opération correspond à la substitution simple :
m:=(a+b)/2
Il est commode de la voir comme une opération prenant comme entrée a et b et ayant comme sortie m. On écrira donc :
m ¬¾ moyenne(a,b) = m:=(a+b)/2
On pourra ensuite définir la moyenne de 4 nombres en utilisant cette opération :
m ¬¾ moyenne4(a,b,c,d)  =
VAR  tmp  IN
tmp ¬¾ moyenne(a,b);
m ¬¾ moyenne(c,d);
m ¬¾ moyenne(tmp,m);
END

3.3   Structure d'une machine abstraite

Une machine abstraite est un programme composé d'une suite de déclarations de différentes natures (constantes, variables, opérations ...).

3.3.1   Machine de base

La machine de base est formée d'un nom, un ensemble de variables, un invariant portant sur les variables de la machine, une initialisation de ces variables ainsi que des opérations.

Une machine élémentaire est déclarée de la manière suivante :
MACHINE  nom nom de la machine
VARIABLES x1,...,xn noms des variables
INVARIANT  I propriété
INITIALISATION  S0 substitution
OPERATIONS substitutions
  var1 ¬¾ nom_de_l'opération(var2)  =  S;  
·
·
·		  
END  

Exemple : notion de point
MACHINE  point
VARIABLES  x,y
INVARIANT  xÎ 0..1024 Ù y Î 0..768
INITIALISATION  x,y:=0,0
OPERATIONS  
v ¬¾ abs  =  v:=x;
v ¬¾ ord  =  v:=y;
move(dx,dy) =
     PRE  x+dx £ 1024 Ù y+dy £ 768
     THEN (x,y):=(x+dx,y+dy)
     END
END

Conditions
Une machine abstraite doit suivre certaines contraintes. Dans le cas de notre exemple il faudrait vérifier :
Opérations spécifiées
Il n'est pas nécessaire d'implanter complètement une opération, les machines servent alors à décrire des spécifications, c'est-à-dire ce que fait l'opération en évitant de décrire comment l'opération le fait. On peut par exemple vouloir implanter une opération qui étant donné un ensemble fini de points nous renvoie l'abscisse la plus petite.

px ¬¾ pp_abs(E) =
PRE EÎ P(0..1024 × 0..768) Ù E ¹Ø
THEN  ANY x WHERE  $ y. (x,y)Î E Ù " (x',y'). (x',y')Î EÞ x£ x'
         THEN px:=x END
END

3.3.2   Ensembles et constantes

Ensembles
Les modélisations manipulent souvent des ensembles qui restent non spécifiés jusqu'à la phase d'implantation. Par exemple pour modéliser une base de données, on introduira l'univers global des objets dans la base qui est un ensemble fini, on pourra piocher dans cet ensemble pour ajouter de nouveaux objets. Une variable de la machine abstraite décrit le sous-ensemble de cet univers qui correspond à l'état courant de la base.

Il est également utile de pouvoir introduire de nouveaux ensemble finis par extension en énumérant les objets de cet ensemble.

Les ensembles ainsi introduits sont toujours finis et non vide et on convient de les identifier par des noms en majuscule. Les objets introduits dans l'énumération d'un ensemble sont tous distincts.

Cette déclaration se fait de la manière suivante :
SETS
ENSEMBLE_ABSTRAIT;
ENSEMBLE_EN_EXTENSION={a1,...,an}
Constantes
Il est utile également d'introduire des constantes correspondant à des valeurs particulières qui restent "symboliques" jusqu'à l'implantation. C'est le cas par exemple de la taille des ensembles introduits. La déclaration de constantes se fait de la manière suivante :
CONSTANTS
c1,...,cn
Propriétés
Si les valeurs des constantes et ensembles ainsi introduits ne seront précisées qu'au moment de l'implantation (ils correspondront à des constantes du programme à exécuter), il peut être utile d'exprimer des contraintes sur ces objets. C'est le rôle de la déclaration PROPERTIES des machines abstraites. Cette déclaration introduit une formule portant sur les constantes et ensembles déclarés qui est supposée être vérifiée.

Exemple
MACHINE Mariages
SETS
  PERSONNES;
  STATUT={marié,célibataire};
  SEXE={homme,femme}
CONSTANTS  max_pers
PROPERTIES
  max_persÎ N-{0} Ù card(PERSONNES)=max_pers
VARIABLES
  personnes, sexe, statut
INVARIANT
  personnesÍ PERSONNES
  Ù sexeÎ personnes --> SEXE
  Ù statutÎ personnes --> STATUT
La machine sera complétée par une substitution d'initialisation. On peut choisir d'initialiser les ensembles en prenant l'ensemble vide pour les personnes et les fonctions.
INITIALISATION
  personnes,sexe,statut:=Ø,Ø,Ø
Si on voulait spécifier qu'initialement personnes est un ensemble quelconque de femmes célibataires, on écrirait :
INITIALISATION
  personnes:Î P(PERSONNES)
  || sexe:=personnes × {femme}
  || statut:=personnes × {célibataire}

On peut également ajouter une opération de création :
OPERATIONS
  ajout(s,m)  = 
      PRE sÎSEXE Ù m Î STATUT Ù PERSONNES - personnes ¹Ø
      THEN
          ANY x WHERE x Î PERSONNES-personnes
          THEN personnes:=personnesÈ{x} || sexe(x):=s || statut(x):=m
          END
      END
Exercice
Spécifier une opération de mariage.

3.3.3   Machine paramétrée

Il est possible de paramétrer une machine abstraite. Les paramètres jouent un rôle analogue à celui des constantes et ensembles. Ces paramètres représentent d'ailleurs des ensembles finis non vides de valeurs numériques ou des valeurs numériques.

La machine paramétrée pourra être utilisée avec différentes instances pour les paramètres.

Les conditions sur les paramètres sont exprimées dans un champ appelé CONSTRAINTS par une formule ne portant que sur les paramètres de la machine.

Exemple
Nous décrivons une machine abstraite pour spécifier des tableaux.

MACHINE  Array(INDEX,VAL)
VARIABLES  table
INVARIANT  table Î INDEX --> VAL
INITIALISATION  table:ÎINDEX --> VAL
OPERATIONS 
  enter(i,v) =
      PRE  i Î INDEX Ù v Î VAL
      THEN  table(i):=v
      END;
  v ¬¾ access(i) =
      PRE  i Î INDEX
      THEN  v:=table(i)
      END;
  i ¬¾ search(v) =
      PRE  v Î ran(table)
      THEN  i:Î table-1[{v}]
      END;
  b ¬¾ test(v) =
      PRE  v Î VAL
      THEN  b:=bool(v Î ran(table))
      END;

3.3.4   Autres champs

Les machines abstraites peuvent contenir d'autres champs tels que DEFINITIONS qui permet d'introduire des abréviations améliorant la lisibilité ou ASSERTIONS qui permet d'énoncer des propriétés qui sont toujours vérifiées par la machine car conséquences de l'invariant.

3.4   Combiner des machines abstraites

Plusieurs opérations permettent de combiner des machines entre elles. La déclaration d'une machine M peut contenir une ou plusieurs des déclarations d'inclusion suivante INCLUDES, IMPORTS, USES, SEES, PROMOTES, EXTENDS.

3.4.1   Substitution multiple généralisée

On a déjà utilisé la notation x1:=e1 || x2:=e2 comme abbréviation pour la substitution multiple x1,x2 := e1,e2. Cette notation peut s'étendre pour combiner deux substitutions généralisées S1 || S2 portant sur des variables distinctes.

3.4.2   INCLUDES

INCLUDES prend en argument une liste de machines M1,...,Mk. Si la machine M inclut une machine M'(X,x) paramétrée par un ensemble X et un scalaire x, alors les paramètres seront instanciés dans la clause d'inclusion, on écrira donc INCLUDES  Mi(P,p) où P et p sont respectivement un ensemble et un scalaire de la machine M.

Les ensembles, constantes et variables incluses deviennent des ensembles, constantes et variables de la machine M. Les variables de la machine incluse Mi ne peuvent être modifiées que par les opérations de la machine Mi.

Si certaines opérations op1,...,opn de la machine incluse doivent devenir des opérations de M alors on utilisera la déclaration PROMOTES op1,...,opn. On peut également utiliser EXTENDS au lieu de INCLUDES, dans ce cas toutes les opérations des machines incluses deviennent des opérations de la machine M. On implante ainsi l'analogue de l'héritage entre des classes.

Le fait d'utiliser une clause INCLUDES demande de vérifier des obligations de preuve. Si la machine M inclut une machine M'(P,p), la condition principale à vérifier est que l'instanciation a de la machine incluse satisfait bien les contraintes indiquées dans M'. Cette instanciation peut se faire à l'aide des paramètres, constantes et ensembles de M.

L'opération d'initialisation de la machine M est composée de l'initialisation de M' exécutée conjointement à la déclaration d'initialisation indiquée dans M. Pour montrer que l'initialisation et les opérations de M préservent l'invariant de M, on peut utiliser le fait que l'initialisation et les opérations de M' préservent l'invariant de M'.

Lorsque deux machines M1 et M2 sont incluses dans une même machine M alors les variables de M1 et M2 doivent être différentes (de manière à éviter de casser les invariants de chaque machine). Au besoin, on utilisera une opération de renommage sur les variables et opérations des machines incluses.

La commande d'inclusion est une facilité d'écriture, il serait possible d'expanser les déclarations des machines incluses dans la machine principale.

Exemple
On aurait pu découper notre machine Mariages en deux en introduisant tout d'abord une machine Personnes ne contenant que les personnes et leur sexe :

MACHINE Personnes
SETS
  PERSONNES;
  SEXE={homme,femme}
CONSTANTS  max_pers
PROPERTIES
  max_persÎ N-{0} Ù card(PERSONNES)=max_pers
VARIABLES  personnes, sexe
INVARIANT
  personnesÍ PERSONNES   Ù sexeÎ personnes --> SEXE
INITIALISATION   personnes,sexe:=Ø,Ø
L'opération de création d'une personne prend en argument la personne créée :
OPERATIONS
  ajout_personne(x,s)  = 
      PRE sÎSEXE Ù x Î PERSONNES - personnes
      THEN personnes:=personnesÈ{x} || sexe(x):=s
      END
On peut alors construire la machine des mariages au-dessus de la machine des personnes :
MACHINE Mariages
SETS   STATUT={marié,célibataire};
INCLUDES Personnes
VARIABLES   statut
INVARIANT   statutÎ personnes --> STATUT
INITIALISATION   statut:=Ø
Pour implanter l'opération de création, on va utiliser l'opération ajout_personne de la machine Personnes.
OPERATIONS
ajout(s,m)  = 
      PRE sÎSEXE Ù m Î STATUT Ù PERSONNES - personnes ¹Ø
      THEN
         ANY x WHERE x Î PERSONNES - personnes
         THEN ajout_personne(x,s) || statut(x):=m END
      END 

3.4.3   USES

USES prend en argument une liste de noms de machines M1,...,Mk. Les variables, paramètres, constantes et ensembles des machines utilisées sont visibles dans la machine M, peuvent être utilisés dans les invariants, substitutions de M. Cependant la machine M ne peut voir les opérations des machines de la clause USES et ne peut en modifier les variables. Les éventuels paramètres des machines Mi ne sont pas instanciés dans M et doivent être distincts de ceux de M.

L'idée est que dans le futur, une machine N sera construite qui incluera la machine M et toutes les machines des clauses USES de M. La vérification de la cohérence globale du système sera faite dans la machine N.

La déclaration USES sert à partager des informations statiques entre deux machines incluses dans une troisième.

Exemple
En reprenant notre exemple de mariage, une alternative serait de construire une machine Statut qui utilise la machine Personnes et implante le statut, une opération de mise-à-jour du statut est introduite. Il n'est pas possible dans la machine Statut de maintenir l'invariant que statut est une fonction totale sur personnes, en effet la mise à jour du statut se fait indépendemment des modifications apportées à la variable personnes. On se contente donc de déclarer statut comme une fonction partielle de l'ensemble PERSONNES dans STATUT.

La machine Mariage est alors construite dans un troisième temps par inclusion des machines Personnes et Statut, cette machine peut déclarer l'opération d'ajout et contraindre la fonction statut à être totale sur personnes :

MACHINE Statut
SETS
  STATUT={marié,célibataire}
USES Personnes
VARIABLES   statut
INVARIANT   statutÎ PERSONNES +-> STATUT
INITIALISATION   statut:=Ø
OPERATIONS
  set_statut(x,m)  = 
      PRE m Î STATUT Ù x Î PERSONNES THEN statut(x):=m END
END
La machine Mariages est alors construite de la manière suivante :
 
MACHINE Mariages
INCLUDES
  Personnes,Statut
INVARIANT
  dom(statut)=personnes
OPERATIONS
ajout(s,m)  = 
      PRE sÎSEXE Ù m Î STATUT Ù PERSONNES - personnes ¹Ø
      THEN  ANY x WHERE xÎ PERSONNES - personnes
              THEN ajout_personne(x,s) || set_statut(x,m) END 
      END 
END
 

3.4.4   SEES

SEES prend en argument une liste de noms de machines M1,...,Mk. Les constantes, ensembles, variables, et les opérations ne modifiant pas les variables des machines apparaissant dans la clause SEES sont visibles dans la machine M. Cependant les variables des machines vues sont complètement cachées et ne peuvent être utilisée dans l'invariant de M, elles sont par contre accessibles en lecture dans les opérations de M. Lorsqu'une machine M a une clause SEES M', alors c'est que l'implantation de M comportera en particulier une instance de M'.

Précédent Suivant Index