# Méthode B/Première machine abstraite

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.
/* Le nom de la machine est réservation. On lui passe en paramètre la variable max_sieges. */
/* Prédicat d'appartenance. max_sieges appartient à l'ensemble des nombres naturels implantables */
/* nb_sieges_dispos est une variable. On va apprendre dans la rubrique INVARIANT quel est son type. */
/* 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.*/
/* 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.*/
/* 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 :
Dans cet exemple, nous n'avons que le premier cas. */
/* 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 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. */
/* Fin de la spécification abstraite. */

### Une autre machine abstraite B

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