Z-Notation - Z notation
Die Z - Notation / z ɛ d / ist eine formale Spezifikationssprache benutzt wird für die Modellierung und Computersysteme. Es zielt auf die klare Spezifikation von Computerprogrammen und computerbasierten Systemen im Allgemeinen ab.
Geschichte
1974 veröffentlichte Jean-Raymond Abrial "Data Semantics". Er verwendete eine Notation, die später bis Ende der 1980er Jahre an der Universität Grenoble gelehrt wurde . Während seiner Zeit bei EDF ( Électricité de France ) schrieb Abrial interne Notizen zu Z. Die Z-Notation wird in dem Buch Méthodes de Programmation von 1980 verwendet .
Z wurde ursprünglich 1977 von Abrial mit Hilfe von Steve Schuman und Bertrand Meyer vorgeschlagen . Es wurde an der Programming Research Group der Oxford University weiterentwickelt , wo Abrial Anfang der 1980er Jahre arbeitete, nachdem sie im September 1979 in Oxford angekommen war.
Abrial hat gesagt, dass Z so heißt "Weil es die ultimative Sprache ist!" obwohl der Name " Zermelo " durch seine Verwendung der Zermelo-Fraenkel-Mengentheorie auch mit der Z-Notation verbunden ist .
Verwendung und Notation
Z basiert auf der mathematischen Standardnotation, die in der axiomatischen Mengentheorie , der Lambda-Kalküle und der Prädikatenlogik erster Ordnung verwendet wird . Alle Ausdrücke in Z-Notation sind typisiert , wodurch einige der Paradoxien der naiven Mengenlehre vermieden werden . Z enthält einen standardisierten Katalog (der als mathematischer Werkzeugkasten bezeichnet wird ) häufig verwendeter mathematischer Funktionen und Prädikate, der unter Verwendung von Z selbst definiert wird.
Da die Z-Notation (genau wie die APL-Sprache , lange bevor sie) viele Nicht- ASCII- Symbole verwendet, enthält die Spezifikation Vorschläge zum Rendern der Z-Notation-Symbole in ASCII und in LaTeX . Es gibt auch Unicode- Kodierungen für alle Standard-Z-Symbole.
Normen
ISO hat 2002 eine Z-Standardisierungsbemühung abgeschlossen. Diese Norm und ein technisches Korrigendum sind von ISO kostenlos erhältlich:
- der Standard ist kostenlos auf der ISO-ITTF-Site öffentlich verfügbar und kann separat auf der ISO-Site erworben werden;
- das technische Korrigendum ist auf der ISO-Site kostenlos erhältlich.
Vergeben
1992 genehmigte Ihre Majestät die Königin mit großer Freude die Empfehlung des Premierministers , dass der Queen's Award for Technological Achievement dieses Jahr dem Oxford University Computing Laboratory verliehen werden sollte . Das Oxford University Computing Laboratory [erhielt] den Preis gemeinsam mit IBM United Kingdom Laboratories Limited für die Entwicklung einer Programmiermethode basierend auf elementarer Mengenlehre und Logik, bekannt als Z-Notation , und deren Anwendung im IBM Customer Information Control System (CICS) Produkt .“
Siehe auch
- Z-Benutzergruppe (ZUG)
- Community Z Tools (CZT)-Projekt
- Andere formale Methoden (und Sprachen, die formale Spezifikationen verwenden ):
- FDM (Formal Development Methodology), das sich um die Spezifikations-Untersprachen Ina Jo und Ina Flo dreht, die in den 1980er und 1990er Jahren sehr beliebt waren
- VDM-SL , die wichtigste Alternative zu Z
- B-Methode , entwickelt von Jean-Raymond Abrial (Erfinder der Z-Notation)
- Z++ und Object-Z : Objekterweiterungen für die Z-Notation
- Alloy , eine von der Z-Notation inspirierte Spezifikationssprache, die die Prinzipien der Object Constraint Language (OCL) implementiert .
- Verus, ein proprietäres Tool von Compion, Champaign, Illinois (später von Motorola gekauft), für den Einsatz in dem mehrstufigen sicheren UNIX-Projekt, das von seiner Division Addamax entwickelt wurde.
- Fastest ist ein modellbasiertes Testwerkzeug für die Z-Notation.
Verweise
Weiterlesen
- Spivey, John Michael (1992). Die Z-Notation: Ein Referenzhandbuch . Internationale Reihe in Informatik (2. Aufl.). Lehrlingssaal .
- Davies, Jim ; Woodcock, Jim (1996). Verwendung von Z: Spezifikation, Verfeinerung und Beweis . Internationale Reihe in Informatik. Lehrlingssaal. ISBN 0-13-948472-8.
- Bowen, Jonathan (1996). Formale Spezifikation und Dokumentation mit Z: Ein Fallstudienansatz . Internationale Thomson-Computerpresse, Internationaler Thomson-Verlag . ISBN 1-85032-230-9.
- Jacky, Jonathan (1997). Der Weg von Z: Praktisches Programmieren mit formalen Methoden . Cambridge University Press . ISBN 0-521-55976-6.