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
pp.270–279
June, 2005
IEEE
Abstract

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

logics.

BibTEX file for the publication
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.