Constructing a new language to facilitate mathematical proofs In the event-B context
James Snook · ePrints Soton (University of Southampton) · 2020
There are many languages used for modelling systems, and verifying the consistency of specifications. Having a valid specification reduces the chances of finding major issues later in the development process. Many of these systems use a set theoretic syntax, which gives a powerful mathematical system for modelling discrete systems. This thesis focuses on the Event-B modelling system, although the results could be applied to other set theoretic modelling systems. The aim of this thesis is to increase the number of mathematical theories available to the Event-B modeller, as this allows allows more accurate models to be created. The approach taken is to facilitate the definition of abstract mathematical types such as Monoids, Groups, and Rings in such a way that they can be built up hierarchically, and concrete mathematical types e.g., the naturals can use the results of the abstract types. This work firstly shows how the current set theoretic language (Event-B) can be used to define abstract mathematical types, and have concrete mathematical types reuse the results of the abstract types. It also demonstrates many difficulties of defining these types using the set theoretic syntax. To resolve these issues a new language, B♯ , is proposed. This language is designed to facilitate the definition of abstract mathematical types, and translate to the current Event-B syntax. The major additions to the new language to allow the definition of mathematical types are type classes and subtypes. At its core the B♯ language is a HOL style language. This work demonstrates how a HOL style language can be translated into a set theoretic style language. This translation is then extended to translate all the features of the B♯ language to the Event-B syntax. This allows theorems defined in the B♯ language to be used by Event-B modellers. A developer environment to define B♯ theorems is built, and the translation from the B♯ syntax to the Event-B syntax is implemented. This is used to define several mathematical types, and demonstrate the practicality of the approach. iv The approach of adding a translation phase from a new syntax was found to be a safe (inconsistencies could not be added to proving mechanisms) and effective way of adding features to the Event-B toolset. Many additional features and improvements are suggested. This approach could be used in a similar manner to other theorem provers use of a meta language (ML) to safely add features without introducing inconsistencies.