Contractor.NET: Inferring Typestate Properties to Enrich Code Contracts

EDGARDO ZOPPI; VICTOR A. BRABERMAN; GUIDO DE CASO; DIEGO GARBERVESTKY; SEBASTIÁN UCHITEL

Honolulu

Workshop; TOPI 2011: 1st Workshop on Developing Tools as Plug-ins - ICSE 2011; 2011

ACM

In this work we present Contractor.NET, a Visual Studio extension that supports the construction of contract specifications with typestate information which can be used for verification of client code. Contractor.NET uses and extends Code Contracts to provide stronger contract specifications. It features a two step process. First, a class source code is analyzed to extract a finite state behavior model (in the form of a typestate) that is amenable to human-in-theloop validation and refinement. The second step is to augment the original contract specification for the input class with the inferred typestate information, therefore enabling the verification of client code. The inferred typestates are: a level of abstraction that has been successfully used to validate software artifacts, assisting in the detection of a number of concerns in various case studies including specifications of Microsoft Server protocols.