CW 398

Nele Smeets, Eric Steegmans
Beyond design by contract: formal specification of composed behaviour

Abstract

The basic building blocks of Design by Contract are Boolean assertions, which are used to express preconditions, postconditions and invariants. For composed commands, i.e. for commands whose effect is realized using other commands, the expressiveness of such contracts appears to be insufficient. In this paper, we propose an extension of the Design by Contract methodology that enables us to express the specification of a composed method in terms of the specification of the composing methods. Among the main advantages of this approach, we distinguish increased expressiveness of contracts, better consistency and trivial code generation.

report.pdf (247K) / mailto: N. Smeets