Z-Notation

Z ist der Name einer Notation zur formalen Spezifikation von Software-Systemen und -Modulen.

Z basiert auf der Zermelo-Fraenkel-Mengenlehre und der Prädikatenlogik erster Stufe. Spezifikationen für komplexe Software-Systeme in Z werden durch die hierarchische Komposition von Schemata erreicht. Ein Schema besteht dabei aus einer Anzahl typisierter Variablen und Bedingungen, welche an die Belegungen der Variablen gestellt werden.

Z wurde von Jean-Raymond Abrial Ende der 1970er Jahre geschaffen und durch die Programming Research Group im Oxford University Computing Laboratory weiterentwickelt. Im Jahr 2002 wurde Z durch die ISO (ISO 13568) standardisiert.

Erweiterungen

Object-Z Beispiel

Object-Z

Object-Z ist eine objektorientierte Erweiterung, die an der University of Queensland, Australien, entwickelt wurde. Sie erweitert Z durch Sprachkonstrukte, die den objektorientierten Paradigmen ähneln. Im Wesentlichen sind dies Klassen, Vererbung und Polymorphismus.

Object-Z ist zwar nicht so populär wie Z selbst, doch es erhielt erhebliche Aufmerksamkeit von der formalen Spezifikations-Gemeinschaft. Untersuchungen über verschiedene Aspekte der Sprache erfolgen derzeit, einschließlich-Sprachen, die Object-Z nutzen und diverser Tool-Unterstützungen (z.B. durch das Community Z-Tools-Projekt).

Z++

Z++ ist eine objektorientierte Erweiterung der Z-Notation.

Literatur

• J. Michael Spivey: The Z Notation: a reference manual, 2nd edition, Prentice Hall International Series in Computer Science 1992, ISBN ISBN 0-13-978529-9
• Jim Davies and Jim Woodcock: Using Z: Specification, Refinement and Proof. Prentice Hall International Series in Computer Science 1996, ISBN 0-13-948472-8
• Jonathan Bowen: Formal Specification and Documentation using Z: A Case Study Approach. International Thomson Computer Press 1996, ISBN 1-85032-230-9
• Jonathan Jacky: The Way of Z: Practical Programming with Formal Methods. Cambridge University Press 1997, ISBN 0-521-55976-6
• Information Technology – Z Formal Specification Notation – Syntax, Type System and Semantics, ISO/IEC 13568:2002 2002
• Z: An Introduction to Formal Methods, 2nd edition, John Wiley & Sons Ltd 1996, ISBN 0-471-93973-0
• Object-Z: An object-oriented extension to Z., David A. Carrington, David Duke, Roger Duke, Paul King, Gordon A. Rose, and Graeme Smith. in S. Vuong, Formal Description Techniques II, FORTE'89, S. 281-296, North-Holland, 1990.
• Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics (ISO/IEC 13568:2002)

Weblinks

• Community Z Tools
• CADiZ (Free Software Tools that assist the use of Z)
• Object-Z Webseite, University of Queensland, Australien
• Z User Meetings, International Conference of Z Users