An observationally complete program logic for imperative higher-order functions

作者：Honda Kohei; Yoshida Nobuko^*; Berger Martin

来源：Theoretical Computer Science, 2014, 517: 75-101.

DOI：10.1016/j.tcs.2013.11.003

• Completeness Characteristic formulae
• Program logic
• Higher-order function
• Imperative programming
• Observational equivalence

We establish a strong completeness property called observational completeness of the program logic for imperative, higher-order functions introduced in [1]. Observational completeness states that valid assertions characterise program behaviour up to observational congruence, giving a precise correspondence between operational and axiomatic semantics. The proof layout for the observational completeness which uses a restricted syntactic structure called finite canonical forms originally introduced in game-based semantics, and characteristic formulae originally introduced in the process calculi, is generally applicable for a precise axiomatic characterisation of more complex program behaviour, such as aliasing and local state.

• 出版日期2014-1-16