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.

Proposition

Z is a typed language, to introduce a variable in a specification, it needs to be declared and associated.
e.g. x : N, where N is set of all natural numbers.
A predicate is an expression containing one or more free variables which act as a placeholders for values drawn from specific sets.
e.g. give x, y : N, the expression x = y + 3 is a predicate with two free variables x and y.
A predicate is a template for constructing propositions by plugging in values.
A predicate is like a proposition with various "slots" to be filled in by objects of various kinds.
Therefore to build a proposition from a predicate, we must remove all the free variables.
This can be done either by:
- Replace free variable with a particular value.
- Bind it with a quantification.

∀ <name> : <type> | <optional constraint> | ∙ <predicate>