Data type specification: Parameterization and the power of specification techniques

ABSTRACT

This paper extends our earlier work on abstract data types by providing an algebraic treatment of parametrized data types (e.g., sets-of-(), stacks-of-(), etc.), as well as answering a number of questions on the power and limitations of algebraic specification techniques. In brief: we investigate the “hidden function” problem (the need to include operations in specifications which we want to be hidden from the user); we prove that conditional specifications are inherently more powerful than equational specifications; we show that parameterized specifications must contain “side conditions” (e.g., that finite-sets-of-d requires an equality predicate on d), and we compare the power of the algebraic approach taken here with the more categorical approach of Lehman and Smyth.

REFERENCES

• 1: (1973) (J. A. Goguen, J. W. Thatcher, E. G. Wagner and J. B. Wright) "A Junction between computer science and category theory: 1, Basic definitions and examples," Part 1, IBM Research report RC-4526, Sept 1973.
• 2: (1975) (J. A. Goguen, J. W. Thatcher, E. G. Wagner and J. B. Wright) "Abstract data types as initial algebras and correctness of data representations," Proceedings, Conference on Computer Graphics, Pattern Recognition and Data Structure, May 1975, pp. 89-93.
• 3: 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]
• 4: (1976) (J. W. Thatcher, E. G. Wagner and J. B. Wright) "Specification of abstract data types using conditional axioms," IBM Research Report RC-6214, September 1976.
• 5: (1976a) (J. A. Goguen, J. W. Thatcher, E. G. Wagner) "An initial algebra approach to the specification, correctness, and implementation of abstract data types," IBM Research Report RC-6487, October 1976. To appear, Current Trends in Programming Methodology. IV: Data Structuring(R. Yeh, Ed.) Prentice Hall, New Jersey.
• 6: (1977) (J. B. Wright E. G. Wagner J. W. Thatcher) "A uniform approach to inductive posets and inductive closure." Lecture Notes in Computer Science 53(Mathematical Foundations of Computer Science 1977), pp. 192-212. IBM Research Report RC-6817, October 1977. To appear, Theoretical Computer Science, 1978.
• 7: (1977a) (J. A. Goguen) "Abstract errors for abstract data types," UCLA Semantics Theory of Computation Report #6, February 1977. ProceedingsIFIP Working Conference on Formal Description of Programming Concepts, St. Andrews, New Brunswick, pp. 21.1-21.32, August, 1977.
• 8: D. Brand, A note on data abstractions, ACM SIGPLAN Notices, v.13 n.1, p.21-24, January 1978 [doi>10.1145/953428.953430]
• 9: Burstall, R. M. and Goguen, J. A. (1977) "Putting Theories together to make Specifications," Proceedings1977 IJCAI, MIT, Cambridge, MA., August, 1977.
• 10: Ehrig, H. and Kreowski, H. J. (1977) "Some remarks concerning correct specification and implementation of abstract data types," Technical University of Berlin, Report 77-13, August 1977.
• 11: Ehrig, H., Kreowski, H. J., and Padawitz, P. (1977) "Spezifikation. Korrektheit, und Implementierung von abstrakten Datenstrukturen," Einfurhungsskript zur LV Theorie von Datenstrukturen an der TU Berlin (SS 1977).
• 12: (1977a) "Stepwise specification and implementation of abstract data types," Technical University of Berlin, Report, November 1977.
• 13: Seymour Ginsburg, The Mathematical Theory of Context-Free Languages, McGraw-Hill, Inc., New York, NY, 1966
• 14: Goguen, J. A., and Tardo, J. (1977) "OBJ-0 preliminary users manual," UCLA, Los Angeles, CA. 1977.
• 15: Guttag, J. V. (1975) "The specification and application to programming of abstract data types," Univ. of Toronto, Computer Systems Research Group, Techical Report CSRG-59, September, 1975.
• 16: John Guttag, Abstract data types and the development of data structures, Proceedings of the 1976 conference on Data : Abstraction, definition and structure, p.72, March 22-24, 1976, Salt Lake City, Utah, United States
• 17: Guttag, J. V. (1977) "The algebraic specification of abstract data types," USC Computer Science Department, Draft Manuscript, April, 1977.
• 18: Guttag, J. V., Horowitz, E., and Musser, D. R. (1976) "Abstract data types and software validation," Information Sciences Institute, Report RR-76-48 (Marina del Rey, Calif.).
• 19: Guttag, J. V., Horowitz, E., and Musser, D. R. (1976a) "The design of data type specifications," Information Sciences Institute, Report RR-76-48 (Marina del Rey, Calif.).
• 20: Jhon V. Guttag , Ellis Horowitz , David R. Musser, Some extensions to algebraic specifications, Proceedings of an ACM conference on Language design for reliable software, p.63-67, March 28-30, 1977, Raleigh, North Carolina
• 21: Hilfinger, Paul N. (1978) Correspondence from Members, SIGPLAN NOTICES, 13, January, 1978 pp 11-12.
• 22: Hoare, C. A. R. (1972) "Proof of Correctness of Data Representations," Acta Informatica 1, (1972) pp. 271-281.
• 23: Ellis Horowitz , Sartaj Sahni, Fundamentals of data structures in PASCAL, Computer Science Press, Inc., New York, NY, 1984
• 24: D. J. Lehmann , M. B. Smyth, Data Types, University of Warwick, Coventry, UK, 1977
• 25: Lehman, D. J. and Smyth, M. B. (1977a) "Data Types," Proceedings18th IEEE Symposium on Foundations of Computing, Providence, R.I., November 1977, pp. 7-12,
• 26: Liskov, B. H. and Berzins, V. (1977) "An appraisal of program specification," MIT, Laboratory for Computer Science, Computation Structures Memo 141-1, April, 1977.
• 27: Majster, M. E. (1977) "Data types, abstract data types and their specification problem," Technical University of Munich, Report TUM-INFO-7740, August 1977.
• 28: Limits of the "algebraic" specification of abstract data types, ACM SIGPLAN Notices, v.12 n.10, p.37-42, October 1977 [doi>10.1145/954627.954630]
• 29: Majster, M. E. (1978)Correspondence from Members, SIGPLAN NOTICES, 13, January, 1978 pp 8-10. (1978)
• 30: Marvin Lee Minsky, Computation: Finite and Infinite Machines, Prentice-Hall, Inc., Upper Saddle River, NJ, 1967
• 31: James H. Morris, Jr., Types are not sets, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.120-124, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512938]
• 32: Scott, Dana (1972) "Continuous Lattices," Lecture Notes in Mathematics 274 (1972) pp. 97-136.
• 33: (1972a) "Data types as lattices," unpublished notes, Amsterdam (1972); Oxford (1974). SIAM J. Computing 5 (1976), pp. 522-587.
• 34: Spitzen, J. and (1975) Wegbreit, B. "The verification and synthesis of data structures," Acta Informatica 4, (1975) pp. 127-144.
• 35: Tarski, A. (1968) "Equational logic and equational theories of algebras," Contributions to Mathematical Logic(K. S.chütte, Ed), North Holland, Amsterdam, 1968.
• 36: Zilles, S. N. (1975) "An introduction to data algebras," working draft paper, IBM Research, San Jose, September, 1975.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Bounded-action devices (e.g., Turing machines, random access machines)

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Parallelism and concurrency

General Terms:
Theory