Search

Invariant-based programming is a correct-by-construction programming methodology in which programs are expressed as graphs of situations connected by transitions . Such graphs are called invariant diagrams . The situations correspond to the pre- and postconditions and loop invariants of the program, while the transitions correspond to the program statements. The situations are developed before the transitions, and each transition is verified at the time it is added to the diagram. The correctness conditions for the transitions are derived using Hoare-like rules. In this paper, we present an embedding of invariant diagrams in the higher-order logic framework Isabelle/HOL for both proving the verification conditions in the Isabelle proof assistant, as well as generating code that is operationally consistent with the verification semantics by constructing a proof that the generated code is correct with respect to the situations of the invariant diagram. We describe a mechanic translation of the transitions of an invariant diagram into a collection of mutually recursive functions and an associated correctness theorem stating that the value computed by the functions satisfies the final situation. We show that the proofs of the correctness theorem and the well-foundedness of the recursive functions can be built mechanically. The verification conditions are lemmas in the proofs. The collection of recursive functions is a refinement of the original invariant diagram, and is in a form that can be directly converted to executable code by Isabelle. This allows proof-producing compilation of invariant diagrams into any of the languages supported by Isabelle code generator. We illustrate our approach with a case study, and show that full proof automation can be achieved. This work is a step towards verified compilation of invariant diagrams.