Complete contracts through specification drivers

TL;DR

This paper introduces a technique to achieve complete contracts in software design by complementing Design by Contract, enabling rigorous checking and improvement of contract completeness without new syntax.

Contribution

It presents a simple method to derive and verify complete contracts, addressing limitations of existing Design by Contract techniques.

Findings

Enables derivation of complete contracts from partial ones

Allows rigorous checking of contract completeness

Improves contract quality without additional syntax

Abstract

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.