Tool Support for Design by Contract

Défense de mémoire d'Adrien Houdart

The Skalup development team uses the technique of Design by Con-tract (DbC) for the realisation of its programs. This methodology aims at introducing the concept of contract in computer applications. These contracts consist of preconditions, postconditions and invariants and are represented in the source code in the form of semi-formal specifications on top of methods and classes.

The technique of Design by Contract was born out of researches con-ducted by Bertrand Meyer, in connection with its Ei˙el programming language. Simultaneously, Liskov has also introduced the concepts of pre-conditions, postconditions and invariants in her researches on the princi-ple of substitution. Programming with contracts supposes that software developers define precisely what a function / method does and what are the conditions to use it.

Although the DbC technique significantly reduces the number of bugs within an application, Skalup developers face another problem; ensuring that the specifications correspond to the implementation to which they are linked. Currently this check is done manually and therefore takes a considerable time.

The objective of this master thesis is to analyse what exists in terms of code analysis tools for specifications, suggest improvements, contribute to research on this issue and determine the limits of the verifications that can be performed. The second part of the thesis will focus on the real-ization of a static analysis tool for semi-formal specifications. This tool would aim to inform the developers that an inconsistency between the code and the specification was made in the application.

Keywords: Design by Contract, specifications, precondition, post-conditions, invariant, errors detection, static analysis.

Contact : Isabelle Daelman - 4966 - isabelle.daelman@unamur.be
Télecharger : vCal