Wiki Agenda Contact English version

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)


Auteurs: Martin Clochard

Catégories: Semantics of languages

Outils: Why3

see also the index (by topic, by tool, by reference, by year)


This example is split into several files.

download ZIP archive