Simultaneous checking of completeness and ground confluence for algebraic specifications

ABSTRACT

Algebraic specifications provide a powerful method for the specification of abstract data types in programming languages and software systems. Completeness and ground confluence are fundamental notions for building algebraic specifications in a correct and modular way. Related works for checking ground confluence are based on the completion techniques or on the test that all critical pairs between axioms are valid with respect to a sufficient criterion for ground confluence. It is generally accepted that such techniques may be very inefficient, even for very small specifications. Indeed, the completion procedure often diverges and there often exist many critical pairs of the axioms. In this article, we present a procedure for simultaneously checking completeness and ground confluence for specifications with free/nonfree constructors and parameterized specifications. If the specification is not complete or not ground confluent, then our procedure will output the set of patterns on whose ground instances a function is not defined and it can easily identify the rules that break ground confluence. In contrast to previous work, our method does not rely on completion techniques and does not require the computation of critical pairs of the axioms. The method is entirely implemented and allowed us to prove the completeness and the ground confluence of many specifications in a completely automatic way, where related techniques diverge or generate very complex proofs. Our system offers two main components: (i) a completeness and ground confluence analyzer that computes pattern trees of defined functions and may generate some proof obligations; and (ii) a procedure to prove (joinable) inductive conjectures which is used to discharge these proof obligations.

REFERENCES

