Hoare Logic for Mutual Recursion and Local Variables

12 years 2 months ago
Hoare Logic for Mutual Recursion and Local Variables
We present a (the rst?) 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) approach, 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 exible Call rule.
David von Oheimb
Added 04 Aug 2010
Updated 04 Aug 2010
Type Conference
Year 1999
Authors David von Oheimb
Comments (0)