# Translating Event-B machines to Eiffel programs

## TL;DR

This paper introduces a source-to-source translation method from Event-B models to Eiffel programs, allowing correctness proofs via Eiffel's Design-by-Contract while leveraging object-oriented features.

## Contribution

It presents the first systematic mapping from Event-B to Eiffel, integrating formal correctness proofs with object-oriented programming.

## Key findings

- Enables proof of system properties through Eiffel's Design-by-Contract.
- Preserves all features of object-oriented programming in the translation.
- Facilitates formal verification in practical software development.

## Abstract

Formal modelling languages play a key role in the development of software since they enable users to prove correctness of system properties. However, there is still not a clear understanding on how to map a formal model to a specific programming language. In order to propose a solution, this paper presents a source-to-source mapping between Event- B models and Eiffel programs, therefore enabling the proof of correctness of certain system properties via Design-by-Contract (natively supported by Eiffel), while still making use of all features of O-O programming.