Précédent Suivant Index

B   Langage de la méthode B

B.1   Formules

L'anti-restriction consiste à restreindre le domaine d'une relation R au complémentaire d'un ensemble E. Elle se note en E <<| R (E <<| R en notation ASCII).

La surcharge droite d'une relation R par une relation S est une relation dont le domaine est l'union des domaines de R et de S. Elle correspond à S sur le domaine de S et à R sur les éléments du domaine de R qui ne sont pas dans le domaine de S. Elle se note R <+ S et R <+ S en notation ASCII.

  1. Donner une formule équivalente à x |® y Î E <<| R uniquement en terme d'appartenance à E et R.
  2. Donner une formule équivalente à x |® y Î R <+ S uniquement en terme d'appartenance à R et S puis en utilisant l'anti-restriction.

B.2   Objets et formules

On souhaite modéliser un système de gestion de cours. Le système comprend des professeurs, des étudiants, des cours. Chaque cours est enseigné par un seul professeur et peut accueillir un nombre maximum d'étudiants. Il ne peut y avoir plus d'étudiants inscrits dans un cours que le nombre maximal. Chaque étudiant est identifié par un numéro unique.

Décrire dans le langage de B la modélisation de ce problème. On prendra comme ensemble abstraits les ensembles PROFESSEURS, ÉTUDIANTS et COURS qui représentent le type des objets que peut manipuler le système. On introduira en particulier les relations est_suivi_par, est_enseigné_par, a_pour_professeur.

Utiliser prioritairement les notations algébriques de B. On peut introduire des notations pour désigner les sous ensembles des objets apparaissant effectivement dans le système. Dans une modélisation UML, ÉTUDIANTS correspondrait à l'ensemble de tous les objets possibles dans la classe des étudiants; cet ensemble est défini une fois pour toute alors que étudiants correspond à toutes les instances présentes dans le système à un moment donné.
profs Í PROFESSEURS
étudiants Í ÉTUDIANTS
cours Í COURS
max Î cours --> N
no Î etudiants >-> N
est_enseigné_par Î cours +-> profs
est_suivi_par Î étudiants « cours
a_pour_professeur Î étudiants « profs = est_suivi_par ; est_enseigné_par
" c. c Î cours Þ card(est_suivi_par-1[{c}]) £ max(c)

B.3   Substitutions

Expliciter la formule [S]P dans les cas suivants :

B.3.1   Substitutions simples

S P [S]P
x:=1 x¹y  
x:=y x =y  
x:=0 y > 0  
x:=x+1 x > 0  
x:=1 (" x. xÎ N Þ x ³ y) Ú x ³ 0  
y:=x (" x. xÎ N Þ x ³ y)  

B.3.2   Substitutions multiples

S P [S]P
x,y:=1,2 x+y ³ z  
x,y:=0,1 " x. x Î N Þ x ³ y  
x,y:=y,x " x. x Î N Þ x ³ y  

B.3.3   Substitutions généralisées

S P [S]P
x>0 | x:=x-1 x > y  
x Î N | xs:=xs È {x} xs Í N  
   x Î S ==> T:=TÈ{x}
[]  x ÏS ==> S:=SÈ{x}
x Î S Ç T  

B.3.4   Raffinement

On suppose que x et y sont des variables de type N. Soit les substitutions :
S1 º PRE  x¹ 0 THEN y:=y/x END      S2 º IF  x¹ 0 THEN y:=y/x END
  1. Pour une formule P quelconque, calculer [S1]P et [S2]P.
  2. A-t-on S1Í S2, S2Í S1 ?
  3. On introduit maintenant :
    S3 º PRE  x¹ 0 THEN ANY z WHERE z £ y THEN y:=z END END.
    Calculer [S3]P, a-t-on S1Í S3, S3Í S1 ? On a [S1]P = x¹ 0 Ù [y:=y/x]P et [S2]P = x¹ 0 Þ [y:=y/x]P Ù x=0 Þ P On a donc toujours [S1]P Þ [S2]P donc en particulier [S1]y=y Þ [S2]y=y et [S1]y¹y' Þ [S2]y¹y' donc S1 Í S2.

    Par contre [S1]y=y º x¹ 0 Ù y/x = y/x Û x¹0 et [S2]y=y º (x¹0 Þ y/x = y/x) Ù (x=0 Þ y=y) donc [S2]y=y Û true Donc on n'a pas en général [S2]y=y Þ [S1]y=y.

    On a [S3]P = x¹ 0 Ù " z. z < y Þ [y:=z]P On vérifie aisément que x¹ 0 Þ y/x £ y et donc [S3]P Þ [S1]P et donc S1 est un raffinement de S3 et donc S3 Í S1 On a également [S3]y=y º x¹ 0 Ù " z. z < y Þ z=z Û x¹ 0 Û [S1]y=y et [S3]y¹y' º x¹ 0 Ù " z. z < y Þ z¹y' [S1]y¹y' º x¹ 0 Ù y/x ¹y' Comme il est faux que y/x ¹y' implique " z. z < y Þ z¹y', on en déduit que on n'a pas S1 Í S3
Précédent Suivant Index