Program Logics

An Axiomatic Basis for Computer Programming

C.A.R. Hoare

Defines program correctness using pre- and post-conditions joined by inference rules, giving imperative programs the kind of proof mathematics already had.

Assumes first-order logic and the idea of a proof rule; the programs themselves are tiny

The Existence of Refinement Mappings

Martín Abadi & Leslie Lamport

Gives conditions under which a lower-level specification correctly implements a higher-level one, formalising 'refinement' as a mapping between the two systems' state spaces that a verifier can check mechanically.