
VOLUME 11, ISSUE 1, PAPER 1
A Hoare logic for the coinductive tracebased bigstep semantics of While

©Keiko Nakata, Institute of Cybernetics ©Tarmo Uustalu, Institute of Cybernetics 
Abstract
In search for a foundational framework for reasoning about observable
behavior of programs that may not terminate, we have previously devised a
tracebased bigstep 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 statebased semantics. Here we present a Hoare logic
counterpart of our coinductive tracebased semantics and prove it sound and
complete. Our logic subsumes the standard partialcorrectness statebased Hoare
logic as well as the totalcorrectness variation: they are embeddable. In the
converse direction, projections can be constructed: a derivation of a Hoare
triple in our tracebased logic can be translated into a derivation in the
statebased 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 metatheory is entirely
constructive as well, and we have formalized it in Coq.

Publication date: February 12, 2015
Full Text: PDF  PostScript DOI: 10.2168/LMCS11(1:1)2015
Hit Counts: 5566 
Creative Commons  