Inductive methods for reasoning about abstract data types

ABSTRACT

Rewriting techniques have been used to reason about a variety of topics related to programming languages, e.g., abstract data types, Petri Nets, FP programs, and data bases. They have also been used in the implementation and definition of a variety of programming languages. At the 1980 POPL Conference, David Musser proposed a new method of proving inductive properties of abstract data types. Since that time, this method, which came to be called inductionless induction, has attracted considerable attention. Numerous applications and improvements have been proposed and several implementations described. However, little or no work has appeared that questions the basic utility of the idea. The thesis of this paper is that while induction using equational term-rewriting holds great promise, inductionless induction does not. More specifically, we argue that for reasoning about abstract data types traditional inductive methods are usually superior.

REFERENCES

• 1: Backus, J., Williams, J. H., and Wimmers, E. L. FL Language Manual (Preliminary Version), IBM Almaden Research Center Research Report, 1986.
• 2: F Bellegarde, Rewriting systems on FP expressions to reduce the number of sequences yielded, Science of Computer Programming, v.6 n.1, p.11-34, Jan. 1986
• 3: Boyer, R. S. and Moore, J. S. A Computat.i.onal Lo~;ic, Academic Press, 1979.
• 4: Burstall, R. "Proving properties of programs by structural induction," Computer J. 12:1 (1969), 41-48.
• 5: BurstaI1, R. and Goguen, J. "Putting Theories Together to Make Specifications," Proceedings Fifth IJCAI, 1977.
• 6: C. Choppy , C. Johnen, PETRIREVE: proving Petri net properties with rewriting systems, Proc. of the first international conference on Rewriting techniques and applications, p.271-286, December 1985, Dijon, France
• 7: Stavros S. Cosmadakis , Paris C. Kanellakis, Two applications of equational theories to database theory, Proc. of the first international conference on Rewriting techniques and applications, p.107-123, December 1985, Dijon, France
• 8: Forgaard, R. and Guttag, J. V. "REVE: A Term Rewriting System Generator with Failure-Resistant Knuth-Bendix," Proceedings of an NSF Workshop on the Rewrite Rule Laboratory, General Electric Corporate Research and Development Report No. 84GEN008, Schenectady, NY, April 1984, 5-31.
• 9: Fribourg, L. "Oriented Equational Clauses as a Programming Language," Journal of Logic Programming 1 (1984), 165-177.
• 10: Kokichi Futatsugi , Joseph A. Goguen , Jean-Pierre Jouannaud , José Meseguer, Principles of OBJ2, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.52-66, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318610]
• 11: Joseph A. Goguen, How to Prove Algebraic Inductive Hypotheses Without Induction, Proceedings of the 5th Conference on Automated Deduction, p.356-373, July 08-11, 1980
• 12: Guttag, J. V. and Horning, J. J. "The Algebraic Specification of Abstract Data Types," Acta Informatica 10 (1978), 27-52.
• 13: J V Guttag , J J Horning, Report on the Larch shared language, Science of Computer Programming, v.6 n.2, p.103-134, March 1986
• 14: Guttag, J. V., Horning, J. J., and Wing, J. M. "An Overview of 1;he Larch Family of Specification Languages," IEEE Software 2:5 (Sept. 1985), 24-36.
• 15: Henkin, L. "The Logic of Equality," American Mathematical ~onthly 84 (1977), 597-612.
• 16: Huet, G. and Hullot, J. M. "Proofs by Induction in Equational Theories with Constructors," J. Computer and System Science8 25:2 (Oct. 1982), 239-266.
• 17: Jouannaud, J.-P. and Kounalis, E. "Proof by Induction in Equational Theories without Constructors," Proc. Second IEEE Symposium on Logic in Computer Science, Cambridge, M_k, June 1986, 358-366.
• 18: Deepak Kapur , David R. Musser, Proof by consistency, Artificial Intelligence, v.31 n.2, p.125-157, Feb. 1987 [doi>10.1016/0004-3702(87)90017-8]
• 19: Knuth, D. E. and Bendix, P. B. "Simple Word Problems in Universal Algebras," in Computational Problems in Abstract Algebra, J. Leech (ed.), Pergamon Press, Oxford, 1969, 263-297.
• 20: Lankford, D. S. "A Simple Explanation of Inductionless Induction," MTP-14, Louisiana Technical University, 1981.
• 21: Lazrek, A., Lescanne, P., and Thiel, J.-J. "Proving Inductive Equalities: Algorithms and Implementation," Report 86-R-087, Centre Recherche en Informatique de Nancy, France, September 1986.
• 22: Pierre Lescanne, Computer experiments with the REVE term rewriting system generator, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.99-108, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567078]
• 23: David R. Musser, On proving inductive properties of abstract data types, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.154-162, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567461]
• 24: Musser, D. It. "Abstract Data Type Specification in the AFFIRM System," IEEE Transactions on Software Engineering 6 (}.980).
• 25: Paul, E. "Proof by Induction in Equational Theories with Relations between Constructors," Proceedings of the Ninth Colloquium on Trees in Algebra and Programming, Bordeaux (1984), Cambridge University Press, 210-225.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Abstract data types

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Algebraic approaches to semantics
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Languages, Theory