Den Z-notasjon er en spesifikasjon språk som brukes for å beskrive og modellere datasystemer.
Z-rangering ble opprettet av Jean-Raymond Abrial . Z dukket først opp i en bok i løpet av 1980-utgaven av Meyer og Baudouins arbeid, Methods of programming, Eyrolles. På den tiden var det bare notater fra Jean-Raymond Abrial, interne for EDF. De fulgte med på artikkelen han hadde publisert i 1974, med tittelen Data Semantics in Data Base Management (Kimbie, Koffeman, red., Nord-Holland, 1974, s. 1-59 ).
I 1983 brukte Delobel og Adiba den opprinnelige Z-notasjonen i sin bok "Databases and Relational Systems" (Dunod). Under navnet "binær relasjonsmodell" brukes den til dem for å introdusere "n-ary relasjonsmodell" av Ted Codd. En grafisk notasjon bruker denne binære relasjonsmodellen, det er NIAM (Nijssen Information Analysis Method), (H. Habrias, The binær relasjonsmodell, Eyrolles, 1988) utviklet innen Control Data i Brussel.
Abrial tok Z med til Programming Group i Oxford i September 1987. Han forlot Z for å foreslå metode B på 1980-tallet. Den første internasjonale standarden (ISO) på Z ble publisert iJuli 2002.
Brukes når det er mulig, ASCII notasjon av B. Vi finner korrespondanse med notasjonen B Metode B .
[STUDENT, GRUPPE]
STUDENT og GROUP er grunnleggende typer (SETS av B)
Her er hva i Z, vi kaller diagrammer:
Et diagram har et navn, her MyPetiteEcole, to deler:
Husk at POW ({1, 2}) = {{}, {1}, {2}, {1,2}}
Δ erklærer: promo, promo ', aPourGroupe, aPourGroupe'. Premien uttrykker staten etter operasjonen.
Advarsel!
Du leste riktig. Ovenfor skrev vi = (likhetspredikat) og ikke: = (substitusjon). En ordning er et predikat. Linjeskiftet uttrykker en konjunktjon (⩓).
Registreringsordningen gir predikatet som må respekteres av registreringsoperasjonen.
Χ erklærer: promo, promo ', aPourGroupe, aPourGroupe' og begrensningene:
promo = promo '
aPourGroupe' = aPourGroupe
Dette betyr at vi ikke vil at avstemningsoperasjonen skal endre tilstanden til dataene.
Et diagram vil gjøre det mulig å spesifisere en starttilstand, som, som i B, brukes til å sikre at man virkelig kan ha en tilstand som tilfredsstiller begrensningene.
RAPPORT :: = ok | allerede kjent | ukjent
RAPPORT er en gratis type.
Vi kommer til å ha en robust spesifikasjon
RInscription == (Inscription & Succès) or DéjàConnuDet er andre operatører enn & og eller for beregning av ordninger.
etc.
Vi har presentert lukkede diagrammer. Erklæringer er lokale for disse skjemaene.
Det er åpne ordninger (aksiomatisk beskrivelse) som introduserer en eller flere globale variabler og muligens spesifiserer en begrensning på deres verdier.
Eksempel:
carré : NAT → NAT _________________{... | ... • ...}
Det er tre deler {erklæring | begrensning • uttrykk}
eksempel:
{x : NAT | pair (x) • x * x} est l'ensemble des carrés des nombres pairs.Vi kan ta et diagram som en type.
Et diagram blir da sett på som settet med tilstander som respekterer diagrammet. En diagramtypevariabel kan da ta en av disse tilstandene som respekterer diagrammet som er angitt som typen av variabelen.
Eksempel
På fransk tre bøker om Z.