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 ?
  APourAdresse' = APourAdresse <+ {(nom? |-> adr?)}

 _________________________________________

A-t-on besoin, en Z, de spécifier que : NomConnu' = NomConnu \/ {nom?}

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 := {} ||
   APour Adresse := {}

OPERATIONS
   AjoutDAdresse(nom, adr) =
      PRE
         nom : NOM - NomConnu &
         adr : ADRESSE
      THEN
         APourAdresse := APourAdresse <+ {nom |-> adr} ||
         NomConnu := NomConnu \/{nom}
      END

END

• En B n'est modifié que ce que l'on spécifie explicitement être modifié.
• En Z, la spécification est un prédicat. Notez que le := n'est pas utilisé en Z.