Master thesis

In this thesis we develop a framework of reusable mathematical models intended to be used in Eiffel contracts. As first steps towards this goal we identify the necessary mathematical concepts and compare already existing approaches to formal software development to the current specificationrelated facilities provided by the Eiffel language. Equipped with this theoretical background, we derive a new contract language named Intermediate Functional Language (IFL), which is specifically designed to support highlevel mathematical constructs from set theory and relation algebra. To give the proof of concept, we extend some existing classes of the EiffelBase library with mathematical model contracts. The principal contribution of this thesis consists of a set of library classes bundled in the Mathematical Model Library (MML), providing the necessary support to write powerful and expressive model contracts in IFL. A language processing tool is presented that helps in automating the process of extracting the model contracts of an IFL annotated class and generating the associated proof obligations. 
Project plan (PDF) Final Report (PDF) 