mercredi 11 mars 2015

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...

2 commentaires:

Xavier PERINO a dit…

J'en reste bouche B. signé Zorro. En réalité signé J et pas X.

Aredius44 a dit…

Je comprends ! car ce n'était ni du Z ni du B ! comme on dit dans le milieu, c'était plein de scories qui se sont produites lors du copier-coller d'un CD retrouvé vers mon blog.
Tu as bien fait de commenter. Je viens de découvrir que j'ai un wikibook sur la Toile. Etonnante Toile. je n'avais pas à faire ça. Mais j'ai pensé à ton we que j'avais peut-être gâcher ou gâché déjà. Alors j'ai corrigé et commenté. Maintenant, tu me diras, "mais ça sert à quoi ?"
Je te dirai que par exemple, la partie sécuritaire du logiciel de la dernière ligne du métro parisien, la navette de l'aéroport Ch. De Gaulle, le métro de Barcelone, en Chine, etc... ont été réalisés en suivant la méthode B. Quand tu es passé à cette utilisation des maths (enfin des maths qui servent dans le coeur du métier), tu ne supportes plus la boxologie merisienne, youemellienne et ses textes fumeux et pédantesques.
http://fr.wikibooks.org/wiki/M%C3%A9thode_B/Diff%C3%A9rence_avec_Z

 
Site Meter