Master thesis

Type of project:
Master thesis WS 2003/2004-SS 2004, 12 January - 09 July 2004

Tobias Widmer

Reusable Mathematical Models


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 specification-related 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 high-level 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)