V rámci projektu vyskúšate aj špecifikáciu v jazyku Z. Obmedzíte sa však na vybrané operácie z UML modelu (podľa požiadaviek projektu) a poskytnete ich model v jazyku Z. Táto časť projektu nadväzuje na prednášku o jazyku Z a cieľom týchto inštrukcií nie je jej náhrada.
Na vytvorenie špecifikácie v jazyku Z použite kostru. Špecifikáciu píšte v LaTeX syntaxi pre jazyk Z, ktorej opis nájdete tu (Robert Büssow and Wolfgang Grieskamp: The Z of ZeTa):
http://staffwww.dcs.shef.ac.uk/people/A.Simons/z2sal/zdocs/Z of ZeTa.pdf
Všimnite si, že predtým ako špecifikujete operácie, musíte jednou alebo viacerými schémami špecifikovať stav systému, ktorá je spoločná pre všetky operácie. Stav nemusí byť úplný -- sústreďte sa na veci, ktoré sa týkajú operácií, ktoré chcete špecifikovať. Definujte aj iniciálizáciu stavu systému.
Na špecifikáciu v jazyku Z použijete nasledujúci softvér:
MiKTeX je jednou voľne dostupných implementácií systému na sadzbu textu LaTeX.
Do adresára s vašou špecifikáciou skopírujte štýl z-eves.sty. Použite príkaz pdflatex alebo texify z adresára miktex\bin na generovanie DVI alebo PDF súboru s vysádzanou špecifikáciou.
Systém Z/EVES nájdete na dokumentovom serveri AIS-u. Spustíte ho prostredníctvom súboru lisp.exe z adresára system.
Pôvodná webová stránka systému už nejestvuje, ale dostupný je na http://fmt.cs.utwente.nl/courses/fmse/ alebo http://www.uni-koblenz.de/~winter/Lehre/SS01/ZEves/ZEves.html (kde je dostupná aj nová verzia)
Súbor so špecifikáciou sa dá načítať voľbou File/Read z hlavného menu. Toto zároveň overí správnosť syntaxe, ale časti špecifikácie, ktoré boli úspešne načítané si systém zapamätá, a tak je nevyhnutné použiť príkaz
reset;
pred ďalším pokusom. Keďže nebudeme ďalej so špecifikáciou v systéme pracovať, jednoduchšie je použiť voľbu Chceck File, ktorá špecifikáciu len skontroluje.
Pozrite a vyskúšajte kontrolu pomocou systému Z/EVES a preklad MiKTeXom niektorých príkladov špecifikácií v jazyku Z: