Soundness and completeness of an axiom system for program verification

Authors	Stephen A. Cook
Editors
Type	article
Year	1978
Citekey	`cook1978soundness`

Published in	SIAM Journal on Computing
Volume	7
Issue	1
Pages	70--90

DOI	10.1137/0207005

Distinct from	hostert2026completeness Cook's relative completeness, extended to a logic that breaks his stratification. The paper says so directly: Cook 'examines completeness of the Hoare triple rules under the assumption that one has a complete proof system for the assertion logic, a property that has come to be called relative completeness. In the case of Iris, we effectively do something' similar -- but Iris is higher-order and has no strict separation between assertion logic and specification logic, which is what made the result hard to state at all.

Distinct from

hostert2026completeness Cook's relative completeness, extended to a logic that breaks his stratification. The paper says so directly: Cook 'examines completeness of the Hoare triple rules under the assumption that one has a complete proof system for the assertion logic, a property that has come to be called relative completeness. In the case of Iris, we effectively do something' similar -- but Iris is higher-order and has no strict separation between assertion logic and specification logic, which is what made the result hard to state at all.

A simple ALGOL-like language is defined which includes conditional, while, and procedure call statements as well as blocks. A formal interpretive semantics and a Hoare style axiom system are given for the language. The axiom system is proved to be sound, and in a certain sense complete, relative to the interpretive semantics. The main new results are the completeness theorem, and a careful treatment of the procedure call rules for procedures with global variables in their declarations.

pdf, 2.1 MB. Not published — it may be under copyright. The facts and links here are.

How it got here	agent via bibtex
Added	2026-08-05 00:00 UTC
Approved by	a person 2026-08-12 14:59 UTC

cook relatively-complete

@article{cook1978soundness,
  title        = {Soundness and completeness of an axiom system for program verification},
  author       = {Stephen A. Cook},
  year         = {1978},
  journal      = {SIAM Journal on Computing},
  volume       = {7},
  number       = {1},
  pages        = {70--90},
  doi          = {10.1137/0207005},
}

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

Soundness and completeness of an axiom system for program verification

The work

Where it appeared

Identifiers

Related

Abstract

A copy is held

How it got here

Filed under

Cite it as