Z notation

An example of a formal specification (in Spanish) using the Z notation.

Formal specification language used for describing and modelling computing systems.

- Z notation

54 related topics


Formal specification

In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software.

Charles Babbage, sometimes referred to as the "father of computing".

languages such as Z, VDM or B rely on this paradigm

Jean-Raymond Abrial

An example of a formal specification (in Spanish) using the Z notation.

Jean-Raymond Abrial (born 1938) is a French computer scientist and inventor of the Z and B formal methods.

Specification language

Formal language in computer science used during systems analysis, requirements analysis, and systems design to describe a system at a much higher level than a programming language, which is used to produce the executable code for a system.

Structure of the syntactically well-formed, although nonsensical, English sentence, "Colorless green ideas sleep furiously" (historical example from Chomsky 1957).

This is in contrast to so-called model-oriented specification in frameworks like VDM and Z, which consist of a simple realization of the required behaviour.

Bertrand Meyer

French academic, author, and consultant in the field of computer languages.

His experiences with object technology through the Simula language, as well as early work on abstract data types and formal specification (including the Z notation), provided some of the background for the development of Eiffel.


Family of mixed-language application servers that provide online transaction management and connectivity for applications on IBM mainframe systems under z/OS and z/VSE.

Part of CICS was formalized using the Z notation in the 1980s and 1990s in collaboration with the Oxford University Computing Laboratory, under the leadership of Tony Hoare.

Programming Research Group

Part of the Oxford University Computing Laboratory (OUCL) in Oxford, England, along with the Numerical Analysis Group, until OUCL became the Department of Computer Science in 2011.

Tony Hoare, leader of the PRG from 1977 to 1999

The PRG was a centre of excellence in the field of formal methods, playing a leading role in the development of the Z notation (initiated by a visit of Jean-Raymond Abrial) and CSP (together with the associated Occam programming language).

Dansk Datamatik Center

Danish software research and development centre that existed from 1979 to 1989.

DDC's origins were in the Technical University of Denmark.
DDC subsequently located itself in the converted textile mill along the Mølleåen in Lyngby.

It sought to remedy VDM's weaknesses with respect to modularity, concurrency, and lack of tools, and it also sought to unify approaches taken in the likes of Z notation, CSP, Larch, and OBJ.


UML notation for a class. This Button class has variables for data, and functions. Through inheritance a subclass can be created as subset of the Button class. Objects are instances of a class.

Z++ (pronounced zed plus plus) is an object-oriented extension to the Z specification language.

Formal methods

In computer science, specifically software engineering and hardware engineering, formal methods are a particular kind of mathematically rigorous techniques for the specification, development and verification of software and hardware systems.

Charles Babbage, sometimes referred to as the "father of computing".

Examples of this lightweight approach to formal methods include the Alloy object modelling notation, Denney's synthesis of some aspects of the Z notation with use case driven development, and the CSK VDM Tools.

HOL (proof assistant)

HOL (Higher Order Logic) denotes a family of interactive theorem proving systems using similar (higher-order) logics and implementation strategies.

An interactive proof session in CoqIDE, showing the proof script on the left and the proof state on the right.

3) ProofPower a collection of tools designed to provide special support for working with the Z notation for formal specification. 5 of the 6 tools are GNU GPL v2 licensed. The sixth (PPDaz) has a proprietary license.