Programs: Formal specification with Z

  • Mordechai Ben-Ari


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.


Schema Signal Phone Number Predicate Calculus Traffic Signal Cache Size 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag London 2001

Authors and Affiliations

  • Mordechai Ben-Ari
    • 1
  1. 1.Department of Science TeachingWeizmann Institute of ScienceRehovotIsrael

Personalised recommendations