Abstract
An approach for synthesizing data type implementations based on the theory of term rewriting systems is presented. A specification is assumed to be given as a system of equations; an implementation is derived from the specification as another system of equations. The proof based approach used for the synthesis consists of reversing the process of proving theorems (i.e. searching for appropriate theorems rather than proving the given ones). New tools and concepts to embody this reverse process are developed. In particular, the concept of expansion, which is a reverse of rewriting (or reduction), is defined and analyzed. The proposed system consists of a collection of inference rules — instantiation, simplification, expansion and hypothesis tesing, and two strategies for searching for theorems depending upon whether the theorem being looked for is in the equational theory or in the inductive theory of the specification.
Research supported in part by the National Science Foundation under grants DCR-8401624 and DCR-8319966
Chapter PDF
Similar content being viewed by others
Keywords
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.
6. References
R. M. Burstall and J. Darlington, “A Transformation System for Developing Recursive Programs”, Journal of the Association for Computing Machinery, 24, 1 (January 1977), 44–67.
J. Darlington, “Program Transformation”, in Functional Programming and its Applications, An advanced course, J. D. al, (ed.), Cambridge University Press, 1982, 193–209.
N. Dershowitz, “Orderings for Term Rewriting Systems”, J.TCS, 17, 3 (1982), 279–301.
N. Dershowitz, J. Hsiang, N. Josephson and D. Plaisted, “Associative-Commutative Rewriting”, in Proc. 8th IJCAI, Karlsruhe, Germany, 1983.
M. S. Feather, “A System for Assisting Program Transformation”, Transactions on Programming Languages and Systems, 4, 1 (January 1982),.
J. A. Goguen and J. Tardo, “An Introduction to OBJ-T”, in Specification of Reliable Software, IEEE, 1979.
J. A. Goguen, J. W. Thatcher and E. G. Wagner, “Initial Algebra Approach to the Specification, Correctness, and Implementation of Abstract Data Types”, in Current Trends in Programming Methodology, vol. IV Data Structuring, R. T. Yeh, (ed.), Prentice Hall (Automatic Computation Series), Englewood Cliffs, NJ, 1978.
J. V. Guttag and J. J. Horning, “The Algebraic Specification of Abstract Data Types”, Acta Informatica, 10, 1 (1978), 27–52.
J. V. Guttag, D. Kapur and D. R. Musser, “On Proving Uniform Termination and Restricted Termination of Rewriting Systems”, in Proc. 9th ICALP, Aarhus, Denmark, 1982.
J. Hsiang, “Topics in Automated Theorem Proving and Program Generation”, UIUCDCS-R-82-1113, U. of Illinois at Urbana Champaign, Urbana Illinios, Dec. 1982.
G. Huet and J. M. Hullot, “Proofs by Induction in Equational Theories with Constructors”, in 21st IEEE Symposium on Foundations of Computer Science, 1980, 96–107.
D. K. Kapur, “Towards a Theory for Abstract Data Types,”, Tech. Rep.-237, Lab. for Computer Science, MIT, Cambridge, MA 02139, May 1980.
D. K. Kapur and D. R. Musser, “Rewrite Rule Theory and Abstract Data Type Analysis”, in Computer Algebra, EUROSAM 1982, Lecture Notes in Computer Science 144, Calmet, (ed.), Springer Verlag, April 1982, 77–90.
D. Kapur and M. K. Srivas, “A Rewrite Rule Based Approach for Synthesizing Abstract Data Types”, Tech. Rep. 84/080, Dept. of Computer Science, SUNY at Stony Brook, Stony Brook, NY 11794, July 1984.
D. E. Knuth and P. B. Bendix, “Simple Word Problems in Universal Algebras”, in Computational Algebra, J. Leach, (ed.), Pergamon Press, 1970, 263–297.
L. Kott, “Unfold/Fold Program Transformations”, Research Report No. 155, INRIA, Le Chesnay, France, August 1982.
D. S. Lankford and A. M. Ballantyne, “Decision Procedure for Simple Equational Theories with Commutative-Associative Axioms”, Report ATP-39, Univ. of TExas at Austin, 1977.
D. S. Lankford and A. M. Ballantyne, “The Refutation Completeness of Blocked Permutative Narrowing and Resolution”, in 4th Conf. on Automated Deduction, Austin, TX, 1979.
D. S. Lankford, “A Simple Explanation of Inductionless Induction”, MTP-14, Louisiana Tech Univ., 1981.
P. Lescanne, “Computer Experiments with the REVE Term Rewriting System Generator”, in 10th Annual Symposium on Principles of Prgoramming Languages, Austin, Texas, January 1983.
Z. Manna and R. Waldinger, “A Deductive Approach to Program Synthesis”, ACM Trans. Prog. Lang. and Systems, 2 1 (January 1980), 90–121.
D. R. Musser, “Abstract Data Types in the AFFIRM System”, Trans. on Software Eng., 1(6), (Jan. 1980),, IEEE.
D. R. Musser, “On Proving Inductive Properties of Abstract Data Types”, in Conference record of the Seventh Annual ACM Symposium on Principles of Programming Languages, Las Vegas, Nevada, January 1980, 154–162.
G. E. Peterson and M. E. Stickel, “Complete Sets of Reductions for Some Equational Theories”, J. ACM, 28, (1981), 233–264.
M. K. Srivas, “Automatic Synthesis of Implementations for Abstract Data Types from Algebraic Specifications”, MIT/LCS/Tech. Rep.-276, Laboratory for Computer Science, MIT, June 1982.
M. E. Stickel, “A Unification Algorithm for Associative-Commutative Functions”, J. ACM, 28, (1981), 233–264.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1985 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kapur, D., Srivas, M. (1985). A rewrite rule based approach for synthesizing abstract data types. In: Ehrig, H., Floyd, C., Nivat, M., Thatcher, J. (eds) Mathematical Foundations of Software Development. CAAP 1985. Lecture Notes in Computer Science, vol 185. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15198-2_12
Download citation
DOI: https://doi.org/10.1007/3-540-15198-2_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-15198-2
Online ISBN: 978-3-540-39302-3
eBook Packages: Springer Book Archive