Hoare logic for higher order store with simple foundations
Nathaniel Charlton · 2012
We revisit the problem of providing a Hoare logic for a simple language for higher order store programs, considered by Reus and Streicher (ICALP, 2005). In a higher order store program, the procedures/commands of the program are not xed, but can be manipulated at runtime by the program itself; such programs provide a foundation to study language features such as reection, dynamic loading and runtime code generation. We present progress in three areas. Firstly, we present a new semantic model of the programming language, using at states rather than domains. This model is much simpler and leads to a more powerful logic: unintuitive restrictions on proof rules are eliminated, nondeterministic programs are handled, programs which perform syntactic equality tests on commands can be reasoned about, and some convenient new proof rules are validated. Secondly we explain and demonstrate with an example that, contrary to what has been stated in the literature, such a proof system does support proofs which are (in a specic sense) modular. Thirdly we extend the programming language with an operator for runtime specialisation of code, which is a simple form of runtime code generation. We provide new proof rules for reasoning about this operator, including a new recursion rule. We demonstrate these rules with an example.