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.




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