A Floating-Point Numbers Theory for Event-B

Static type checking helps catch errors in manipulating variables values early on, and most specification languages, like Event-B, are strongly typed. However, the type system of Event-B language is relatively simple and provides only a way to specify discrete behaviour using Integer type. There is no possibility to model continuous behaviour, which would have helped analyse hybrid systems. More precisely, the Event-B language doesn’t consider in its type-checking system the possibility of defining such behaviours and checking the correctness of the values of the continuous variables within the Event-B models. In this article, we propose to extend the type-checking system of Event-B to include Float variables by specifying a floating point numbers theory using the theory plugin.