A constructive alternative to axiomatic data type definitions

ABSTRACT

Many computer scientists advocate using axiomatic methods (such as algebraic specification) to specify a program data domain—the universe of abstract data objects and operations manipulated by a program. Unfortunately, correct axiomatizations are difficult to write and to understand. Furthermore, their non-constructive nature precludes automatic implementation by a language processor. In this paper, we present a more disciplined, purely constructive alternative to axiomatic data domain specification. Instead of axiomatizing the program data domain, the programmer explicitly constructs it by using four type construction mechanisms: constructor generation, union generation, subset generation, and quotient generation. These mechanisms are rich enough to define all of the abstract data objects that programmers commonly use: integers, sequences, trees, sets, arrays, functions, etc. In contrast to axiomatic definitions, constructive definitions are easy to write and to understand. An unexpected advantage of the constructive approach is a limited capacity to support non-deterministic operations. As an illustration, we define a non-deterministic “choose” operation on sets.

REFERENCES

• 1: ADJ (J. Goguen, J. Thatcher, E. Wagner) (1976) An Initial Algebra Approach to the Specification, Correctness, and Implementation of Abstract Data Types, IBM Research Report RC 6487.
• 2: J. A. Goguen , J. W. Thatcher , E. G. Wagner , J. B. Wright, Initial Algebra Semantics and Continuous Algebras, Journal of the ACM (JACM), v.24 n.1, p.68-95, Jan. 1977 [doi>10.1145/321992.321997]
• 3: Robert S. Boyer , J. Strother Moore, Proving Theorems about LISP Functions, Journal of the ACM (JACM), v.22 n.1, p.129-144, Jan. 1975 [doi>10.1145/321864.321875]
• 4: Cartwright, R. (1976): User-Defined Data Types as Aid to Verifying LISP Programs, in S. Michaelson and R. Milner (eds.), Automata Languages, and Programming, pp. 228-256, Edinburgh Press, Edinburgh.
• 5: Robert Cartwright , John McCarthy, First order programming logic, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.68-80, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567759]
• 6: Enderton, H. B. (1972): A Mathematical Introduction to Logic, Academic Press, New York.
• 7: Guttag, J. V. et. al. (1976): Abstract Data Types and Software Validation, USC Information Sciences Institute Technical Report ISI/RR-76-48.
• 8: Guttag, J. V. (1977): Abstract Data Types and the Development of of Data Types, Acta Informatica 10, 27-52.
• 9: Guttag, J. V. and J. J. Horning (1978): The Algebraic Specification of Data Structures, Comm. ACM 20, 396-404.
• 10: Friedrich W. von Henke , David C. Luckham, Automatic program verification III: a methodology for verifying programs., Stanford University, Stanford, CA, 1974
• 11: Hoare, C. A. R. (1972): Proofs of Correctness of Data Representation, Acta Informatica 1, 271-281.
• 12: Hoare, C. A. R. (1973): Recursive Data Types, Stanford Artificial Intelligence Project Memo AIM-223.
• 13: McCarthy, J. (1963): A Basis for a Mathematical Theory of Computation, in P. Braffort and D. Hirschberg (eds.), Computer Programming and Formal Systems), pp. 33-70. North-Holland Publishing Company, Amsterdam.
• 14: 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]
• 15: Scott, D. (1976): Data Types as Lattices, SIAM J. Comput. 5, 522-586.
• 16: Spitzen, J. and B. Wegbreit (1975): The Verification and Synthesis of Data Structures, Acta Informatica 4, 127-144.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.11 Software Architectures
            Subjects: Domain-specific architectures

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: LISP
      D.3.3 Language Constructs and Features
          Subjects: Classes and objects

General Terms:
Languages