Wiki Agenda Contact Version française

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.

download ZIP archive