Contract Guided System Development

Funded by Fundação para a Ciência e Tecnologia, Ministério da Ciência e do Ensino Superior, POSI/CHS/48015/2002, from June 2004 to May 2006. Funding: Euro 42.000.

Research Position Grant - Deadline January 30th, 2006.

Research Position Grant - Deadline September 15th, 2005.

Research Position Grant - Deadline September 15th, 2004.




The project centers on Contract Guided System Development, a software methodology that aims at producing provably correct pieces applications. The methodology integrates specification, design, and verification, based on the concept of contracts.

Although design by contract has been promoted for several years now, there are many open problems that must be addressed in order for he methodology to be effectively used. These include semantic issues, in particular conflicts that arise from the use of contracts for different purposes, namely a) declarative vs operational, i.e. for establishing correct usage of a class by its clients vs for monitoring that same usage, and b) horizontal vs vertical, i.e. for making public what services are provided vs for establishing what properties need to be ensured by implementations. More generally, the relationship between contracts and Hoare's original assertion calculus needs more careful investigation, namely in relationship to the use of data refinement techniques and its associated invariants as a means of supporting correct development of code.

We tackle these issues within an integrated effort of bringing ADT-based development into OO programming. The project contributes to the area of object-oriented system development by means of systematising and automating the task of creating classes as implementations of ADTs. Moreover it will contribute to the implementation of systems of classes that are correct with respect to their specification. This is achieved by following three complementary directions.

The idea of the project emerges from a pioneering programme at the Department of Informatics, Faculty of Sciences, University of Lisbon, to provide undergraduate students with a method to develop reliable, quality software. Such a programme was established in the academic year of 1999/2000, and encompasses three one-semester courses that students must take in turn. Students learn (object- oriented) programming supported by the methodology of design by contract.


The project aims at the development of a methodology that integrates design, specification, and verification of object-oriented system, based on the concept of contracts.

Includes: a) attacking the problem: start from an abstract data type (ADT), subclass a given class, write the class from scratch; b) classifying the different kinds of routines needed (queries, modifiers, constructors); c) commiting to an implementation, choosing the attributes; d) selecting the routines that constitute the building blocks of the contract, writing contracts for the remaining routines, and for the class; e) identifying the constraints: visibility of pre-conditions, implicit assertions, meta-assertions; f) inheriting contracts, g) contract writing for correctness proof versus contract writing for runtime monitoring.
A language of assertions, a superset of the Java boolean expressions, used to write contracts for classes. A language of abstract data types effective in driving the (semi-) automatic specification of classes.
Translation system
Translating abstract data types into Java interfaces with contracts, that preserves the semantics of the ADT.
Case studies


Contract Guided System Development
Expected results: A methodology of object-oriented contract guided system development for the Java programming language.
Description: Takes the whole duration of the project, and constitutes the main task where all other tasks meet. It is responsible for choosing the assertion language, the guidelines for contract guided system development, and the methodology in general as mentioned in the objectives.
A proof system for asserting class correctness
Expected results: A proof system and proof techniques
Description: Investigates the relation between Hoare triples and contract-driven correctness formulae, in particular the ability to talk about the state at the beginning execution (common in contracts, absent in Hoare's methodology).
From Abstract Data Types to Contract-Annotated Interfaces
Expected results: A language of ADTs, a translation of ADTs into contract-annotated Java interfaces, and a proof of its correctness.
A system to generate contract-annotated Java interfaces from ADT specifications
Expected results: A prototype tool.

Related Projects

Java Modeling Language (JML)
A behavioral interface specification language that can be used to specify the behavior of Java modules.
Extended Static Checking
A programming tool for finding errors in Java programs.
Aims to specify and verify properties of classes in object-oriented languages, using proof tools like PVS and Isabelle.
A dynamic invariant detector.
Mikado and Agile
Two EC-funded projects under the Information Society Technologies Programme, initiative FET-Global Computing, which the team is involved, may use the methodology here developed in their prototype implementations.