What good are strong specifications?

Nadia Polikarpova, Carlo A. Furia, Yu Pei, Yi Wei, Bertrand Meyer

Research output: Chapter in book / Conference proceedingConference article published in proceeding or bookAcademic researchpeer-review

22 Citations (Scopus)

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.
Original languageEnglish
Title of host publication2013 35th International Conference on Software Engineering, ICSE 2013 - Proceedings
Pages262-271
Number of pages10
DOIs
Publication statusPublished - 30 Oct 2013
Externally publishedYes
Event2013 35th International Conference on Software Engineering, ICSE 2013 - San Francisco, CA, United States
Duration: 18 May 201326 May 2013

Conference

Conference2013 35th International Conference on Software Engineering, ICSE 2013
CountryUnited States
CitySan Francisco, CA
Period18/05/1326/05/13

ASJC Scopus subject areas

  • Software

Cite this