Aller au contenu

Méthode B/Première machine abstraite

Ajouter des liens
Un livre de Wikilivres.

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... . À 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;<br/>


    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;<br/>


    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;<br/>


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


    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;<br/>


    suppression_projet(pp)=
       PRE
          pp : PROJET &
          pp : projet &
          pp /: ran (est_responsable_de_projet)
       THEN
          projet := projet - {pp}
       END
 '''END'''
Récupérée de « https://fr.wikibooks.org/w/index.php?title=Méthode_B/Première_machine_abstraite&oldid=686953 »