Abstract data types and software validation

ABSTRACT

A data abstraction can be naturally specified using algebraic axioms. The virtue of these axioms is that they permit a representation-independent formal specification of a data type. An example is given which shows how to employ algebraic axioms at successive levels of implementation. The major thrust of the paper is twofold. First, it is shown how the use of algebraic axiomatizations can simplify the process of proving the correctness of an implementation of an abstract data type. Second, semi-automatic tools are described which can be used both to automate such proofs of correctness and to derive an immediate implementation from the axioms. This implementation allows for limited testing of programs at design time, before a conventional implementation is accomplished.

REFERENCES

• 1: 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]
• 2: DaM, O.-J. The SIMULA 67 common base language. Norwegian Comput. Ctr., Oslo, 1968.
• 3: Goguen, J.A., Thatcher, J.W., Wagner, E.G., and Wright, J.B. Abstract data-types as initial algebras and correctness of data representations. Proc. Conf. on Comptr. Graphics, Pattern Recognition and Data Structure, May 1975.
• 4: Good, D.I., London, R.L, and Bledsoe, W.W. An interactive program verification system. IEEE Trans. Software Eng. SE-1, 1 (March 1975), 56-67.
• 5: Guttag, J.V., Horowitz, E., and Musser, D. The design of data type specifications. In Current Trends in Programming Methodology, R.T. Yah, Ed., Prentice-Hall, Englewood Cliffs, N.J., 1978, pp. 60-79.
• 6: 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
• 7: John Guttag, Abstract data types and the development of data structures, Communications of the ACM, v.20 n.6, p.396-404, June 1977 [doi>10.1145/359605.359618]
• 8: Guttag, J.V., and Homing, J.J. The algebraic specification of abstract data types. Acta lnformatica 10, 1 (1978), 27-52.
• 9: Hoare, C.A.R. Proof of correctness of data representations. Acta Informatica 4 (1972), 271-281.
• 10: Hoare, C.A.R., and Wirth, N. An axiomatic definition of the programming language PASCAL. Acta Informatica 2 (1973), 335-355.
• 11: Hoare, C.A.R. Recursive data structures, lnt. J. Comptr. and Inform. Sci. 4, 2 (June 1975), 105-132.
• 12: Horowitz, E., and Salmi, S. Fundamentals of Data Structures. Computer Science Press, June 1976.
• 13: R. D. Jenks, The SCRATCHPAD language, Proceedings of the ACM SIGPLAN symposium on Very high level languages, p.101-111, March 28-29, 1974, Santa Monica, California, United States
• 14: Barbara Liskov , Alan Snyder , Russell Atkinson , Craig Schaffert, Abstraction mechanisms in CLU, Communications of the ACM, v.20 n.8, p.564-576, Aug. 1977 [doi>10.1145/359763.359789]
• 15: Zohar Manna, Mathematical Theory of Computation, Dover Publications, Incorporated, 2003
• 16: McCarthy, J. Basis for a mathematical theory of computation. In Computer Programming and Formal Systems, P. Braffort and D. Hirchberg, Eds., North-Holland Publ. Co., Amsterdam, 1963, pp. 33-70.
• 17: Musser, D.R. A data type verification system based on rewrite rules. Proc. of Sixth Texas Conf. of Comput. Syst., Austin, Tex., Nov. 1977.
• 18: Palme, J. Protected program modules in SIMULA 67. FOAP Rep. No. C8372-M3(E5), Research Inst. of National Defense, Stockholm, 1973.
• 19: Parnas, D. L. Information distribution aspects of design methodology. Information Processing 71, 1 (1972), North-Holland Pub. Co., Amsterdam, 339-344.
• 20: Spitzen, J., and Wegbreit, B. The verification and synthesis of data structures. Acta Informatica 4 (1975), 127-144.
• 21: Standish, T.A. Data structures: an axiomatic approach. BBN Rep. No. 2639, Bolt Beranek and Newmann, Cambridge, Mass., 1973.
• 22: Norihisa Suzuki, Automatic verification of programs with complex data structure., 1976
• 23: Ben Wegbreit , Jay M. Spitzen, Proving Properties of Complex Data Structures, Journal of the ACM (JACM), v.23 n.2, p.389-396, April 1976 [doi>10.1145/321941.321957]
• 24: Wulf, W.A., London, R.L., and Shaw, M. An introduction to the construction and verification of Alphard programs. IEEE Trans. Software Eng. SE-2, 4 (December 1976), 253-265.
• 25: Zilles, S. N. Abstract specifications for data types. IBM Res. Lab., San Jose, Calif., 1975.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Abstract data types

General Terms:
Design, Languages, Performance, Reliability, Theory, Verification

Keywords:
abstract data type, correctness proof, data structure, data type, specification