ETH Logo

AutoInfer: Automated Contract Inference

Overview

Contracts are essential for automated program verification, testing and fixing. In languages supporting Design by Contract, programmers usually write simple contracts for their classes. But those contracts are far from complete. In this project, we explore ways to infer better and sometimes complete contracts for those classes.

Basic concepts

Dynamic contract inference
Dynamic contract inference techniques try to infer specifications by generalizing information collected through actual program execution. For example, by analyzing the execution of extend (v) from class LINKED_LIST, one can notice that the number of elements in the list, represented by count, is always increased by 1. This observation can be generalized into a postcondition stating count = old count + 1.

Automated contract inference
The prerequisite of applying dynamic contract inference is to have a set of configurations under which the program under analysis can be executed. Normally, a user provided test suite serves this purpose. To automate the whole process, we can apply automated test case generation to the program first, collect all passing test cases, and use those test cases as input to contract inference.

Implementation

We developed a tool called AutoInfer, which leverages the existing contracts in program, and infers more expressive contracts for command (methods that do not return any value) postconditions. Compare to other dynamic inference techniques, AutoInfer focuses in two forms of contracts:
Both kinds of assertions are difficult to handle with existing approaches. Applying AutoInfer to basic Eiffel data structure classes such as array, list, queue, stack, set and hash table shows that 75% of the complete postconditions of commands can be inferred fully automatically.

Download

AutoInfer is part of the Eiffel Verification Environment repository (EVE), and the source code is available at here.

Project members

Publications

2011