In this tutorial I will introduce CodeContracts, the .NET solution for contract specifications.
CodeContracts consist of a language and compiler-agnostic API to express contracts, and of a set of tools to automatically generate the documentation and to perform dynamic and static verification. The CodeContracts API is part of .NET since v4, the tools are available for download on the Visual Studio Gallery. To date, they have been downloaded more than 100,000 times.
In Proceedings of SigADA High Integrity Language Technology (HILT 2013)
Francesco Logozzo and Manuel Fähndrich. Pentagons: A weakly relational domain for the efficient validation of array accesses, Association for Computing Machinery, Inc., March 2008.
Francesco Logozzo, Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Mike Barnett. A Semantic Integrated Development Environment, ACM SIGPLAN, October 2012.
Patrick Cousot, Radhia Cousot, and Francesco Logozzo. A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis, Association for Computing Machinery, Inc., January 2011.
Manuel Fahndrich and Francesco Logozzo. Clousot: Static contract checking with Abstract Interpretation, Springer Verlag, June 2010.
Mehdi Bouaziz, Francesco Logozzo, and Manuel Fahndrich. Inference of Necessary Field Conditions with Abstract Interpretation , Springer, December 2012.
Francesco Logozzo and Tom Ball. Modular and Verified Automatic Program Repair, ACM SIGPLAN, 23 October 2012.
Mike Barnett, Manuel Fahndrich, and Francesco Logozzo. Embedded Contract Languages, Association for Computing Machinery, Inc., March 2010.