Code contracts in DotNet 4.0

Microsoft research has come out with some new additions in the .Net 4.0 release, and one feature that caught my eye was code contracts. An earlier Microsoft research project dealt with a language called spec#, which is an extension of C# but with some added enhancements (, code contracts being one of them. Now that code contracts are a feature of .Net 4.0, the .Net family of languages can benefit much in terms of secure and verifiable code (an article that explains how you can use this feature in code can be found here. The code contract constructs are found in the System.Diagnostics.Contracts namespace).

But my train of thought was not in the inclusion of code contracts in the latest release of the .Net framework, but on the origins of code contracts and contractual programming. Code contracts are derived from the concept of design by contract, a term invented by Bertrand Meyer and now a trademark of Eiffel software. Meyer created the programming language Eiffel to demonstrate design by contract and other concepts that helped create more secure software (secure as in stability and the ability to handle erroneous conditions effectively). The design by concept principle reflects the real world scenario of a publishing entity and a subscribing entity (or a ‘client’ and ‘supplier’ as described in Eiffel texts), where the subscriber receives from the publisher, and the publisher offers to the subscriber. The publisher has to make sure that the subscriber has fulfilled his or her part in the bargain in order to supply or sell. The subscriber has the benefit of receiving from the publisher, as long as his end of the bargain is kept. Both entities have to follow a common contractual set of rules in their transactions. This concept applied to programming is an overview of what design by contract is all about. Methods and classes need to provide preconditions, postconditions and invariants which stand as contractual bindings that have to be followed in the message passing scenario of the object oriented world. The Eiffel language enables design by contract design, and has more advanced extensions where contracts are inherited by sub-members of abstract types (more information can be found at

The Eiffel language appeared commercially by the end of 1986. Design by contract is an old concept, but one that is showing positive signs of adoption from the day of inception. The .Net 4.0 feature of code contracts is one such sign, and hopefully the .Net community will utilize and benefit from this feature in writing secure code, taking the opportunity to practice a time tested principle in the complex world of software development today.


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s