Programs: Formal specification with Z
Suppose that you are asked to develop a program. The first thing that you must do is to write a specification of the program: what the program must do. Formally, a specification is a precondition and a postcondition, and the correctness of the program is defined relative to a specific precondition and postcondition. In practice, predicate calculus and number theory as we have presented them are inconvenient for writing specifications, and other notations have been devised.
Unable to display preview. Download preview PDF.