On proving inductive properties of abstract data types

ABSTRACT

The equational axioms of an algebraic specification of a data type (such as finite sequences) often can be formed into a convergent set of rewrite rules; i.e. such that all sequences of rewrites are finite and uniquely terminating. If one adds a rewrite rule corresponding to a data type property whose proof requires induction (such as associativity of sequence concatenation), convergence may be destroyed, but often can be restored by using the Knuth-Bendix algorithm to generate additional rules. A convergent set of rules thus obtained can be used as a decision procedure for the equational theory for the axioms plus the property added. This fact, combined with a "full specification" property of axiomatizations, leads to a new method of proof of inductive properties--not requiring the explicit invocation of an inductive rule of inference.

REFERENCES

• 1: Bledsoe W. W., and P, Bruell, "A Man-Machine Theorem-Proving System," Artificial Intelligence, Vol. 5, pp. 51-72 (1974).
• 2: Boyer, R. S., and J S. Moore, "A Lemma Driven Automatic Theorem Prover for Recursive Function Theory," Proceedings IJCAI-77 Conference, Vol. 1, pp. 511-519 (August 1977).
• 3: Burstall, R. M. and J. A. Goguen, "Putting Theories Together to Make Specifications," Proceedings of Fifth International Joint Conference on Artificial Intelligence, August 1977, pp. 1045-1058.
• 4: Courcelle, B., "On Recursive Equations Having a Unique Solution," IRIA-LABORIA Report No. 285, March 1978.
• 5: Dahl, O. J., "Can Program Proving Be Made Practical?" Institute of Informatics, University of Oslo, Norway, (1978).
• 6: Nachum Dershowitz , Z Manna, Proving termination and multiset orderings, Stanford University, Stanford, CA, 1978
• 7: Goguen, J. A., and J. J. Tardo, "An Introduction to OBJ: A Language for Writing and Testing Formal Algebraic Specifications," Proceedings of Specification of Reliable Software Conference Boston, April 3-5, 1979, pp. 170-189.
• 8: Goguen, J. A., J. W. Thatcher, E. G. Wagner and J. B. Wright, "Abstract Data Types as Initial Algebras and the Correctness of Data Representations," Proceedings of Conference on Computer Graphics, Pattern Recognition and Data Structure, Beverly Hills, Ca., pp. 89-93 (1975).
• 9: John Vogel Guttag, The specification and application to programming of abstract data types., 1975
• 10: John Guttag, Abstract data types and the development of data structures, Communications of the ACM, v.20 n.6, p.396-404, June 1977 [doi>10.1145/359605.359618]
• 11: Guttag, J. V., "Notes on Type Abstraction." Proceedings of Specifications of Reliable Software Conference, Boston, April 3-5, 1979, pp. 36-46. Also to appear in IEEE Transactions on Software Engineering.
• 12: John V. Guttag , Ellis Horowitz , David R. Musser, Abstract data types and software validation, Communications of the ACM, v.21 n.12, p.1048-1064, Dec. 1978 [doi>10.1145/359657.359666]
• 13: Guttag, J. V., E. Horowitz, and D. R. Musser, "The Design of Data Type Specifications," in Current Trends in Programming Methodology, Vol. IV, R. T. Yeh, ed., Prentice-Hall, 1978.
• 14: Guttag, J. V., and Horning, J. J., "The Algebraic Specification of Abstract Data Types," Acta Informatica, 10, 27-52, 1978.
• 15: F. W von Henke , D. C. Luckham, A methodology for verifying programs, Proceedings of the international conference on Reliable software, p.156-164, April 21-23, 1975, Los Angeles, California
• 16: Huet, G. "Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems," IRIA - LABORIA Report No. 250, Domaine de Voluceau, 78150 Rocquencourt, France.
• 17: Huet, G. and D. S. Lankford, "On the Uniform Halting Problem for Term Rewriting Systems," IRIA - LABORIA Report.
• 18: Knuth, D. E. and P. B. Bendix, "Simple Word Problems in Universal Algebras," in Computational Problems in Abstract Algebra, J. Leech, ed., Pergamon Press, New York, 1970, pp. 263-297.
• 19: Lankford D. S., Canonical Inference, University of Texas Automatic Theorem Proving Project Report ATP-32, December 1975.
• 20: Lankford, D. S. and A. M. Ballantyne, Decision Procedures for Simple Equational Theories with Commutative-Associative Axioms: Complete Sets of Commutative-Associative Reductions, University of Texas Automatic Theorem Proving Project Report ATP-39, August 1977.
• 21: Lipton, R. and Snyder, L., "On the Halting of Tree Replacement Systems," Conference on Theoretical Computer Science, University of Waterloo, 1977.
• 22: Musser, D. R., "A Data Type Verification System Based on Rewrite Rules," Proceedings of the Sixth Texas Conference on Computing Systems, Austin Texas, November 1977.
• 23: Musser, D. R., "Abstract Data Type Specification in the AFFIRM System," Proceedings of the Specifications of Reliable Software Conference, Boston, April 3-5, 1979, pp. 47-57. Also to appear in IEEE Transactions on Software Engineering.
• 24: Nakajima, R., "Sypes--Partial Types--for Program and Specification Structuring and a First Order System Iota Logic," Research Report No. 22, Institute of Informatics, University of Oslo, November 1977.
• 25: Greg Nelson , Derek C. Oppen, A simplifier based on efficient decision algorithms, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.141-150, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512775]
• 26: Spitzen, J., and B. Wegbreit, "The Verification and Synthesis of Data Structures," Acta Informatica, vol. 4, (1975), pp. 127-144.
• 27: Stickel, M. E. and G. E. Peterson, "Complete Sets of Reductions for Equational Theories with Complete Unification Algorithms," Department of Computer Sciences, University of Arizona, and Department of Mathematical Sciences, University of Missouri, September, 1977.
• 28: Norihisa Suzuki, Verifying programs by algebraic and logical reduction, Proceedings of the international conference on Reliable software, p.473-481, April 21-23, 1975, Los Angeles, California
• 29: Zilles, S. N., An Introduction to Data Algebra, Draft Working Paper, IBM San Jose Research Lab., Sept. 1975.