Udooz!

Design by contract is a popular approach to designing software. This approach prescribes the software designers should define formal verifications, specification of every components in an application. These verifications and specifications should answer the following questions:

1. What does it expect?
2. What does it guarantee?
3. What does it maintain?

These can be achieved by contracts or assertion which can consumed at method level. These contracts normally contains:

• Acceptable inputs for an operation (method/procedure)
• Pre and Post-conditions
  
• Return value
  
• Exceptions
• Side effects
• Invariants (for sub-classes may strengthen)

To use this approach in .NET, Microsoft Research Lab released "Code Contracts" for .NET.

There are three components available in this release. These are:

• Contract Framework APIs
• Binary Rewriter
• Static Checker

The first two are for runtime checking.

Contract Framework APIs
Contract.Requires() - Pre condition
Contract.Ensures() - Post condition (additional helper methods: Contract.OldValue(), Contract.Result())
Contract.Invariant() - Invariants
ContractInvariantMethodAttribute - Method level attribute, so that we can put all invariant objects into a method.

Binary Rewriter
Normal IL code for the above mentioned APIs cannot be executed at runtime. To provide runtime checking for contracts, you have to use binary rewriter which takes the IL and transforms the contracts so that contracts are executed at the exact programming points.

Get a copy of CodeContract here and user manual here.