The EventB2Dafny Tool. EventB2Dafny is implemented as a plug-in of Rodin. It takes an EventB machine proof-obligation and generates an equivalent Dafny program. You can then use Dafny proof environment to discharge the proof-obligation. You can check on the syntax of Dafny programs here
Keywords for this software
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.
- Dalvandi, Mohammadsadegh; Butler, Michael; Rezazadeh, Abdolbaghi: From Event-B models to Dafny code contracts (2015)