Computing Publications

Publications Home » An Observationally Complete Progr...

An Observationally Complete Program Logic for Imperative Higher-Order Functions

Kohei Honda, Martin Berger, Nobuko Yoshida

Conference or Workshop Paper
20th IEEE Symposium on Logic in Computer Science, 2005
20th IEEE Symposium on Logic in Computer Science
June, 2005

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


BibTEX file for the publication built & maintained by Ashok Argent-Katwala.