E-SPARK: Automated Generation of Provably Correct Code from Formally Verified Designs

An approach to generating provably correct sequential code from formallydeveloped algorithmic designs is presented. Given an algorithm modelledin the Event-B formalism, we automatically translate the design into the SPARKprogramming language. Our translation builds upon Abrial’s approach to the developmentof sequential programs from Event-B models. However, as well as generatingcode, our approach also automatically generates code level specifications, i.e.SPARK pre- and post-conditions, along with loop invariants. In terms of the SPARKproof tools, having the loop invariants increases verification automation. A prototype,known as E-SPARK, has been implemented as a plugin for the Rodin Platform(Event-B toolkit), and tested on a range of examples, i.e. searching, sorting andnumeric calculations