Z-Notation - Z notation

Ein Beispiel für eine formale Spezifikation (in Spanisch) unter Verwendung der 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