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

TL;DR

This paper presents a method to convert proof tableaux of Hoare logic into inference sequences of rewriting induction, enabling the use of termination techniques to prove total correctness of programs.

Contribution

It introduces a transformation from Hoare logic proof tableaux to rewriting induction sequences, linking partial and total correctness proofs.

Findings

Transformation is valid for partial correctness proofs.

Termination of the rewriting system implies total correctness.

Enables applying rewriting termination techniques to program correctness.

Abstract

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.