A General Axiom of Assignment
The axiomatic method of Floyd  and Hoare  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”  rather than Hoare’s “sufficient preconditions”.
Unable to display preview. Download preview PDF.
- 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
- 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
- Laventhal, M.S.: Verifying Programs which Operate on Data Structures, Proc. Int. Conf. on Reliable Software, 1975, pp. 420–426.Google Scholar