1. 3

Abstract: “An approach to generating provably correct sequential code from for- mally developed algorithmic designs is presented. Given an algorithm modelled in the Event-B formalism, we automatically translate the design into the SPARK programming language. Our translation builds upon Abrial’s approach to the development of sequential programs from Event-B models. However, as well as generating code, our approach also automatically generates code level specifications, i.e. SPARK pre- and post-conditions, along with loop invariants. In terms of the SPARK proof 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 and numeric calculations.”

    1. 2

      Also consider Practical Formal Verification of Domain-Specific Language Applications where IVORY ( a restricted version of the C programming language, embedded in Haskell) and DSL based on UML, were translated in ACL2.

      One concern about this approach is the trustworthiness of the verification condition generator (VCG). There has been some effort to mechanically verifying the VCG. The complexity of any such approach is directly related to the semantics of the two languages under consideration.

      1. 1

        Thanks for this and Layered Concurrent Programs. :)