We propose a simple compositional program logic for an
imperative extension of call-by-value PCF, built on Hoare logic and
our preceding work on program logics for pure higher-order functions.
A systematic use of names and operations on them allows precise and
general description of complex higher-order imperative behaviour. The
proof rules of the logic exactly follow the syntax of the language and
can cleanly embed, justify and extend the standard proof rules for
total correctness of Hoare logic. The logic offers a foundation for
general treatment of aliasing and local state on its basis, with
minimal extensions. After establishing soundness, we prove that valid
assertions for programs completely characterise their behaviour up to
observational congruence, which is proved using a variant of finite
canonical forms. The use of the logic is illustrated through reasoning
examples which are hard to assert and infer using existing program
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.