• 1: Klaus Becker, Proving Ground Confluence and Inductive Validity in Constructor Based Equational Specifications, Proceedings of the International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.46-60, April 13-17, 1993
• 2: Becker, K. 1996. How to prove ground confluence. SEKI-rep. SR-96-02, Universität Kaiserslautern.
• 3: Adel Bouhoula, Using induction and rewriting to verify and complete parameterized specifications, Theoretical Computer Science, v.170 n.1-2, p.245-276, Dec. 1996 [doi>10.1016/S0304-3975(96)00005-9]
• 4: Adel Bouhoula, Automated theorem proving by test set induction, Journal of Symbolic Computation, v.23 n.1, p.47-77, Jan. 1997 [doi>10.1006/jsco.1996.0076]
• 5: Adel Bouhoula, Simultaneous Checking of Completeness and Ground Confluence, Proceedings of the 15th IEEE international conference on Automated software engineering, p.143, September 11-15, 2000
• 6: Bouhoula, A. and Jacquemard, F. 2007. Verifying regular trace properties of security protocols with explicit destructors and implicit induction. In Proceedings of the Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA-07), 27--44.
• 7: Adel Bouhoula , Jean-Pierre Jouannaud, Automata-driven automated induction, Information and Computation, v.169 n.1, p.1-22, 25 August 2001 [doi>10.1006/inco.2001.3036]
• 8: Adel Bouhoula , Jean-Pierre Jouannaud , José Meseguer, Specification and proof in membership equational logic, Theoretical Computer Science, v.236 n.1-2, p.35-132, April 6, 2000 [doi>10.1016/S0304-3975(99)00206-6]
• 9: Bouhoula, A., Kounalis, E., and Rusinowitch, M. 1995. Automated mathematical induction. J. Logic Comput. 5, 5, 631--668.
• 10: Bouhoula, A. and Rusinowitch, M. 1995. Implicit induction in conditional theories. J. Autom. Reasoning 14, 2, 189--235.
• 11: H Comon, Sufficient completeness, term rewriting systems and “anti-unification”, Proc. of the 8th international conference on Automated deduction, p.128-140, August 1986, Oxford, United Kingdom
• 12: Hubert Comon, Inductive Proofs by Specification Transformation, Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, p.76-91, April 03-05, 1989
• 13: Dershowitz, N. 1983. Well-Founded orderings. Tech. rep. ATR-83-8478-3, Office of Information Sciences Research, The Aerospace Corporation, El Segundo, California. May.
• 14: Nachum Dershowitz, Termination of rewriting, Journal of Symbolic Computation, v.3 n.1-2, p.69-116, Feb./April 1987 [doi>10.1016/S0747-7171(87)80022-6]
• 15: Nachum Dershowitz , Jean-Pierre Jouannaud, Rewrite systems, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 16: Nachum Dershowitz , M. Okada, A rationale for conditional equational programming, Theoretical Computer Science, v.75 n.1-2, p.111-138, Sep. 1990 [doi>10.1016/0304-3975(90)90064-O]
• 17: Nachum Dershowitz , M. Okada , G. Sivakumar, Confluence of conditional rewrite systems, 1st international workshop on Conditional Term Rewriting Systems, p.31-44, August 1988, Orsay, France
• 18: Hartmut Ehrig , B. Mahr, Fundamentals of Algebraic Specification I, Springer-Verlag New York, Inc., Secaucus, NJ, 1985
• 19: L. Fribourg, A strong restriction of the inductive completion procedure, Journal of Symbolic Computation, v.8 n.3, p.253-276, Sep. 1989 [doi>10.1016/S0747-7171(89)80069-0]
• 20: 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]
• 21: H. Ganzinger, Ground term confluence in parametric conditional equational specifications, 4th Annual Symposium on Theoretical Aspects of Computer Sciences on STACS 87, p.286-298, February 1987, Passau, Germany
• 22: R. Göbel, Ground confluence, on Rewriting techniques and applications, p.156-167, May 1987, Bordeaux, France
• 23: Goguen, J. A. and Meseguer, J. 1988. Order-Sorted algebra I: Partial and overloaded operations, errors and inheritance. Tech. rep., SRI International, Computer Science Lab. Given as lecture at a Seminar on Types, Carnegie-Mellon University, June 1983.
• 24: Bernhard Gramlich , Claus-Peter Wirth, Confluence of Terminating Conditional Rewrite Systems Revisited, Proceedings of the 7th International Conference on Rewriting Techniques and Applications, p.245-259, July 27-30, 1996
• 25: Guttag, J. V. and Horning, J. J. 1978. The algebraic specification of abstract data types. Acta Inf. 10, 27--52.
• 26: Gerard Huet , Jean-Marie Hullot, Proofs by induction in equational theories with constructors, Proceedings of the 21st Annual Symposium on Foundations of Computer Science, p.96-107, October 13-15, 1980
• 27: Jean-Pierre Jouannaud , Emmanuel Kounalis, Automatic proofs by induction in theories without constructors, Information and Computation, v.82 n.1, p.1-33, July 1989 [doi>10.1016/0890-5401(89)90062-X]
• 28: S. Kaplan, Simplifying conditional term rewriting systems: unification, termination and confluence, Journal of Symbolic Computation, v.4 n.3, p.295-334, Dec. 1988 [doi>10.1016/S0747-7171(87)80010-X]
• 29: Deepak Kapur, An automated tool for analyzing completeness of equational specifications, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.28-43, August 17-19, 1994, Seattle, Washington, United States [doi>10.1145/186258.186496]
• 30: Deepak Kapur , Paliath Narendran , Friedrich Otto, On ground-confluence of term rewriting systems, Information and Computation, v.86 n.1, p.14-31, May 1990 [doi>10.1016/0890-5401(90)90023-B]
• 31: Kapur, D. and Narendran, P. 1992. Double-Exponential complexity of computing a complete set of AC-unifiers. In Proceedings of the 9th IEEE Symposium on Logic in Computer Science. IEEE.
• 32: Deepak Kapur , Paliath Narendran , Daniel J. Rosenkrantz , Hantao Zhang, Sufficient-completeness, ground-reducibility and their complexity, Acta Informatica, v.28 n.4, p.311-350, April 1991 [doi>10.1007/BF01893885]
• 33: Emmanuel Kounalis, Completeness in Data Type Specifications, Research Contributions from the European Conference on Computer Algebra-Volume 2, p.348-362, April 01-03, 1985
• 34: Emmanuel Kounalis , Michaël Rusinowitch, Studies on the Ground Convergence Property of Conditional Theories, Proceedings of the Second International Conference on Methodology and Software Technology: Algebraic Methodology and Software Technology, p.363-376, May 22-25, 1991
• 35: Wolfgang Küchlin, A Confluence Criterion Based on the Generalised Neman Lemma, Research Contributions from the European Conference on Computer Algebra-Volume 2, p.390-399, April 01-03, 1985
• 36: A. Lazrek , P. Lescanne , J. J. Thiel, Tools for proving inductive equalities, relative completeness, and &ohgr;-completeness, Information and Computation, v.84 n.1, p.47-70, Jan. 1990 [doi>10.1016/0890-5401(90)90033-E]
• 37: Peter Padawitz, The equational theory of parameterized specifications, Information and Computation, v.76 n.2-3, p.121-137, February/March 1988 [doi>10.1016/0890-5401(88)90006-5]
• 38: Plaisted, D. A. 1985. Semantic confluence tests and completion methods. Inf. Control 65, 2-3, 182--215.
• 39: M. Schmidt-SchauΒ, Computational aspects of an order-sorted logic with term declarations, Springer-Verlag New York, Inc., New York, NY, 1989
• 40: Smolka, G., Nutt, W., Goguen, J. A., and Meseguer, J. 1987. Order sorted equational computation. In Proceedings of the Colloquium on Resolution of Equations in Algebraic Structures.
• 41: Jean Jacques Thiel, Stop losing sleep over incomplete data type specifications, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.76-82, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800518]
• 42: Martin Wirsing, Algebraic specification, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.2 Grammars and Other Rewriting Systems
      F.4.3 Formal Languages
          Subjects: Algebraic language theory

General Terms:
Languages, Theory, Verification

Keywords:
Automated deduction, algebraic specifications, completeness, ground confluence, parameterization, term rewriting systems