Hoare Logic for Higher Order Store Using Simple Semantics
Hoare Logic for Higher Order Store Using Simple Semantics
复制标题
使用简单语义的高阶存储的霍尔逻辑
DOI：
10.1007/978-3-642-20920-8_10
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Nathaniel Charlton
中科院分区：
文献类型：
--
作者：
Nathaniel Charlton
We revisit the problem of providing a Hoare logic 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 fixed, but can be manipulated at runtime by the program itself; such programs provide a foundation to study language features such as reflection, dynamic loading and runtime code generation. By adapting the semantics of a proof system for a language with conventional (fixed) mutually recursive procedures, studied by von Oheimb (FSTTCS, 1999), we construct the same logic as Reus and Streicher, but using a much simpler model and avoiding unnecessary restrictions on the use of the proof rules. Furthermore our setup handles nondeterministic programs "for free". We also 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 specific sense) modular.
关于运行时代码更新的形式化推理
DOI：
10.1109/icdew.2011.5767624
发表时间：
2011
期刊：
--
影响因子：
--
作者：
Charlton N
通讯作者：
Charlton N
递归世界上的阶跃索引克里普克模型
影响因子：
--
作者：
Birkedal L
通讯作者：
Birkedal L