EventB2SQL

EventB2SQL is a Rodin plugin for generating database applications from abstract Event-B models. EventB2SQL generates code for four types of applications:
* Java with MySQL backend (JDBC)
* Java with SQLite backend (JDBC)
* Java for Android with native SQLite backend
* PHP with MySQL backend (PDO)

EventB2SQL can translate abstract Event-B models that use features such as:
* enumerated sets
* variables of set and relation types
* simultaneous assignment
* set comprehensions
* quantified assertions

See the wiki for installation instructions and brief usage examples.