A General Axiom of Assignment

  • Joseph M. Morris
Part of the NATO Advanced Study Institutes Series book series (ASIC, volume 91)

Abstract

The axiomatic method of Floyd [1] and Hoare [2] has become the most popular formal method for reasoning about programs. Axiomatic semantics, more or less complete, exist for various programming languages [3, 4] and the method is widely used in deriving and verifying programs. Some areas of programming, however, have thus far defied a general axiomatic treatment. One such area is that of pointers and linked data structures, which will be the subject of this and the following two papers. The goal is to make manageable the formal verification of list-processing programs, using axiomatic semantics. The present work does not claim to be complete, but is more systematic than previous treatments [5, 6, 7, 8], and is more general. These advantages accrue from the use of Dijkstra’s “weakest preconditions” [9] rather than Hoare’s “sufficient preconditions”.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    Floyd, R.W.: Assigning Meanings to Programs, Proc. Symp. in Applied Mathematics, Vol. 19, J.T. Schwartz (ed.), American Mathematical Society, 1967, pp. 19–32.Google Scholar
  2. [2]
    Hoare, C.A.R.: An Axiomatic Basis for Computer Programming, Comm. ACM, Vol. 12, No. 10, October 1969, pp. 576–580,MATHCrossRefGoogle Scholar
  3. [2]
    Hoare, C.A.R.: An Axiomatic Basis for Computer Programming, Comm. ACM, Vol. 12, No. 10, October 1969, pp. 583.CrossRefGoogle Scholar
  4. [3]
    Hoare, C.A.R., and Wirth, N.: An Axiomatic Definition of the Programming Language Pascal, Acta Informatica, Vol. 2, No. 4, 1973, pp. 335–355.CrossRefGoogle Scholar
  5. [4]
    London, R.L., Guttag, J.V., Horning, J.J., Lampson, B.W., Mitchell, J.G., and Popek, G.J.: Proof Rules for the Programming Language Euclid, Acta Informatica, Vol. 10, 1978, pp. 1–26.MATHCrossRefGoogle Scholar
  6. [5]
    Burstall, R.M.: Some Techniques for Proving Correctness of Programs which Alter Data Structures, Machine Intelligence 7, D. Michie (ed.)., American Elsevier, New York, 1972, pp. 23–50.Google Scholar
  7. [6]
    Kowaltowski, T.: Data Structures and Correctness of Programs, Jrnl. ACM, Vol. 26, No. 2, 1979, pp. 283–301.MathSciNetMATHCrossRefGoogle Scholar
  8. [7]
    Laventhal, M.S.: Verifying Programs which Operate on Data Structures, Proc. Int. Conf. on Reliable Software, 1975, pp. 420–426.Google Scholar
  9. [8]
    Luckham, D.C., and Suzuki, N.: Verification of Array, Record, and Pointer Operations in Pascal, ACM Trans. Programming Languages and Systems, Vol. 1, No. 2, 1979, pp. 226–244.MATHCrossRefGoogle Scholar
  10. [9]
    Dijkstra, E.W.: A Discipline of Programming, Prentice-Hall, Englewood Cliffs, N.J., 1976.MATHGoogle Scholar
  11. [10]
    Gries, D.: The Multiple Assignment Statement, IEEE Trans. Software Engineering, Vol. SE-4, No. 2, 1978, pp. 89–93.CrossRefGoogle Scholar

Copyright information

© D. Reidel Publishing Company 1982

Authors and Affiliations

  • Joseph M. Morris
    • 1
  1. 1.Dept. of Computer ScienceTrinity CollegeDublin 2Ireland

Personalised recommendations