Méthode B/Première machine abstraite

Un livre de Wikilivres.
Sauter à la navigation Sauter à la recherche

Cette machine est écrite en notation B Ascii. Il existe aussi une « notation mathématiques », fournie plus loin, qui utilise les symboles usuels de la mathématique ensembliste et de la logique des prédicats.

 MACHINE
  reservation (max_siege)

/* Le nom de la machine est réservation. On lui passe en paramètre la variable max_sieges. */

 CONSTRAINTS
 max_sieges : NAT

/* Prédicat d'appartenance. max_sieges appartient à l'ensemble des nombres naturels implantables */

 VARIABLES
 nb_sieges_dispos

/* nb_sieges_dispos est une variable. On va apprendre dans la rubrique INVARIANT quel est son type. */

 INVARIANT
 nb_sieges_dispos : 0..max_sieges
 

/* L'invariant est un prédicat qui doit respecter l'état de la machine. On apprend ici que nb_sieges_dispos est un élément (: est la notation ascii pour l'appartenance ensembliste) de l'ensemble qui va de 0 à max_sieges, max_sieges ayant été passé en paramètre à la machine. nb_sieges_dispos est donc un nombre entier. C'est le nombre de sièges disponibles. On le comprendra avec l'opération réserver.*/

INITIALISATION
 nb_sieges_dispos := max_siege
 

/* La rubrique INITIALISATION permet de vérifier que la spécification a au moins un modèle, une instanciation qui satisfait l'invariant L'opérateur := se lit devient égal à. Il s'agit de la spécification d'une opération. Il s'agit également d'une substitution simple. Cette opération, lorsqu'elle est appliquée au prédicat qui représente la contrainte que l'état de la machine doit respecter, modélise la transformation de la mémoire opérée par l'initialisation : [ nb_sieges_dispos := max_sieges] (siege : 0..max_sieges) <=> max_siege : 0..max_sieges et produit le prédicat qui représente la condition minimale que l'état doit vérifier avant l'exécution de l'opération pour que, après l'exécution, les propriétés de l'état soient toujours vérifiées. [ nb_sieges_dispos := max_sieges] (nb_sieges_dispos : 0..max_sieges) se lit : « nb_sieges_dispos devient égal à max_sieges établit que nb_sieges_dispos : 0.. max_sieges. » Plus généralement, si I désigne un prédicat qui doit être respecté par l'état de la machine et si x := E modélise une des opérations de la machine, alors [x := E] I représente la plus faible condition pour que l'exécution x := E se termine et établisse I. Explications :

[x := E] I remplace les occurrences libres de x dans I par l'expression E.
Par exemple, [x := x+1] (x : N) donne x+1 : N ;
[S] I est interprété ainsi :
I est la condition désirée « après » (on dit aussi post-condition). C'est un prédicat.
[S] I est la condition nécessaire et suffisante « avant ».

Ainsi toute substitution S définit ce qu'on appelle un « transformateur de prédicat » qui associe à toute post-condition R la plus faible pré-condition, notée [S] I, permettant de garantir que R est vraie juste après l'exécution de l'opération. Lorsque c'est bien le cas (R est vraie après l'exécution de l'opération S), on dit que S établit R. La notion de plus faible précondition (weakest precondition) a été introduite par E.W. Dijkstra avec la notation wp(S,I).

Exemple : condition désirée après : x <=10 substitution : x := x+1 condition nécessaire et suffisante « avant » :

[x := x+1] (x<=9)
x+1 <= 10
x <= 9
x<=9 est la condition nécessaire et suffisante pour que x <= 10 soit vrai après la substitution.*/
OPERATIONS

/* Cette rubrique (en B, on dit aussi clause) contient la définition des opérations offertes par la machine abstraite (on dit aussi, opérations faisant partie du répertoire d'instructions de la machine, ou encore, services offerts par la machine abstraite). Une opération a une en-tête qui a la forme générale suivante : Nom des paramètres de sortie <-- Nom de l'opération (Nom des paramètres d'entrée)

On a donc 4 cas possibles :

    • Nom de l'opération
    • Nom de l'opération (nom des paramètres d'entrée)
    • Nom des paramètres de sortie <-- nom de l'opération (nom des paramètres d'entrée)

Dans cet exemple, nous n'avons que le premier cas. */

reserver =
 PRE
 0 < nb_sieges_dispos
 THEN
 nb_sieges_dispos := nb_sieges_dispos - 1
 END;

