Developing a new language to construct algebraic hierarchies for Event-B

This paper proposes a new extension to the Event-B modelling method to facilitate the building of hierarchical mathematical libraries to ease the formal modelling of many systems. The challenges are to facilitate building mathematical theories, be compatible with the current method and tools, and to be extensible by users within the Rodin Platform supporting Event-B.Our contribution is a new language, called B#, which includes the additional features of type classes and sub-typing. The B# language compiles to the current language used by the Rodin's Theory Plug-in, which ensures consistency, and also gives compatibility with the current Rodin tools. We demonstrate the advantages of the new language by comparative examples with the existing Theory Plug-in language.