Méthode B/Différence avec Z
Apparence
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.