Proving Properties of Complex Data Structures

ABSTRACT

This paper is concerned with proving properties of programs which use data structures. The goal is to be able to prove that all instances of a class (e.g. as defined in Simula) satisfy some property. A method of proof which achieves this goal, generator induction, is studied and compared to other proof rules and methods: inductive assertions, recursion induction, computation induction, and, in some detail, structural induction. The paper concludes by using generator induction to prove a characteristic property of an implementation of hashtables.

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: BUItSTALL, R.M. Proving properties of programs by structural induction. Computer J. 12, 1 (Feb. 1969), 41-48.
• 3: C~RV, H.B., AND FErs, R. Combinatorg Logw. North-Holland Pub. Co., Amsterdam, 1958.
• 4: DA~L, O.J., MYHRHAUG, B., AND NYOAARD, K. Common base language. S-22, Norwegian Comput. Center, Oslo, Norway, Oct. 1970.
• 5: D,~HL, O.J., DIJKSTaA, E.W., ANy HOARE, C.A R. Structured Programming. Academic Press, New York, N.Y., 1972.
• 6: DEUTSCH, L.P. An interactive program verifier. Ph.D. Thesis, Dep. of Comput. Sci., U. of California at Berkeley, 1973.
• 7: FLOYD, R.W. Assigning meanings to programs. In Mathematical Aspects of Computer Science, J.T. Schwartz, Ed., Amer. Math. Soc., 1967, pp. 19-32.
• 8: Goov, D.I., LosvoN, R.L., AND BLEDSOS, W.W. An interactive program verification system. 1EEE Trans. on Software Eng. SE.I, 1 (March 1975), 59--67.
• 9: HoA~E, C.A.R. Proof of correctness of data representations. Acta lnformatica 1, 4 (1972), 271-281.
• 10: HOARS, C.A.R Procedures and parameters: An axiomatic approach. In Symposmm on Semantics of Algorithmic Languages, E. Engeler, Ed., Springer-Verlag, Berlin, Heidelberg, New York, 1970, pp. 102-116.
• 11: Barbara Liskov , Stephen Zilles, Programming with abstract data types, Proceedings of the ACM SIGPLAN symposium on Very high level languages, p.50-59, March 28-29, 1974, Santa Monica, California, United States
• 12: LUCKHAM, D.C., PARK, D.M.R, AND PATERSON, M.S. On formalized computer programs. J. Comput. Syst. Scis. 4 (1970), 220-249.
• 13: McCARTHY, J. A bas~s for a mathematical theory of computation. In Com~uter Programme'nO and Formal Systems, P. Braffort and D. Hirschberg, Eds., North-Holland, Amsterdam, 1963 pp. 33-70.
• 14: MCCARTHY, J., XND PAINTER, J.A. Correctness of a compiler for arithmetic expressions. In Mathematical Aspects of Computer Science, J.T. Schwartz, Ed., Amer. Math. Soc., 1967, pp. 33-41.
• 15: Zohar Manna , Stephen Ness , Jean Vuillemin, Inductive methods for proving properties of programs, Communications of the ACM, v.16 n.8, p.491-502, Aug. 1973 [doi>10.1145/355609.362336]
• 16: MOOR~, JS. Introducing Prog into the pure Lisp theorem prover. CSL-74-3, Xerox Palo Alto Research Center, Palo Alto, Calif, Dec. 1974.
• 17: James H. Morris, Jr., Protection in programming languages, Communications of the ACM, v.16 n.1, p.15-21, Jan. 1973 [doi>10.1145/361932.361937]
• 18: 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]
• 19: PALME, J. Protected program modules in Simula 67. Research Inst. of National Defense, Stockholm, Sweden, July 1973.
• 20: William Robert Price, Implications of a virtual memory mechanism for implementing protection in a family of operating systems, 1973
• 21: SPITZEN, J, AND WEGBRmT, B. The verfficatmn and synthesis of data structures. Acta Informalica 4 (1975), 127-144.
• 22: VAN WIJNGAKRTEN, A.V., ET AL. Report on the algorithmic language Algol 68. Numer. Math. I$ (1969), 79--218.
• 23: W~tLDINGE~, R.J., AND L~vI~r, K.N. Reasoning about programs. Artif. lntell. 5, 3 (Fall 1974), 255-316.
• 24: Ben Wegbreit, The treatment of data types in EL1, Communications of the ACM, v.17 n.5, p.251-264, May 1974 [doi>10.1145/360980.360992]
• 25: Niklaus Wirth , C. A. R. Hoare, A contribution to the development of ALGOL, Communications of the ACM, v.9 n.6, p.413-432, June 1966 [doi>10.1145/365696.365702]
• 26: WULF, W.A ALPHARD: Toward a language to support structured programs. Comput. Sci. Dep., Carnegie-Mellon U., Pittsburgh, Pa., April 1974.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  E. Data

General Terms:
Theory, Verification