English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

A proof tableau of Hoare logic is an annotated program with pre- andpost-conditions, which corresponds to an inference tree of Hoare logic. In thispaper, we show that a proof tableau for partial correctness can be transformedinto an inference sequence of rewriting induction for constrained rewriting. Wealso show that the resulting sequence is a valid proof for an inductive theoremcorresponding to the Hoare triple if the constrained rewriting system obtainedfrom the program is terminating. Such a valid proof with termination of theconstrained rewriting system implies total correctness of the program w.r.t.the Hoare triple. The transformation enables us to apply techniques for provingtermination of constrained rewriting to proving total correctness of programstogether with proof tableaux for partial correctness.

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