Stop losing sleep over incomplete data type specifications

ABSTRACT

We give an algorithm to test the completeness of definitions holding on the rewrite systems that they generate. At the opposite of existing techniques that are very restrictive (left-hand sides of definitions must be linear) or rather inefficient our solution is both powerful and efficient. Also, the algorithm that we give detects ambigous or/and incomplete definitions and can tell you why they are ambigous or/and incomplete. It applies too to definitions in presence of equations.

REFERENCES

• 1: Bidoit M. "Une Methode de Presentation des Types Abstraits: Applications" These de 3-eme cycle Universite de Paris Sud, Orsay - 1981 -
• 2: Dershowitz N. "Computing with Rewrite Systems" - 1982 -
• 3: John V. Guttag , Ellis Horowitz , David R. Musser, The design of data type specifications, Proceedings of the 2nd international conference on Software engineering, p.414-420, October 13-15, 1976, San Francisco, California, United States
• 4: Padawitz P. "Correctness, Completeness and Consistency of Equational Data Type Specifications" Ph.D. Thesis Technische Universitat Berlin - 1983 -
• 5: Hullot J.M. "Compilation de Formes Canoniques dans les Theories Equationnelles" These de 3-eme cycle Universite de Paris Sud, Orsay - 1980 -
• 6: Huet G. - Hullot J.M. "Proofs by induction in equational theories with constructors" Proc. 21th FOCS - 1980 - Also, JCSS 25-2 - 1982 -
• 7: Gerard Huet , Derek C. Oppen, Equations and rewrite rules: a survey, Stanford University, Stanford, CA, 1980
• 8: Jouannaud J.P. "Church-Rosser Computation with Equational Term Rewriting Systems" Centre de Recherche en Informatique de Nancy - 1983 -
• 9: Lescanne P. "Computer Experiments with the REVE Term Rewriting Generator" Centre de Recherche en Informatique de Nancy and Laboratory of Computer Science, M.I.T. - 1983 -

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.2 Grammars and Other Rewriting Systems
          Subjects: Parallel rewriting systems (e.g., developmental systems, L-systems)

General Terms:
Algorithms, Languages, Theory

Keywords:
Completeness, Data types specifications, Equational theories, Substitutions, Term rewriting systems, Unification