Brussels / 31 January & 1 February 2015

schedule

Contract-based Programming - A Route to Finding Bugs Earlier


Contract-based programming is a software development technique, which is used to find programming errors earlier in the development process. "Contract" refers to formal declarations of how types and subprograms ("functions and methods" if you aren't an Ada programmer already) behave. In the strictest form, the contracts are checked as a part of the compilation process, and only a program which can be proven to conform with the contracts will compile. In a less strict form, it is more similar to "preventive debugging", where the contracts are inserted as run-time checks, which makes it more likely to identify errors during testing.

Ada provides a quite extensive support for contract-based programming. The checks are specified as a mix of compile-time checks, obligatory run-time checks, and optional run-time checks. In addition to that, SPARK defines a subset of Ada with full compile-time checks.

The presentation will introduce the Ada features related to contract-based programming, and provide suggestions for how to make use of the features in practice. It is organized in three main sections: type/object invariants; pre- and postconditions for operations; making the contracts for entire packages consistent. If there is time, the presentation will close with a live test of the guidelines on an example problem selected by the audience.

The intended audience is anybody with enough programming experience to know concepts like types, encapsulation and packages. Having seen source text in Pascal-like programming languages will be a benefit.

Speakers

Photo of Jacob Sparre Andersen Jacob Sparre Andersen

Links