Wiki Agenda Contact English version

Double WP

This is a case study formalizing a toy compiler and proving its correctness. There are two versions given below. The first version is presented in the paper Double WP: vers une preuve automatique d'un compilateur and is compatible with Why3 0.88. The second version is adapted to Why3 1.0 and above. This second version makes use of type invariants.


Auteurs: Léon Gondelman / Martin Clochard

Catégories: Semantics of languages / Type invariant

Outils: Why3

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


The version compatible with Why3 0.88 is described there.

download ZIP archive


The version compatible with Why3 1.0 and above is described there.

download ZIP archive