Contractor.NET is 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-the-loop 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 enabledness preserving: 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.
Contractor.NET is based on Contractor, a previous work by the same authors.
This project was selected as one of the recipients of the Software Engineering Innovation Foundation Awards.
News
- June 22th, 2011. Version 1.3 of the plug-in is released. Contract instrumentation was extended to support non-deterministic abstractions.
- April 19th, 2011. Version 1.2 of the plug-in is released. Fixed a CCI bug in the instrumentation that prevented some contracts to be included in the final assembly.
- April 7th, 2011. Version 1.1 of the plug-in is released. Changes include a configuration pane in VS, as well as integration with the newest Code Contracts release.
- March 3rd, 2011. Our paper was accepted to be presented at the TOPI 2011 workshop!
- January 20th, 2011. We submitted a paper to the TOPI 2011 workshop.
Screenshots
