This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
An Alphard Specification of a Correct and Efficient Transformation on Data Structures
November 1980 (vol. 6 no. 6)
pp. 572-584
J.L. Bentley, Departments of Computer Science and Mathematics, Carnegie-Mellon University
In this paper we study the problem of designing and specifying standard program components applicable to a wide variety of tasks; we choose for this study the specific problem domain of data structures for general searching problems. Within this domain Bentley and Saxe [1] have developed transformations for converting solutions of simple searching problems to solutions of more complex problems. We discuss one of those transformations, specify precisely the transformation and its conditions of applicability, and prove its correctness; we accomplish this by casting it in terms of abstract data types-specifically by using the Alphard form mechanism. The costs of the structures derived by this transformation are only slightly greater than the costs of the original structures, and the correctness of the transformation definition together with the correctness of the original structure assure the correctness of the derived structure. The transformation we describe has already been used to develop a number of new algorithms, and it represents a new level of generality in software engineering tools.
Index Terms:
transformations on data structures, Abstract data types, generic definitions, program verification, searching problems
Citation:
J.L. Bentley, M. Shaw, "An Alphard Specification of a Correct and Efficient Transformation on Data Structures," IEEE Transactions on Software Engineering, vol. 6, no. 6, pp. 572-584, Nov. 1980, doi:10.1109/TSE.1980.234506
Usage of this product signifies your acceptance of the Terms of Use.