Die Z Notation , genannt nach der Zermelo-Fraenkel Mengenlehre, ist eine formelle Spezifizierungssprache, die verwendet ist, um Rechensysteme zu beschreiben und zu modellieren. Es wird an der klaren Spezifizierung von Computerprogrammen und computergestützten Systemen im Allgemeinen ins Visier genommen.

Geschichte

1974 hat Jean-Raymond Abrial "Datensemantik" veröffentlicht. Er hat eine Notation verwendet, die später in der Universität von Grenoble bis zum Ende der 1980er Jahre unterrichtet würde. Während an EDF (Électricité de France) Abrial innere Zeichen auf Z geschrieben hat. Die Z Notation wird verwendet 1980 bestellen Méthodes de programmation vor.

Z wurde von Abrial 1977 mit der Hilfe von Steve Schuman und Bertrand Meyer ursprünglich vorgeschlagen. Es wurde weiter an Programming Research Group an der Universität Oxford entwickelt, wo Abrial am Anfang der 1980er Jahre gearbeitet hat, Oxford im September 1979 erreicht.

Abrial antwortet auf die Frage "Warum Z?" mit, "Weil es die äußerste Sprache ist!"

Gebrauch und Notation

Z basiert auf der mathematischen Standardnotation, die in der axiomatischen Mengenlehre, Lambda-Rechnung und Prädikat-Logik der ersten Ordnung verwendet ist. Alle Ausdrücke in der Z Notation werden getippt, dadurch einige der Paradoxe der naiven Mengenlehre vermeidend. Z enthält einen standardisierten Katalog (hat das mathematische Werkzeug genannt) allgemein verwendeter mathematischer Funktionen und Prädikate.

Obwohl Z Notation (gerade wie die APL Sprache, lange davor) viele non-ASCII Symbole verwendet, schließt die Spezifizierung Vorschläge ein, für die Z Notationssymbole in ASCII und im LATEX zu machen.

Standards

Der ISO hat eine Z Standardisierungsanstrengung 2002 vollendet. Dieser Standard und eine technische Berichtigung sind von ISO umsonst verfügbar:

• der Standard ist vom ISO ITTF Seite öffentlich verfügbar (und für den Kauf von der ISO Seite verfügbar);
• die technische Berichtigung ist von der ISO Seite zu einem Selbstkostenpreis von CHF 0,00 verfügbar.

Werkzeuge

• ERZ: Werkzeug dafür gestaltet ER Modell in die Z Notation gleichwertig, durch Luis Espino um
• Projekt von Community Z Tools (CZT)
• Werkzeuge, um Z Spezifizierungen in Microsoft Word sich zu entwickeln und zu überprüfen
• Der Fusseln-Typ-Kontrolleur von Mike Spivey für Z
• Z/Eves — Ein Probekontrolleur für die Z Notation (deutsche Seite, aber alle Handbücher in Englisch)
• Z/EVES Dokumentation, Zeitungen und Handbücher auf Z/EVES
• ZETA System der offenen Quelle für Entwicklungssoftwarespezifizierungen in Z
• HOL-Z Probeumgebung der offenen Quelle für Z in Isabelle/HOL
• CADiZ, eine Reihe von Werkzeugen der kostenlosen Software, die Gebrauch der Z Notation helfen
• ProofPower, ein Gefolge von Werkzeugen der offenen Quelle, die Spezifizierung und Beweis in HOL und in der Z Notation unterstützen

Siehe auch

• Z User Group (ZUG)

Projekt von Community Z Tools (CZT)

• Andere formelle Methoden (und Sprachen mit formellen Spezifizierungen):
• Z ++ und Gegenstand-Z: Gegenstand-Erweiterungen für die Z Notation
• Abstract Machine Notation (AMN), die in der B-Methode verwendet ist
• Legierung, eine Spezifizierungssprache, die durch die Z Notation und das Einführen der Grundsätze von Object Constraint Language (OCL) begeistert ist.
• Am schnellsten ist ein musterbasiertes Probewerkzeug für die Z Notation.

Weiterführende Literatur

Links

Allgemeiner

• Das World Wide Web Virtuelle Bibliothek: Die Z Notation, durch Jonathan Bowen
• Spezifizierungsvorschläge von Ian Toyn
• W3C WSDL 2.0 eine Spezifizierung, die Z Notationsbehauptungen und Erklärung enthält