Publication

Hoare Logic for Mutual Recursion and Local Variables

Proceedings of FST&TCS'99

Author(s): David von Oheimb
Year: 1999
Publisher: Springer LNCS 1738
Editor: C. Pandu Rangan, Venkatesh Raman and R. Ramanujam
CR Classification: D.2.4, D.3.1, F.3.1
CR General Terms: Languages, Verification, Theory
Keywords: axiomatic semantics, Hoare logic, mutual recursion, soundness, relative completeness, local variables, call-by-value parameters, Isabelle/HOL
Abstract: 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) 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 flexible Call rule.

Copyright © 1999 Springer-Verlag.
This paper has been published by Springer LNCS.
Preprint version available as gzipped PS file and PDF file.
Slides as gzipped PS file.
Isabelle sources

BibTeX entry:

@inproceedings{DvO99, author = {David von Oheimb}, title = {Hoare Logic for Mutual Recursion and Local Variables}, booktitle = {Foundations of Software Technology and Theoretical Computer Science}, year = {1999}, publisher = {Springer}, series = {LNCS}, volume = {1738}, pages = {168--180}, editor = {C. Pandu Rangan, V. Raman and R. Ramanujam}, note = {\url{http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html}}, abstract = { 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) 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 flexible Call rule. }, CRClassification = {D.2.4, D.3.1, F.3.1}, CRGenTerms = {Languages, Verification, Theory} }