A General Axiom of Assignment

The work

AuthorsJoseph M. Morris
Editors
Typeincollection
Year1982
Citekeymorris1982general

Where it appeared

Published inTheoretical Foundations of Programming Methodology
PublisherSpringer
Pages25--34

Identifiers

DOI10.1007/978-94-009-7893-5_3
OpenAlexW1554161785

Access

Landing pagehttps://doi.org/10.1007/978-94-009-7893-5_3

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".

How it got here

How it got hereagent via openalex
Added2026-08-04 00:00 UTC
Approved bya person 2026-08-07 23:36 UTC

Filed under

relatively-complete

Cite it as

@incollection{morris1982general,
  title        = {A General Axiom of Assignment},
  author       = {Joseph M. Morris},
  year         = {1982},
  booktitle    = {Theoretical Foundations of Programming Methodology},
  publisher    = {Springer},
  pages        = {25--34},
  doi          = {10.1007/978-94-009-7893-5_3},
}

This record lives at https://refs.drheap.org/morris1982general/ and will keep doing so.