Complete contracts through specification drivers
This solves the issue of contract incompleteness for software developers, offering a novel approach to enhance software reliability.
The paper addresses the problem of incomplete contracts in Design by Contract, which can lead to malicious implementations, by introducing a technique that enables derivation, checking, and improvement of complete contracts without additional syntax.
Existing techniques of Design by Contract do not allow software developers to specify complete contracts in many cases. Incomplete contracts leave room for malicious implementations. This article complements Design by Contract with a simple yet powerful technique that removes the problem without adding syntactical mechanisms. The proposed technique makes it possible not only to derive complete contracts, but also to rigorously check and improve completeness of existing contracts without instrumenting them.