A Z notation

Szinatktikai konvenciók

Konvenciók

Szavak,dekorációk és azonosítók

Egy szó (Word) a legegyszeűbb név fajta a Z specifikációban : egy nem üres nagy és kis betűkből,
számokból és aláhúzásokból álló sorozat ami betűvel vagy speciáliskarakterrel kezdődik.A szavakat
használjuk a sémák neveiként.Egy azonosító (Ident) egy szó amit egy dekoráció (Decoration) követ ami
egy üres sorozata a "´" , a "?" vagy a "!" karaktereknek:

Ident :: = Word Decoration

Ha egy szót egy specifikációban mint séma nevet használunk akkor séma névről beszélünk és többet már
nem használható mint egy közönséges azonosító.A sémákat inkább szavakkal nevezünk el mint azonosítókkal,
hogy megengedjük a rendszerszerű dekorációt: ha A egy séma és A´-t írunk ez az A egy másolatát jelenti
amiben minden komponens "´"-vel van dekorálva.Amikor egy azonosítót ami már egy nem üres dekorációt tartalmaz
dekorálunk az új dekoráció szemben áll a régivel.
Néhány szónak speciális státusza van mint opertátor szimbólum.Függvény-szimbólumként(In-Fun vagy Post-Fun)
,reláció-szimbólumként(Pre-Rel vagy In-Rel) vagy generikus szimbókumként osztályozhatjuk őket.

Operátor szimbólumok

A Z matematikai jelölései csak néhány alap kifejezést tartalmaz,de ezek elegek, hogy közel bármilyen matematikai
tulajdonságot kifejezzünk.Például itt van egy predikátum ami azt fejezi ki, hogy az "a" és "b" összege legalább "a":

(plus(a,b)) ∈ qeq,

és itt van egy ami az összeadás asszociativitását fejezi ki:
plus(plus(a,b),c) = plus(a,plus(b,c)).

Ezek a predikátumok nagyon ridegek és az ennél bonyolultabb predikátumok egyre nehezebben olvashatóbbak lennének ha
csak tisztán ezekre a jelölésekre számíthatnánk.
Ehelyett írhatjuk a Z-ben is csak úgy mint sok más nyelvben:

a+b > a
( a + b ) + c = a + ( b + c )

Ez a Z-ben is lehetséges ugyanis a + egy infix függvény szimbólum a > pedig egy infix reláció szimbólum.Ezek
összességét hívjuk operátor szimbólumoknak és 3 csoportba tesszük őket: függvény szimbólumok, reláció szimbólumok
és a generikus szimbólumok.
A függvény szimbólumokból két fajta van: infix függvény szimbólum és a postfix mint például a tranzitív lezárt.Minden
infix függvény szimbólumnak van prioritása 1-6-ig ami a kötési erejét írja le növekvően, tehát a magasabb számú prioritás
az erősebb.Ha azonos prioritású szimbólumok találkoznak akkor balasszociativitás van.
Kétfajta reláció szimbólum van: infix és prefix.Az infix reláció szimbólumoknak bináris kapcsolataik vannak - rendezett párok
halmazai - mint értékeik.A prefix reláció szimbólumok értékei halmazok.