Advertisement

Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

The verification and synthesis of data structures

Summary

The concept of machine extension is a commonly used technique for implementing complex software: sets of object classes and operations on these objects are defined and used, often in a layered fashion, to construct the system. This paper addresses the adaptation of this technique to automatic programming. It discusses how such sets of data structures may be precisely specified, presents an axiomatization of a programming language suitable for machine verification, and shows how programs which realize these data structures may be proved correct. A range of data type classes is treated—including arrays, records, and pointers. Some new verification rules are presented to handle programs which use assignments and structured objects.

This is a preview of subscription content, log in to check access.

References

  1. 1.

    Deutsch, L. P.: An interactive program verifier. Computer Science Department, University of California at Berkeley, Ph.D. Thesis, 1973

  2. 2.

    Floyd, R. W.: Toward intercative design of correct programs. Proc. IFIP Congress 71. Amsterdam: North Holland 1972 (p. 7–10)

  3. 3.

    Good, D. I.: Toward a man-machine system for proving program correctness. Computation Center, The University of Texas at Austin, TSN-11, June 1970

  4. 4.

    Green, C.: The application of theorem proving to question answering systems. Stanford University, Ph.D. Thesis, June 1969

  5. 5.

    Hoare, C. A. R.: Proof of correctness of data representations. Acta Informatica 1, 271–281 (1972)

  6. 6.

    Hoare, C. A. R., Wirth, N.: An axiomatic definition of the programming language Pascal. Acta Informatica 2, 335–355 (1973)

  7. 7.

    Igarashi, S., London, R. L., Luckham, D. C.: Automatic program verification I: A logical basis and its implementation. Computer Science Dept., Stanford University, CS-73-365, May 1973. Also in: Acta Informatica 4, 145–182 (1975)

  8. 8.

    King, J.C.: A program verifier September 1969 Pittsburgh (Pa.), Ph.D. Thesis 1969. Computer Science Dept., Carnegie-Mellon University, September 1969

  9. 9.

    Kowalski, R.: An improved theorem-proving system for first-order logic. Dept. of Computational Logic. University of Edinburgh, Memo No. 65, 1973

  10. 10.

    Kowalski, R.: Predicate logic as a programming language. Dept. of Computational Logic, University of Edinburgh, Memo No. 70, 1973

  11. 11.

    Manna, Z., Waldinger, R. J.: Toward automatic program synthesis. Comm. ACM 14, 151–165 (1971)

  12. 12.

    Standish, T.: Data structures, an axiomatic approach. Bolt Beranek and Newman, Inc., Cambridge (Mass.), BBN Report #2639, August 1972

  13. 13.

    Wegbreit, B. et al.: The ECL programmers manual. Center for Research in Computing Technology, Harvard University, 21–72 September 1972

Download references

Author information

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Spitzen, J., Wegbreit, B. The verification and synthesis of data structures. Acta Informatica 4, 127–144 (1975). https://doi.org/10.1007/BF00288745

Download citation

Keywords

  • Information System
  • Operating System
  • Data Structure
  • Communication Network
  • Information Theory