Différence entre Z ET B

Nous sauvegardons ici des textes disparus de la Toile lors de la suppression de pages anciennes.
Supposent de connaître le contexte ! Et Latex aurait été nécessaire.
 
nota : nous avons utilisé aussi bien pour Z que pour B la notation ASCII B. Nous avons utilisé DELTA à la place de la lettre grecque majuscule delta.

Nous avons choisi le cas bien connu du carnet d'adresse..

[NOM, ADRESSE]
 _____CarnetDAdresses___________________
 NomConnu : F NOM
 APourAdresse : NOM -+> ADRESSE
 __________
 dom (APourAdresse) = NomConnu
 ____________________________________
 
Paraphrasage pour ceux ne connaissant pas la notation :

NomConnu appartient à l'ensemble fini des sous-ensembles de NOM. Donc NomConnu est est un ensemble d'éléments de l'ensemble de base NOM. Un ensemble de base est un ensemble fini et non vide sur lequel on construit la spécification.

APourAdresse appartient à l'ensemble des fonctions partielles de NOM vers ADRESSE. Donc ApourAdresse est une fonction partielle de NOM vers ADRESSE

Le domaine de APourAdresse est égal à NomConnu. Dit autrement, les noms connus sont ceux des noms ayant une adresse.

  _____AjoutDAdresse_______________________
   DELTA CarnetDAdresses
   nom? : NOM
   adr? : ADRESSE
  ___________
   nom? :  NomConnu 
   APourAdresse' = APourAdresse <+ {(nom? ,  adr?)}
 
  _________________________________________
 
DELTA indique qu'il s'agit d'un schéma de modification d'état.
On donne un nom qui doit appartenir à NOM, une adr qui doit appartenir à ADRESSE
Le nom introduit doit appartenir à NomConnu. Vous avez compris que le : note l'appartenance ensembliste en notation ascii.
Le nouvel état de ApourAdresse est égal à l'ancien état auquel on ajoute l'ensemble dont l'élément est le couple nom,adr. S'il y a déjà un couple dont l'élément de gauche est égal au nom entré en paramètre, ce couple sera changé par le nouveau couple donné en paramètre. Cette opération conservera le fait que APourAdresse soit une fonction.

Implicitement c'est un ET logique qui relie les lignes.

A-t-on besoin, en Z, de spécifier que :
NomConnu' = NomConnu \/ {nom?}
lors d'un ajout au carnet d'adresses

Réfléchissez bien à cette question.
Et lisez ensuite ce qui suit :
 
 
 Voici ce qu'on écrirait en B. A noter qu'avec les outils logiciels disponibles actuellement, il n'y a aucune difficulté pour écrire directement en notation mathématique. Des maths ensemblistes élémentaires et de la logique des prédicats d'ordre 1.
 
 
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
 
Sur la notation. C'est la même que celle de Z.
Notez que le = après le AjoutDAdresse(nom, adr) n'est pas le prédicat d'égalité, mais le symbole de la définition (dans la notation B c'est le = surmonté d'un chapeau.). Une définition est ce que les informaticiens appellent une "macro". Son expansion est à droite.
Nous avons une opération préconditionnée. On s'assure que le nom passé en paramètre de l'opération n'est pas connu alors que l'adresse adr est bien un élément de l'ensemble de base ADRESSE.
On voit apparaître le := qui se lit "devient égal". Ce n'est donc pas un prédicat. C'est une substitution. Ce qu'on n'a pas en Z.

En B n'est modifié que ce que l'on spécifie explicitement être modifié, l'invariant devant toujours être respecté.

En Z, la spécification est un prédicat. Notez que le := (devient égal*) n'est pas utilisé en Z.

* ce "devient égal" que bien des langages de programmation écrivent "=". On peut s'imaginer que ce que pourra donner l'enseignement de la programmation à l'école. Comprendre le "=" en mathématiques n'est pas évident, alors quand l'élève lira "x = x + 1" lors du cours d'informatique...