An Exercise in Invariant-based Programming with Interactive and Automatic Theorem Prover Support

Ralph-Johan Back, Johannes Eriksson

Invariant-Based Programming (IBP) is a diagram-based correct-by-construction programming methodology in which the program is structured around the invariants, which are additionall…