Proving assertions about programs that manipulate data structures

ABSTRACT

In this paper we wish to consider the problem of proving assertions about programs that construct and alter data structures. Our method will be to define a suitable assertion language L for data structures, to define a simple programming language L' for constructing and altering data structures, to give axioms and rules of inference (in the style of [Hoare 1969]) which specify the effect of program segments on data structures (described by formulas in L) and finally to prove that these axioms are correct (relative to a formal definition of the semantics of L') and, in a reasonable sense, complete. Thus our intention is to provide a complete theoretical framework for describing arbitrary data structures and proving assertions about programs that manipulate them.

REFERENCES

• 1: Burstall, R.M. Some Techniques for Proving Correctness of Programs which Alter Data Structures. Machine Intelligence 7, 1972.
• 2: Cook, S.A. Axiomatic and Interpretive Semantics for an Algol Fragment. Technical Report No. 79, Dept. of Computer Science, University of Toronto, February 1975.
• 3: Stephen A. Cook , Derek C. Oppen, An assertion language for data structures, Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.160-166, January 20-22, 1975, Palo Alto, California [doi>10.1145/512976.512993]
• 4: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 5: Hoare, C.A.R. and Lauer, P.E. Consistent and Complementary Formal Theories of the Semantics of Programming Languages. Acta Informatica 3, 1974, pp. 135-153.
• 6: Shigeru Igarashi , Ralph L. London , David C. Luckham, Automatic program verification I: a logical basis and its implementation., Stanford University, Stanford, CA, 1973
• 7: Kowaltowski, T. Correctness of Programs Manipulating Data Structures. Memorandum No. ERL-M404, Electronics Research Laboratory, University of California, Berkeley, September 1973.
• 8: Lauer, P. Consistent Formal Theories of the Semantics of Programming Languages. Techincal Report TR 25.121, IBM Vienna, November 1971.
• 9: Laventhal, M.S. Verification of Programs Operating on Structured Data. M.Sc. Thesis, M.I.T., February 1974.
• 10: Morris, J.H. Verification Oriented Language Design. Technical Report 7, Dept. of Computer Science, University of California, Berkeley, December 1972.
• 11: Derek Charles Oppen, On logic and program verification., 1975
• 12: Rosenberg, A.L. Data Graphs and Addressing Schemes. Journal of Computer and System Sciences, June 1971, pp. 193-238.
• 13: Standish, T.A. Data Structures: An Axiomatic Approach. Automatic Programming Memo 3, Bolt, Beranek and Newman Inc., August 1973.

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: Assertions

Additional Classification:
  E. Data
  E.1 DATA STRUCTURES

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory

General Terms:
Languages, Theory