Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction

Shinnosuke Mizutani
(Nagoya University)
Naoki Nishida
(Nagoya University)

A proof tableau of Hoare logic is an annotated program with pre- and post-conditions, which corresponds to an inference tree of Hoare logic. In this paper, we show that a proof tableau for partial correctness can be transformed into an inference sequence of rewriting induction for constrained rewriting. We also show that the resulting sequence is a valid proof for an inductive theorem corresponding to the Hoare triple if the constrained rewriting system obtained from the program is terminating. Such a valid proof with termination of the constrained rewriting system implies total correctness of the program w.r.t. the Hoare triple. The transformation enables us to apply techniques for proving termination of constrained rewriting to proving total correctness of programs together with proof tableaux for partial correctness.

In Horatiu Cirstea and David Sabel: Proceedings Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017), Oxford, UK, 8th September 2017, Electronic Proceedings in Theoretical Computer Science 265, pp. 35–51.
Published: 16th February 2018.

ArXived at: http://dx.doi.org/10.4204/EPTCS.265.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org