Program Verification Based on Denotational Semantics

Abstract

A theory of partial correctness proofs is formulated in Scott's logic computable junctions. This theory allows mechanical construction of verification condition solely on the basis of a denotational language definition. Extensionally these conditions, the resulting proofs, and the required program augmentation are similar to those of Hoare style proofs; conventional input, output, and invariant assertions in a first order assertion language are required. The theory applies to almost any sequential language defined by a continuation semantics; for example, there are no restrictions on aliasing or side-effects. Aspects of static semantics,such as type and declaration constraints, which are expressed in the denotational definition are validated as part of the verification condition generation process.