Intro

A specification is a statement of requirements for a system, object or process.
A formal specification is one in which the language of mathematics is used to construct such a statement.
Z is a formal specification language based on set theory and logic.
In a Z specification, discrete mathematical structures are used to create a model of the required system.
Predicate logic is used to state precisely the required relationships between the mathematical structures, thus defining the set of possible valid states for the system.
The math structures are more abstract and problem oriented compared to the data structures used in programming languages.
Predicate logic is then used to precisely define the required effect of operations in the system.
Philosophy is to specify what each operation is supposed to do and not how to do it.

Formal Specification