Computer Laboratory

Technical reports

Transforming axioms for data types into sequential programs

Robert Milne

44 pages

Abstract

A process is proposed for refining specifications of abstract data types into efficient sequential implementations. The process needs little manual intervention. It is split into three stages, not all of which need always be carried out. The three stages entail interpreting equalities as behavioural equivalences, converting functions into procedures and replacing axioms by programs. The stages can be performed as automatic transformations which are certain to produce results that meet the specifications, provided that simple conditions hold. These conditions describe the adequacy of the specifications, the freedom from interference between the procedures, and the mode of construction of the procedures. Sufficient versions of these conditions can be checked automatically. Varying the conditions could produce implementations for different classes of specification. Though the transformations could be automated, the intermediate results, in styles of specification which cover both functions and procedures, have interest in their own right and may be particularly appropriate to object-oriented design.

Full text

PDF (2.2 MB)

BibTeX record

@TechReport{UCAM-CL-TR-221,
  author =	 {Milne, Robert},
  title = 	 {{Transforming axioms for data types into sequential
         	   programs}},
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-221.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-221}
}