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.

Software

• ConGu, CONtract GUided System Development.

• Antónia Lopes
• Isabel Nunes
• José-Luiz Fiadeiro
• Vasco T. Vasconcelos
• João Abreu
• Luís Reis

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.

• Develop a means to prove the correctness of a class with respect to its specification, written in an assertion language that is in turn expressive and easy to master;
• Build a formal specification of abstract data types that is effective in driving the identification of the contracts that must be verified by implementing classes;
• Define the methodology of contract identification.

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.

Methodology

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.

Languages

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.

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.

LOOP

Aims to specify and verify properties of classes in object-oriented languages, using proof tools like PVS and Isabelle.

Daikon

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.