An observationally complete program logic for imperative higher-order functions
File(s)
Published version
Author(s)
Honda, Kohei
Yoshida, Nobuko
Berger, Martin
Type
Report
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.
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.
Date Issued
2013-01-01
Citation
Departmental Technical Report: 13/2, 2013, pp.1-80
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
80
Journal / Book Title
Departmental Technical Report: 13/2
Copyright Statement
© 2013 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
13/2