A General Axiom of Assignment

The work

TitleA General Axiom of Assignment
AuthorsJoseph M. Morris
Typechapter in a collection
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".

Where this came from

How it got herethe agent went looking · found via openalex
First seen2026-08-04
Standingendorsed
Approved2026-08-07

Cite it as

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

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