Méthode B/Spécification algébrique

MACHINE

   VARIABLE (VALEUR)
VARIABLES
      vrb
INVARIANT
      vrb : VALEUR
OPERATIONS

   v <-- valeur =
      BEGIN
         v:= vrb
      END ;

   changer (v) =
      PRE
         v : VALEUR
      THEN
         vrb := v
      END

END

En spécification algébrique, on écrit des AXIOMES :

valeur (changer (v)) = v

• en B, un tel axiome serait un théorème sur le modèle.
• en B, on fait la preuve que si on appelle une opération sous sa précondition, on établit l'invariant :
• I /\ P => [S] I
• (vrb : VALEUR) /\ (v: VALEUR) => [vrb : v] vrb : VALEUR