What is Z?
Z is a precise form of mathematics. It was designed for the formal specification of software systems.
Computer programs have precise meanings, as determined by the computer that executes them. Programs define exactly how a computer is to solve a problem, and hence are inevitably very detailed. This level of detail makes programming tedious for the average human, and error prone for the best of us.
An aim of specification is to define a problem in less detailed terms, capturing what the problem is, without unduly constraining how it is to be solved. A specification should aid understanding, and assist development and maintenance of a corresponding program.
Formal specifications have precise meanings, as defined by standards documents. Although they cannot typically be executed by computers, this precision allows consequences to be determined by formal reasoning, which is a process in which computers can assist. This can allow mistakes to be detected and corrected sooner (and hence more cheaply) than if a program had been built first.
Z can be used for mathematical modelling of many systems, not just software systems.
An International Standard for the syntax, type system and semantics of Z notation was published by ISO in 2002. It is available from http://standards.iso.org/ittf/PubliclyAvailableStandards/c021573_ISO_IEC_13568_2002(E).zip