Hoare Logic for Mutual Recursion and Local Variables
Hoare Logic for Mutual Recursion and Local Variables
复制标题
用于互递归和局部变量的霍尔逻辑
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
David von Oheimb
中科院分区：
文献类型：
--
作者：
David von Oheimb
我们为一种简单的命令式编程语言提供了一个（第一个？）健全且相对完整的Hoare逻辑，包括具有按值调用参数以及全局和局部变量的相互递归过程。对于这种语言，我们形式化了部分正确性的操作语义和公理语义，并证明了它们的等价性。全局变量和局部变量（包括参数）以一种相当直接的方式处理，允许动态和简单的静态作用域。对于完备性证明，我们采用了强大的MGF （Most General Formula）方法，引入并比较了三种变体来处理相互递归引起的复杂性。
We present a (the first?) sound and relatively complete Hoare logic for a simple imperative programming language including mutually recursive procedures with call-by-value parameters as well as global and local variables. For such a language we formalize an operational and an axiomatic semantics of partial correctness and prove their equivalence. Global and local variables, including parameters, are handled in a rather straightforward way allowing for both dynamic and simple static scoping. For the completeness proof we employ the powerful MGF (Most General Formula)a pproach, introducing and comparing three variants for dealing with complications arising from mutual recursion.
All this work is done using the theorem prover Isabelle/HOL, which ensures a rigorous treatment of the subject and thus reliable results. The paper gives some new insights in the nature of Hoare logic, in particular motivates a stronger rule of consequence and a new flexible Call rule.