Hoare Logic and Games
This development implements in Why3 some notions of games and of transitions systems dedicated to proof of programs. A Hoare-style logic is presented and shown correct with respect to the operational semantics of transition systems and games. Note that to replay the proofs of this development, one needs a development version of Why3, to extract from the current git repository (use commit fd6e788915fe02daa9f)
Authors: Martin Clochard
Topics: Semantics of languages
Tools: Why3
see also the index (by topic, by tool, by reference, by year)
This example is split into several files.