IBM Journal of Research and Development
IBM Skip to main content
  Home     Products & services     Support & downloads     My account  

  Select a country  
Journals Home  
  Systems Journal  
Journal of Research
and Development
    Current Issue  
    Recent Issues  
    Papers in Progress  
    Search/Index  
    Orders  
    Description  
    Patents  
    Recent publications  
    Author's Guide  
  Staff  
  Contact Us  
  Related links:  
     IBM Research  

IBM Journal of Research and Development  
Volume 31, Number 5, Page 546 (1987)
Formal Definition/Design of Computer Systems
  Full article: arrowPDF   arrowCopyright info





   

Specification statements and refinement

by C. Morgan, K. Robinson
We discuss the development of executable programs from state-based specifications written in the language of first-order predicate calculus. Notable examples of such specifications are those written using the techniques Z and VDM; but our interest is in the rigorous derivation of the algorithms from which they deliberately abstract. This is, of course, the role of a development method. Here we propose a development method based on specification statements with which specifications are embedded in programs—standing in for developments "yet to be done." We show that specification statements allow description, development, and execution to be carried out within a single language: programs/specifications become hybrid constructions in which both predicates and directly executable operations can appear. The use of a single language—embracing both high- and low-level constructs—has a very considerable influence on the development style, and it is that influence we discuss: the specification statement is described, its associated calculus of refinement is given, and the use of that calculus is illustrated.
Related Subjects: Formal methods; Mathematics; Programming, programs, and programming languages; Semantics