Case studies and tools for contract specifications

Download: PDF, slides (PDF), data and tools.

“Case studies and tools for contract specifications” by Todd W. Schiller, Kellen Donohue, Forrest Coward, and Michael D. Ernst. In ICSE 2014, Proceedings of the 36th International Conference on Software Engineering, (Hyderabad, India), June 2014, pp. 596-607.

Abstract

Contracts are a popular tool for specifying the functional behavior of software. This paper characterizes the contracts that developers write, the contracts that developers could write, and how a developer reacts when shown the difference.

This paper makes three research contributions based on an investigation of open-source projects' use of Code Contracts. First, we characterize Code Contract usage in practice. For example, approximately three-fourths of the Code Contracts are basic checks for the presence of data. We discuss similarities and differences in usage across the projects, and we identify annotation burden, tool support, and training as possible explanations based on developer interviews. Second, based on contracts automatically inferred for four of the projects, we find that developers underutilize contracts for expressing state updates, object state indicators, and conditional properties. Third, we performed user studies to learn how developers decide which contracts to enforce. The developers used contract suggestions to support their existing use cases with more expressive contracts. However, the suggestions did not lead them to experiment with other use cases for which contracts are better-suited.

In support of the research contributions, the paper presents two engineering contributions: (1) Celeriac, a tool for generating traces of .NET programs compatible with the Daikon invariant detection tool, and (2) Contract Inserter, a Visual Studio add-in for discovering and inserting likely invariants as Code Contracts.

Download: PDF, slides (PDF), data and tools.

BibTeX entry:

@inproceedings{SchillerDCE2014,
   author = {Todd W. Schiller and Kellen Donohue and Forrest Coward and
	Michael D. Ernst},
   title = {Case studies and tools for contract specifications},
   booktitle = {ICSE 2014, Proceedings of the 36th International
	Conference on Software Engineering},
   pages = {596--607},
   address = {Hyderabad, India},
   month = jun,
   year = {2014}
}

Back to Publications that describe invariant detection techniques in Daikon.