Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While Seminars/Workshops

Abstract

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. It is constructively equivalent to the textbook-style small-step semantics. On terminating runs, it agrees with the standard inductive state-based semantics.

Recently we designed a Hoare logic counterpart of our coinductive trace-based semantics and proved it sound and complete. Our logic subsumes both the partial correctness Hoare logic and the total correctness Hoare logic: they are embeddible. Since we work in a constructive ambient logic, the range of expressible program properties has a rich structure; in particular, we can distinguish between termination and nondivergence, e.g., unbounded total search fails to be terminating but is nonetheless nondivergent.

My talk will start by introducing the coinductive big-step semantics, then present the Hoare-logic. I will explain some interesting design issues on the semantics and the logic and give an example of unbounded total search. All the results have been formalized in Coq constructively.

This is a joint work with Tarmo Uustalu.