Z notation

Z notation is a formal specification language developed at the University of Oxford in the 1980s, built on Zermelo–Fraenkel set theory and first-order predicate logic. It uses a schema calculus — a structured way to describe states and operations over them — to specify software systems with mathematical precision without prescribing implementation details. A schema in Z names a collection of typed variables and their relationships, making it possible to compose specifications modularly and to prove properties about them. Z was applied industrially to the IBM CICS (Customer Information Control System) transaction processing system, where formal specifications uncovered errors that had persisted in the codebase for decades. Despite its mathematical clarity, Z's adoption has been limited by the same organizational barriers that afflict all formal methods: the cost of training engineers in set theory and the difficulty of integrating specifications into agile development cycles. Z remains a paradigmatic example of how mathematical rigor can be applied to industrial software, even if its uptake has never matched its intellectual merit. The VDM (Vienna Development Method) is a related approach that shares Z's set-theoretic foundations but uses a different notation and methodology.