What Good Are Strong Specifications?

TL;DR

This paper explores the use of strong specifications in software development, demonstrating that they can significantly improve bug detection with manageable costs, thus offering a practical enhancement to traditional lightweight formal methods.

Contribution

It introduces a methodology extending Design by Contract for strong specifications and evaluates its effectiveness and cost in real-world testing scenarios.

Findings

Strong specifications detect twice as many bugs as standard contracts.

Testing against strong specifications has reasonable overhead.

Strong specifications offer a favorable benefit-to-effort ratio.

Abstract

Experience with lightweight formal methods suggests that programmers are willing to write specification if it brings tangible benefits to their usual development activities. This paper considers stronger specifications and studies whether they can be deployed as an incremental practice that brings additional benefits without being unacceptably expensive. We introduce a methodology that extends Design by Contract to write strong specifications of functional properties in the form of preconditions, postconditions, and invariants. The methodology aims at being palatable to developers who are not fluent in formal techniques but are comfortable with writing simple specifications. We evaluate the cost and the benefits of using strong specifications by applying the methodology to testing data structure implementations written in Eiffel and C#. In our extensive experiments, testing against strong specifications detects twice as many bugs as standard contracts, with a reasonable overhead in terms of annotation burden and run-time performance while testing. In the wide spectrum of formal techniques for software quality, testing against strong specifications lies in a "sweet spot" with a favorable benefit to effort ratio.