Z notation

The Z notation /ˈzɛd/ is a formal specification language used for describing and modelling computing systems.

[1] It is targeted at the clear specification of computer programs and computer-based systems in general.

In 1992, the Z User Group (ZUG) was established to oversee activities concerning the Z notation, especially meetings and conferences.

[7] Z is based on the standard mathematical notation used in axiomatic set theory, lambda calculus, and first-order predicate logic.

This standard[10] and a technical corrigendum[11] are available from ISO free: In 1992, Oxford University Computing Laboratory and IBM were jointly awarded The Queen's Award for Technological Achievement "for the development of ... the Z notation, and its application in the IBM Customer Information Control System (CICS) product.

An example of a formal specification (in Spanish) using the Z notation, with named schema boxes, including declarations and predicates