Algorithmic specifications: a constructive specification method for abstract data types

ABSTRACT

This paper presents a new specification method for abstract data types and a pertaining logic. The specification method proposed differs from the classical algebraic one by its constructive, yet abstract nature. Although it leads to a different style in specification, the method avoids some fundamental problems inherent in the algebraic specification method. The logic proposed is essentially a first-order logic for strict (partial) functions. It allows in particular the expression of the semantic conditions guaranteeing the consistency of a specification.

REFERENCES

• 1: BALZER, M. Algorithmische spezifikationen abstrakter datentypen am beispiel der strukturen aus informatik I und II. Master's thesis, FB 10, Universit~it Saarbrfcken, Saarbr~icken, West Germany, (1983).
• 2: BEIERLE, C. Algebraic implementations in an integrated software development and verification system. PhD dissertation, Fachbereich Informatik, Universit~it Kaiserslautern, (1985).
• 3: BERGSTRA, J. A., AND TUCKER, J.V. Initial and final algebra semantics for data type specifications: Two characterization theorems. SIAM J. Cornput. 12, 2 (1983), 366-387.
• 4: Jan A. Bergstra , Manfred Broy , J. V. Tucker , Martin Wirsing, On the Power of Algebraic Specifications, Proceedings on Mathematical Foundations of Computer Science, p.193-204, August 31-September 04, 1981
• 5: Michel Bidoit , Brigitte Biebow , Marie-Claude Gaudel , Christian Gresse , Gérard D. Guiho, Exception handling: formal specification and systematic program construction, IEEE Transactions on Software Engineering, v.11 n.3, p.242-252, March 1985 [doi>10.1109/TSE.1985.232207]
• 6: BOYER, R. S., AND MOORE, J.S. A Computational Logic. Academic Press, New York, 1979.
• 7: Manfred Broy , Martin Wirsing, On the Algebraic Extensions of Abstract Data Types, Proceedings of the International Colloquium on Formalization of Programming Concepts, p.244-251, April 19-25, 1981
• 8: BROY, M., AND WIRSlNO, M. Partial abstract types. Acta Inf. 18 (1982), 47-64.
• 9: M. Broy , M. Wirsing , C. Pair, A systematic study of models of abstract data types, Theoretical Computer Science, v.33 n.2-3, p.139-174, Oct., 1984 [doi>10.1016/0304-3975(84)90086-0 ]
• 10: BURSTALL, R. M., AND GOOUEN, J. A. Putting theories together to make specifications. In Proceedings of 5th Joint Conference on Artificial Intelligence. (Cambridge, 1977), 1045-1058.
• 11: Rod M. Burstall , Joseph A. Goguen, The Semantics of CLEAR, A Specification Language, Proceedings of the Abstract Software Specifications, 1979 Copenhagen Winter School, p.292-332, January 22-February 02, 1979
• 12: CARTWRIGHT, R. A practical formal semantic definition and verification system for TYPED LISP. Stanford A.I. Memo, AIM-296, Stanford University, Stanford, Calif., (1976).
• 13: CARTWRIGHT, R. User-defined data types as an aid to verifying LISP-programs. In Proceedings of the International Colloquium on Languages and Programming (Edinburgh, 1976). S. Michaelson and R. Milner, Eds., Edinburgh Press, Edinburgh, Scotland, U.K. 1976, pp. 228-256.
• 14: Robert Cartwright, A constructive alternative to axiomatic data type definitions, Proceedings of the 1980 ACM conference on LISP and functional programming, p.46-55, August 25-27, 1980, Stanford University, California, United States [doi>10.1145/800087.802789]
• 15: Robert Cartwright, Toward a Logical Thoery of Program Data, Logic of Programs, Workshop, p.37-51, May 01, 1981
• 16: 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]
• 17: H.-D. Ehrich, On the Theory of Specification, Implementation, and Parametrization of Abstract Data Types, Journal of the ACM (JACM), v.29 n.1, p.206-227, Jan. 1982 [doi>10.1145/322290.322303]
• 18: Hartmut Ehrig , B. Mahr, Fundamentals of Algebraic Specification I, Springer-Verlag New York, Inc., Secaucus, NJ, 1985
• 19: 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]
• 20: Harald Ganzinger, Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.3, p.318-354, July 1983 [doi>10.1145/2166.357212]
• 21: GOGOLLA, M., DROSTEN, K., LIPECK, U., AND EHRICH, H.-D. Algebraic and operational semantics of specifications allowing exceptions and errors. Theor. Comput. ScL 34, 3 (1984), 289-314.
• 22: GOGUEN, J., AND MESEGUER, J. Order-sorted algebra I: Partial and overloaded operators, errors, and inheritance. Int. Rep., SRI International, Computer Science Laboratory (1984).
• 23: GOOUEN, J. A., THATCHER, J. W., AND WAONER, E. G. An initial algebra approach to the specification, correctness and implementation of abstract data types. Current Trends in Programruing Methodology IV, R., Yeh, Ed. Prentice-Hall, Englewood Cliffs, N.J., 1978, pp. 80-149.
• 24: GUTTAO, J. V., AND HORNING, J.J. The algebraic specifications of abstract data types. Acta In{. 10, 1 (1978), 27-52.
• 25: J V Guttag , J J Horning, Report on the Larch shared language, Science of Computer Programming, v.6 n.2, p.103-134, March 1986
• 26: John V. Guttag , Ellis Horowitz , David R. Musser, Abstract data types and software validation, Communications of the ACM, v.21 n.12, p.1048-1064, Dec. 1978 [doi>10.1145/359657.359666]
• 27: HARPER, R., MACQUEEN, D., AND MILNER, R. Standard ML. Tech. Rep. ECS-LFCS-86-2, University of Edinburgh, Edinburgh, Scotland, U.K. (1986).
• 28: HOARE, C. A.R. Proof of correctness of data representations. Acta Inf. 1, 4 (1972), 271-281.
• 29: Samuel Kamin, Final Data Types and Their Specification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.1, p.97-121, Jan. 1983 [doi>10.1145/357195.357202]
• 30: KLAEREN, H.A. Algebraische Spezifikationen. Springer Verlag, New York, 1983.
• 31: Herbert A. Klaeren, A constructive method for abstract algebraic software specification, Theoretical Computer Science, v.30 n.2, p.139-204, March 1984 [doi>10.1016/0304-3975(84)90062-8 ]
• 32: KLEENE, S.C. Mathematical Logic. Wiley, New York, 1967.
• 33: LEHMANN, D., AND SMYTH, M. The algebraic specification of data types: A synthetic approach. Math. Syst. Theor. 14 (1981), 97-139.
• 34: LEHMANN, W., AND LOECKX, J. The notion of implementation in the algorithmic specification method. Int. Rep. FB 10, Universit~t Saarbriicken (to be published).
• 35: LEHMANN, T., AND LOECKX, J. Obscure, a specification environment for abstract data types. Int. Rep. A06/87, FB 10, Universi~t Saarbriicken, Saarbriicken, West Germany (1987).
• 36: B. Liskov , R. R. Atkinson , T. Bloom , E. B. Moss , R. Schaffert , A. Snyder, CLU REFERENCE MANUAL, Massachusetts Institute of Technology, Cambridge, MA, 1979
• 37: LOECKX, J. Proving properties of algorithmic specifications of abstract data types in AFFIRM. AFFIRM-Memo-29-JL, University of Southern California-ISI, Marina del Rey, Calif. (1980).
• 38: Jacques Loeckx, Algorithmic Specifications of Abstract Data Types, Proceedings of the 8th Colloquium on Automata, Languages and Programming, p.129-147, July 13-17, 1981
• 39: LOECKX, J. Using abstract data types for the definition of programming languages and the verification of their compilers. Int. Rep. A 81/13 FB 10, Universit~it Saarbrhcken, Saarbriicken, West Germany, (1981).
• 40: LOECKX, J., AND LE~IMANN, T. A formal description of the specification language OBSCURE. Int. Rep. A 07/87 FB 10, UniversitAt Saarbriicken, Saarbriicken, West Germany, 1987.
• 41: Jacques Loeckx , Kurt Sieber, The foundations of program verification (2nd ed.), John Wiley & Sons, Inc., New York, NY, 1987
• 42: Zohar Manna, Introduction to Mathematical Theory of Computation, McGraw-Hill, Inc., New York, NY, 1974
• 43: J Meseguer , J A Goguen, Initiality, induction, and computability, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• 44: Robin Milner, Implementation and applications of Scott's logic for computable functions, Proceedings of ACM conference on Proving assertions about programs, p.1-6, January 06-07, 1972, Las Cruces, New Mexico, United States
• 45: MUSSER, D.R. Abstract data type specification in the AFFIRM System. IEEE Trans. Softw. Eng. SE-6 (1980), 24-32.
• 46: R. Nakajima , T. Yuasa, Iota Programming System, Springer-Verlag New York, Inc., Secaucus, NJ, 1983
• 47: OYAMAGUCHI, M. On the data type extension problem for algebraic specifications. Theor. Comput. Sci. 35, 2 + 3 (1985), 329-336.
• 48: REICHEL, H. Structural Induction on Partial Algebras. Akademie-Verlag, Berlin, GDR, 1984.
• 49: SANNELLA, D. A set-theoretic semantics for CLEAR. Acta In{. 21, 5 (1984), 443-472.
• 50: D Sannella , A Tarlecki, On observational equivalence and algebraic specification, Proc. of the international joint conference on theory and practice of software development (TAPSOFT) Berlin, March 25-29, 1985 on Mathematical foundations of software development, Vol. 1: Colloquium on trees in algebra and programming (CAAP'85), p.308-322, April 1985, Berlin, Germany
• 51: Donald Sannella , Andrzej Tarlecki, Program specification and development in standard ML, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.67-77, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318614]
• 52: SCHOE?T, O. Behavioural correctness of data representations. Int. Pep. CSR-185-85, University of Edinburgh, Edinburgh, Scotland, U.K. (1985).
• 53: SHAW, M.Ed. ALPHARD, Form and Content. Springer-Verlag, New York, 1981.
• 54: J. W. Thatcher , E. G. Wagner , J. B. Wright, Data Type Specification: Parameterization and the Power of Specification Techniques, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.4, p.711-732, Oct. 1982 [doi>10.1145/69622.357192]
• 55: THOMPSON, D. H., Ed. AFFIRM Re{erence Manual. Int. Rep., University of Southern California-ISI, Marina del Rey, Calif. (1979).
• 56: TREINEN, R. Ein Kalkiil fiir algorithmische Spezifikationen. Master's thesis, FB 10, Universit/it Saarbmcken, Saarbriicken, West Germany (1986).
• 57: UHmG, S. Die formale Verifikation eines einfachen 'l~,ersetzers. Master's thesis, FB 10, Universitiit Saarbrficken, Saarbr(icken, West Germany (1986).
• 58: Friedrich W. von Henke, On the representation of data structures in LCF with applications to program generation., Stanford University, Stanford, CA, 1975
• 59: Voss, A. Algebraic implementations in an integrated software development and verification system. Ph.D. dissertation, Fachbereich Informatik, Uniiversit~it Kaiserslautern, West Germany 1985.
• 60: WAND, M. Final algebra semantics and data type extensions. J. Comput. Syst. Sci. 19, 1 (1979).

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Abstract data types

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Methodologies (e.g., object-oriented, structured)
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Languages, Theory, Verification