Case Studies and Tools for Contract Specifications

Todd W. Schiller, Kellen Donohue, Forrest Coward, and Michael D. Ernst

Download: PDF


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 (implications). 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 the developers 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.


Open-Source Tools

Subject Programs and Experimental Data

The program trace files include the Celeriac and Daikon configuration options that were used in the studies.

Labs Framework

Mishra Reader

Sando

Quick Graph


Last modified: Wed Mar 12 01:10:40 EDT 2014