Aller au contenu

Méthode B/Différence avec Z

Un livre de Wikilivres.

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.