Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Embedded Contract Languages

Mike Barnett, Manuel Fahndrich, and Francesco Logozzo


Specifying application interfaces (APIs) with information that goes beyond method argument and return types is a long-standing quest of programming language researchers and practitioners. The number of type system extensions or specification languages is roughly equal to the number of tools that consume them. In other words, every tool comes with its own specification language. In this paper we argue that for modern object-oriented languages, using an embedding of contracts as code is a better approach. We exemplify our embedding of Code Contracts on the Microsoft managed execution platform (.NET) using the C# programming language. The embedding works as well in Visual Basic. We discuss the numerous advantages of our approach and the technical challenges, as well as the status of tools that consume the embedded contracts


Publication typeInproceedings
Published inACM SAC - OOPS
PublisherAssociation for Computing Machinery, Inc.

Newer versions

Patrick Cousot, Radhia Cousot, Francesco Logozzo, and Mike Barnett. An Abstract Interpretation Framework for Refactoring with Application to Extract Methods with Contracts, ACM SIGPLAN, 23 October 2012.

Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Francesco Logozzo. Automatic Inference of Necessary Preconditions, Springer Verlag, January 2013.

Francesco Logozzo. Our Experience with the CodeContracts Static Checker, Springer, January 2012.

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.

Francesco Logozzo. Practical verification for the working programmer with CodeContracts and Abstract Interpretation - Invited Talk, Springer Verlag, January 2011.

Manuel Fahndrich and Francesco Logozzo. Static contract checking with Abstract Interpretation, Springer Verlag, October 2010.

Francesco Logozzo. Practical Specification and Verification with CodeContracts, ACM, November 2013.

> Publications > Embedded Contract Languages