Specification, Design, Implementation
Formal Specifications help us to write programs and enable us to prove that a particular program either does or does not meet its specification.
Z: Many high level abstract mathematical data types and operations are specified by giving their preconditions and postconditions
In moving towards the programming language constructs that are available to us, we often rewrite the specification using less abstract data types and more ‘algorithmic’ constructs.
This second specification in an intermediate between the specification and the final program and it is often referred to as the design.
Any program which is a correct implementation of the design must also be a correct implementation of the specification.