This Article 
 Bibliographic References 
 Add to: 
Using Term Rewriting to Verify Software
April 1994 (vol. 20 no. 4)
pp. 259-274

This paper describes a uniform approach to the automation of verification tasks associated with while statements, representation functions for abstract data types, generic program units, and abstract base classes. Program units are annotated with equations containing symbols defined by algebraic axioms. An operation's axioms are developed by using strategies that guarantee crucial properties such as convergence and sufficient completeness. Sets of axioms are developed by stepwise extensions that preserve these properties. Verifications are performed with the aid of a program that incorporates term rewriting, structural induction, and heuristics based on ideas used in the Boyer-Moore prover. The program provides valuable mechanical assistance: managing inductive arguments and providing hints for necessary lemmas, without which formal proofs would be impossible. The successes and limitations of our approaches are illustrated with examples from each domain.

[1] P. America, "A parallel object-oriented language with inheritance and subtyping,"ACM SIG-PLAN Notices, vol. 25, pp. 161-168, Oct. 1990.
[2] S. Antoy, "Automatically provable specifications," Tech. Rep. 1876, Dept. of Comput. Sci., Univ. of Md., 1987.
[3] S. Antoy, "Design strategies for rewrite rules,"CTRS' 90, published inLecture Notes in Comput. Sci., vol. 516, pp. 333-341, 1990.
[4] S. K. Basu, "On development of iterative programs from functional specifications,"IEEE Trans. Software Eng., vol. 6, no. 2, pp. 170-182, 1980.
[5] R. S. Boyer and J. S. Moore,A Computational Logic. New York: Academic Press, 1979.
[6] R. Burstall, "Proving properties of programs bv structural induction,"Comput. J., vol. 12, no. 1, pp. 41-48, 1969.
[7] C. Choppy, S. Kaplan, and M. Soria, "Complexity analysis of term-rewriting systems,"Theoretical Comput. Sci., vol. 67, pp. 261-282, 1989.
[8] J. de Bakker,Mathematical Theory of Program Correctness. London, England: Prentice-Hall, 1980.
[9] N. Dershowitz, "Termination of rewriting,"J. Symbolic Computation, vol. 3, pp. 69-116, 1987.
[10] R. Potasman, "Percolation-Based Synthesis,"Proc. 27th Design Automation Conf., IEEE CS Press, 1990, pp. 444-449.
[11] E. W. Dijkstra,A Discipline of Programming. Englewood Cliffs, NJ: Prentice-Hall, 1976.
[12] Ehrig, H., and B. Mahr,Fundamentals of Algebraic Specification 1, Springer-Verlag, Berlin, 1985.
[13] S. J. Garland, J. V. Guttag, and J. J. Horning, "Debugging Larch shared language specifications,"IEEE Trans. Software Eng., vol. 16, pp. 1044-1057, 1990.
[14] J. Goguen, "Reusing and Interconnecting Software Components,"Computer, Feb. 1986, pp. 16-28.
[15] J. Goguen, J.-P. Jouannaud, and J. Meseguer, "Operational semantics of order-sorted algebras,"CALP'85, 1985.Lecrure Notes in Computer Science, vol. 194.
[16] J.A. Goguen and T. Winkler, "Introducing OBJ3," Tech. Rep. SRI-CSL-88-9, SRI International, Menlo Park, CA, 1988.
[17] J. Guttag, "Notes on type abstraction."IEEE Trans. Software Eng., vol. 6, pp. 13-23, 1980.
[18] J. V. Guttag, E. Horowitz, and D. R. Musser, "Abstract data types and software validation,"Commun. ACM, vol. 21, pp. 1048-1064, Dec. 1978.
[19] C. A. R. Hoare, "An axiomatic basis for computer programming,"Commun. ACM, vol. 12, no. 10, pp. 576-583, 1969.
[20] C.A.R. Hoare "Proof of correctness of data representations,"Acta Informatica. vol. 1 pp. 271-281, 1972.
[21] G. Huet, "Confluent reductions: Abstract properties and applications of term rewriting systems,"J. ACM, vol. 27, no. 4, pp. 797-821, 1980.
[22] G. Huet and J.-M. Hullot, "Proofs by induction in equational theories with constructors,"JCSS, vol. 25, pp. 239-266, 1982.
[23] S. Kamin, "The expressive theory of stacks,"Acta Informatica, vol. 24, pp. 695-709, 1987.
[24] D. Kapur, P. Narendran, and H. Zhang, "On sufficient-completeness and related properties of term rewriting systems,"Acta Informatica, vol. 24, pp. 395-415, 1987.
[25] J. W. Klop, "Term rewriting systems," in S. Abramsky, D. Gabby, and T. Maibaum, Eds.,Handbook of Logic in Computer Science, ch. 6. New York: Oxford University Press, 1992.
[26] D.E. Knuth and P.B. Bendix,Simple Word Problems in Universal Algebras. New York: Pergamon, 1970, pp. 263-297.
[27] G. T. Leavens, "Modular specification and verification of object-oriented programs."IEEE Software, vol. 8, pp. 72-80, July 1991.
[28] B. Liskov and J. M. Wing, "Family values: A semantic notion of subtyping," Tech. Rep. LCS-TR-562, Mass. Inst. of Technol., Cambridge, MA, 1992.
[29] M. Wang, "A new incompleteness result for Hoare's system,"JACM, vol. 25, pp. 168-175, 1980.
[30] W. A. Wulf, R. L. London, and M. Shaw, "An introduction to the construction and verification of Alphard programs,"IEEE Trans. Software Eng., vol. 2, pp. 253-265, 1976.
[31] R. T. Yeh, "Verification of programs by predicate transformation," inCurrent Treuds in Programming Methodology. vol. 1, R. T. Yeh, ed. Enelewood Cliffs, NJ: Prentice-Hall, 1978, pp. 228-247.

Index Terms:
abstract data types; rewriting systems; program verification; theorem proving; software tools; term rewriting; verification tasks; while statements; representation functions; abstract data types; generic program units; abstract base classes; algebraic axioms; convergence; sufficient completeness; structural induction; Boyer-Moore prover; mechanical assistance
S. Antoy, J. Gannon, "Using Term Rewriting to Verify Software," IEEE Transactions on Software Engineering, vol. 20, no. 4, pp. 259-274, April 1994, doi:10.1109/32.277574
Usage of this product signifies your acceptance of the Terms of Use.