Keiko Nakata ; Tarmo Uustalu - A Hoare logic for the coinductive trace-based big-step semantics of While

lmcs:692 - Logical Methods in Computer Science, February 11, 2015, Volume 11, Issue 1 -
A Hoare logic for the coinductive trace-based big-step semantics of WhileArticle

Authors: Keiko Nakata ; Tarmo Uustalu ORCID

    In search for a foundational framework for reasoning about observable behavior of programs that may not terminate, we have previously devised a trace-based big-step semantics for While. In this semantics, both traces and evaluation (relating initial states of program runs to traces they produce) are defined coinductively. On terminating runs, this semantics agrees with the standard inductive state-based semantics. Here we present a Hoare logic counterpart of our coinductive trace-based semantics and prove it sound and complete. Our logic subsumes the standard partial-correctness state-based Hoare logic as well as the total-correctness variation: they are embeddable. In the converse direction, projections can be constructed: a derivation of a Hoare triple in our trace-based logic can be translated into a derivation in the state-based logic of a translated, weaker Hoare triple. Since we work with a constructive underlying logic, the range of program properties we can reason about has a fine structure; in particular, we can distinguish between termination and nondivergence, e.g., unbounded classically total search fails to be terminating, but is nonetheless nondivergent. Our meta-theory is entirely constructive as well, and we have formalized it in Coq.

    Volume: Volume 11, Issue 1
    Published on: February 11, 2015
    Imported on: April 3, 2011
    Keywords: Computer Science - Logic in Computer Science
      Source : OpenAIRE Graph
    • Highly Adaptable and Trustworthy Software using Formal Models; Funder: European Commission; Code: 231620

    8 Documents citing this article

    Consultation statistics

    This page has been seen 1596 times.
    This article's PDF has been downloaded 751 times.