On the completeness of the inductive assertion method
The work
| Authors | Jacobus W. de Bakker; Lambert G. L. T. Meertens |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1973 |
| Also known as | debakker1973completeness |
| Citekey | bakker1973completeness |
Where it appeared
| Publisher | Mathematisch Centrum, Afdeling Informatica |
|---|---|
| Number in series | IW 12/73 |
| School | Mathematisch Centrum, Afdeling Informatica |
Access
| Landing page | https://ir.cwi.nl/pub/9489 |
|---|
Related
| Superseded by | bakker1975completeness |
|---|
From bibtex.
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.7 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-10-23 01:18 UTC |
| Approved by | a person 2026-10-23 07:46 UTC |
Filed under
Cite it as
@techreport{bakker1973completeness,
title = {On the completeness of the inductive assertion method},
author = {Jacobus W. de Bakker and Lambert G. L. T. Meertens},
year = {1973},
publisher = {Mathematisch Centrum, Afdeling Informatica},
school = {Mathematisch Centrum, Afdeling Informatica},
}
This record lives at https://refs.drheap.org/bakker1973completeness/ and will keep
doing so. It used to be called debakker1973completeness, and those addresses still resolve to this one.