On the completeness of the inductive assertion method
The work
| Authors | Jacobus W. de Bakker; Lambert G. L. T. Meertens |
|---|---|
| Editors | |
| Type | article |
| Year | 1975 first published 1973 |
| Citekey | bakker1975completeness |
Where it appeared
| Published in | Journal of Computer and System Sciences |
|---|---|
| Publisher | Academic Press |
| Number in series | Report IW 12/73 |
| Volume | 11 |
| Issue | 3 |
| Pages | 323--357 |
Identifiers
| DOI | 10.1016/s0022-0000(75)80056-0 |
|---|
Abstract
Manna's theorem on (partial) correctness of programs essentially states that in the statement of the Floyd inductive assertion method, "A flow diagram is correct with respect to given initial and final assertions if suitable intermediate assertions can be found," we may replace "if" by "if and only if." In other words, the method is complete. A precise formulation and proof for the flow chart case is given. The theorem is then extended to programs with (parameterless) recursion; for this the structure of the intermediate assertions has to be refined considerably. The result is used to provide a characterization of recursion which is an alternative to the minimal fixed point characterization, and to clarify the relationship between partial and total correctness. Important tools are the relational representation of programs, and Scott's induction.
A copy is held
pdf, 1.6 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-09-04 18:18 UTC |
Filed under
Cite it as
@article{bakker1975completeness,
title = {On the completeness of the inductive assertion method},
author = {Jacobus W. de Bakker and Lambert G. L. T. Meertens},
year = {1975},
note = {first published 1973},
journal = {Journal of Computer and System Sciences},
publisher = {Academic Press},
volume = {11},
number = {3},
pages = {323--357},
doi = {10.1016/s0022-0000(75)80056-0},
}
This record lives at https://refs.drheap.org/bakker1975completeness/ and will keep doing so.