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.
Authors: Léon Gondelman / Martin Clochard
Topics: Semantics of languages / Type invariant
Tools: Why3
see also the index (by topic, by tool, by reference, by year)
The version compatible with Why3 0.88 is described there.
The version compatible with Why3 1.0 and above is described there.