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.
 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 :
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 » :
 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 : 
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)
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.
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) /\ 
 INITIALISATION
 OPERATIONS

Méthode B/Différence avec Z
nota : nous avons utilisé aussi bien pour Z que pour B la notation ASCII B. 
[NOM, ADRESSE]
 _____CarnetDAdresses___________________
 NomConnu : F NOM
 APourAdresse : NOM -+> ADRESSE
 __________
 dom (APourAdresse) = NomConnu
 ____________________________________
 _____AjoutDAdresse_______________________
 Δ CarnetDAdresses
 nom? : NOM
 adr? : ADRESSE
 ___________
 nom? : NomConnu ?
 _________________________________________
A-t-on besoin, en Z, de spécifier que :
Réfléchissez bien à cette question.
Et lisez ensuite ce qui suit :
 MACHINE
 CarnetDAdresses
 SETS
 NOM; ADRESSE
 VARIABLES
 NomConnu, APourAdresse
 INVARIANT
 NomConnu <: NOM &
 ApourAdresse: NomConnu +->ADRESSE
 INITIALISATION
 NomConnu := {} ||
 OPERATIONS
 AjoutDAdresse(nom, adr) =
 PRE
 nom : NOM - NomConnu &
 adr : ADRESSE
 THEN
 APourAdresse := APourAdresse <+ {nom |-> adr} ||
 END
 END