A formal notation, based on set algebra and predicate calculus, for the specification of computing systems. It was developed at the Programming Research Group, Oxford University. Z specifications have a modular structure. See also constructive specification.