/* Le symbole égal surmonté d'un chapeau se lit « se définit ainsi ». Il se différencie ainsi du symbole d'égalité. Ici, il est noté par « = » en notation ascii.

Vous voyez apparaître un PRE...THEN... . A quoi cela sert-il ? Supposons qu'on ait écrit seulement nb_sieges_dispos := nb_sieges_dispos - 1 On doit avoir : (voir l'exemple précédent)

[nb_sieges_dispos := nb_sieges_dispos - 1] (nb_sieges_dispos : 0..max-sieges) et donc
nb_sieges_dispos - 1 : 0..max-sieges,

prédicat qui ne peut être vérifié si nb_sieges_dispos vaut 0. Or on veut que l'invariant soit respecté par les opérations. On utilise pour ça une précondition d'emploi de l'opération. */


annuler =
PRE
  nb_sieges_dispos < max_sieges
THEN
  nb_sieges_dispos := nb_sieges_dispos + 1
END;

/* Annuler une réservation consiste à additionner 1 au nombre de sièges disponibles. On a mis une précondition pour s'assurer qu'on ne dépassera pas sa limite. */


 END 

/* Fin de la spécification abstraite. */

Une autre machine abstraite B[modifier | modifier le wikicode]

SVP : fournir une page wiki directement intégrable dans l'outil B

 MACHINE maPetiteEntreprise
 /* rédige par Dudule le 06-04-2005 */
 SETS
 PROJET; SERVICE; EMPLOYE
 VARIABLES
 employe, service, projet, est_affecte, est_responsable_de_projet, est_responsable_de_service
 INVARIANT
employe <: EMPLOYE & service <: SERVICE &  projet <: PROJET &
est_affecte : employe --> service & 
est_responsable_de_service : employe >+> service &
est_responsable_de_service <: est_affecte &
est_responsable_de_projet : employe >+> projet &
dom(est_responsable_de_projet) /\ 
 dom(est_responsable_de_service)={}
INITIALISATION
employe, service, projet, est_affecte, est_responsable_de_service,est_responsable_de_projet := {},{},{},{},{},{}
OPERATIONS

   ajout_employe(ss)=
      PRE
        ss : SERVICE  &  ss : service  &  (EMPLOYE -employe) /= {}
    THEN
        ANY ee WHERE
           ee : (EMPLOYE - employe)
         THEN
            employe := employe \/ { ee } 
         ||   est_affecte := est_affecte \/ { ee|->ss }
         END
      END;


   ajout_service=
      PRE
        (SERVICE-service) /= {}
      THEN<
         ANY ss WHERE
            ss : (SERVICE-service)
      THEN
          service:=service \/ {ss}
      END
   END;
   ajout_responsable_service(ee,ss)=
      PRE
         ss : SERVICE &          ss : service &          ee : EMPLOYE &          ee : employe &
         ee /: dom (est_responsable_de_service) &
         ee /: dom(est_responsable_de_projet) &
         ss /: ran (est_responsable_de_service) &
         ee|->ss: est_affecte
      THEN
         est_responsable_de_service:=est_responsable_de_service \/ {ee|->ss}
      END;


   ajout_projet=
      PRE
         (PROJET - projet) /: { }
      THEN
         ANY pp WHERE
            pp : (PROJET - projet)
         THEN
            projet:=projet \/ {pp}
         END
      END;


   ajout_responsable_projet(pp, ee)=
      PRE
         pp : PROJET &
         pp : projet &
         ee : EMPLOYE &
         ee : employe &
         ee /: dom (est_responsable_de_service) &
         ee /: dom (est_responsable_de_projet) &
         pp /: ran (est_responsable_de_projet)
      THEN
         est_responsable_de_projet := est_responsable_de_projet \/ { ee|->pp }
      END;


   suppression_employe(ee)=
      PRE
         ee : EMPLOYE &
         ee : employe &
         ee : dom (est_affecte) &
         ee /: dom (est_responsable_de_service) &
         ee /: dom(est_responsable_de_projet)
      THEN
         employe := employe - {ee} ||
         est_affecte := {ee} <<| est_affecte
      END;


   suppression_responsable_service(ss)=
      PRE
         ss : SERVICE &
         ss : service &
         ss : ran (est_responsable_de_service) &
         est_responsable_de_service~(ss) |-> ss: est_affecte
      THEN
         est_responsable_de_service:= {est_responsable_de_service~(ss)} <<|est_responsable_de_service
      END;


   suppression_service(ss)=
      PRE
         ss : SERVICE &
         ss : service &
         ss /: ran (est_responsable_de_service)
      THEN
         service := service - {ss}
      END;


   suppression_responsable_projet(pp)=
      PRE
         pp : PROJET &
         pp : projet &
         pp : ran (est_responsable_de_projet)
      THEN
         est_responsable_de_projet := {est_responsable_de_projet~(pp)}<<|est_responsable_de_projet
      END;


   suppression_projet(pp)=
      PRE
         pp : PROJET &
         pp : projet &
         pp /: ran (est_responsable_de_projet)
      THEN
         projet := projet - {pp}
      END
END