Personal tools
You are here: Home

ConGu

The ConGu project aims at developing a framework to create property-driven  algebraic speciļ¬cations and to test Java implementations against these speciļ¬cations. It includes the development of a methodology that integrates design, specification, testing and verification of object-oriented systems, based on the concept of contracts.

Motivation

The idea of the Contract Guided System Development project emerged 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, established in the academic year of 1999/2000, encompasses three semesters, where students learn object-oriented programming supported by the methodology of design by contract. Although the DBC methodology has become very popular, we experienced the frustration of not being able to guide students in writing contracts, both that fully specify all the relevant properties, and are monitorable. In the end, students were left with very poor specifications that discourage the further application of DBC.

Objective

Support the checking of Java classes against property-driven algebraic specifications. Checking classes consists in determining, at run-time, whether the classes that are subject to analysis behave as required by the specification. The key idea of ConGu is to reduce the problem to the run-time monitoring of contract annotated classes, which is supported today by several runtime assertion-checking tools.

Overview

The ConGu approach comprises:

  • A specification language.
  • A language for defining refinement mappings between specifications and classes.
  • A mechanized method for replacing classes under test by automatically generated wrapper classes, clients to other automatically generated classes. Some of these are annotated with contracts, automatically generated from the specifications against which the classes are tested. During the execution of a system involving the classes under test, objects are checked against specification (and the violations are reported) and the correctness of clients' behaviour is monitored whenever they use operations of the classes under test. 

 

Overview of the tool

 

  • The approach is currently tailored to Java and JML, but it could be defined towards other OO programming and assertion languages.

Key Characteristics

  • Property-driven specification language - its simplicity (in contrast with model-driven approaches) encourages more software developers to use formal specifications.
  • Automatic generation of fully monitorable contracts covering all specified properties - no frame conditions assumption; monitorization of properties involving methods with side-effects.
  • Not client invasive - user's classes remained unchanged; source code not required.
  • Late binding of Java classes against specifications - promotes checking the same class against different specifications.
  • Mechanisms for composition of specifications in modules - promotes specification reuse.
Document Actions
« December 2017 »
December
MoTuWeThFrSaSu
123
45678910
11121314151617
18192021222324
25262728293031
Log in


Forgot your password?