Design by Contract

Design by Contract: A discipline of software analysis, design, implementation, testing and documentation. It also goes by the name Code Contracts, primarily because the name Design by Contract is trademarked.

The concept of Design by Contract (DbC) was first formalized by a French academic named Bertrand Meyer, creator of the Eiffel programming language (which inspired Java and C#), which is also the only language that was built with DbC in mind. Microsoft research lab had a language called Spec# which also had built-in support for DbC. Spec# was an extension of C# with DbC concepts. Code Contracts is the successor of that project. The .Net framework’s Base Class Library (BCL) has been using Code Contracts extensively since v4.0. Code Contracts used to be available only for Premium and Ultimate customers of VS, but they recently made it open source. It comes with a static checker and a runtime rewriter. Check the user manual for details. 

The static analysis engine uses abstract interpretation (the automatic, compile-time determination of run-time properties of programs), not software verification (conformance to a specification).

Code Contracts vs Traditional if-then-throw block and debug asserts:

Design by Contract is a programming paradigm, it’s not a tool, a library or an extension to a language. It’s an abstract philosophy of how to design robust applications with the help of specifications known as contracts.

We already use some form of contracts in our everyday Object-Oriented Programming, such as Interfaces that serve as contracts for classes, delegates that serve as contracts for methods, and so on. We also write contracts in various forms for our software, such as in comments, as test suites, as documentation, as Debug.Asserts, and so on. The idea of DbC is to formalize a systematic approach so that every phase of the software life-cycle can benefit from a uniform specification. It’s a guide throughout the entire software development process.

The concepts of preconditions, post-conditions and invariants exist at all levels: requirements, design, implementation, testing, documentation. 

Software Analysis: Contracts can be used during the analysis of software components to specify requirements. (https://archive.eiffel.com/doc/manuals/technology/contract/) 

Software Implementation: Contracts define precisely how to implement the components based on preconditions, post-conditions, invariants and exceptions. 

Inheritance: Contracts are inherited and enforce the Liskov Substitution Principle for inheritance, which helps to build robust software components. 

Exception handling: Contracts provide clear exception handling mechanisms. 

Documentation: Contracts provide documentation for each component, documentation that never goes out of sync with the code-base because they are embedded in the code. 

Testing/Debugging: Contracts provide a platform for tools and testing frameworks to auto-generate tests (see Microsoft Pex). It also makes implementation of test cases very easy. 

Some snapshots of what you can do with Code Contracts:

Here's a checklist of some of the advantages and disadvantages of Code Contracts vs Defensive Programming:

Following is a list of discoveries from the investigation of Code Contracts while implementing it in one of my projects.

• If you are trying to apply Code Contracts to an existing code base it is best to disable it at the assembly level and then to incrementally open it up per method, then per class and so on. Otherwise you will be bombarded with hundreds of warnings and squiggly lines everywhere. You can enable/disable them with the following attributes: [assembly: ContractVerification (false )], [ContractVerification (true)] 
• Add a SQL server name in the Code Contracts project properties for caching, I usually use (localdb)\V11.0. 
• Refactor long functions into smaller private methods. Makes it easy to add Contracts. 
• Think about using the baseline option if you want to track warnings only from a certain baseline code (as in keep track of warnings after a certain point, to avoid getting overwhelmed by warnings). 
• If your project contains contracts and is referenced by other projects, it is recommend that you select Build under the contract reference assembly section in the properties tab for CodeContracts. The contract reference assembly for an assembly named A will be called A.Contracts.dll and appears in the project output directory. 
• Invariants are checked on every public method/property call. They are not checked on private method/property calls. 
• All methods called within a contract must be pure. Methods marked with [Pure] attribute. 
• The static checker recognizes a new contract helper AssumeInvariant that allows you to assume the invariant of an object at arbitrary points in your program. It is a work-around for some static checker limitations. 
• If there is one warning in a method, subsequent warnings may be suppressed. So, fix or comment out the other warnings first. Not sure if it’s a limitation or a feature. 
• Most of the LINQ methods are not annotated with the Contracts API (except for All, Any, Sum, etc). Check the source code or tooltip in VS to find out which ones have contracts. 
• The user-supplied string in Requires, Ensures, etc will be displayed whenever the contract is violated at runtime. Currently, it must be a compile-time constant. 
• Multiple invariant conditions in the same expression seem to throw “condition unproven” warnings sometimes. Breaking them up into separate invariant cases works. 
• The static contract checker has limited supported for ForAll and Exists quantifiers, provided the quantified expression is simple like x => x != null. I wasn’t able to make them work statically at all. 
• Static checking does not work for closures. (Need to verify with latest version) 
• No contracts allowed on delegates. (Need to verify with latest version) 
• When writing iterators using yield, the static contract checker will not be able to prove post-conditions. (Need to verify with latest version) 
• Post-conditions (Ensures) of async methods are not checked by the static checker. 
• Any method whose fully qualified name begins with "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path", or "System.Type" are considered Pure, so you can use them in your contracts. 
• In a Pure method either enable the "Infer ensures" in properties or add Ensures (post-condition) in the method. 
• Enable "Infer invariants for readonly" in properties to make readonly properties invariants. 
• Preconditions are checked before running the constructor initializer. 
• Object invariants on interface properties are not supported. 
• You cannot add a Requires contract in an overridden method (because it violates LSP). 
• External input (database, file system, user input, etc) should be handled in Data Access Layer or UI layer, and all validated data should flow into Business Logic Layer as contracts.

Some guidelines to start using Code Contracts:

When adding code contracts to an existing code base it may seem overwhelming to receive hundreds of warnings for only a few contract cases. So, the suggestion is to disable code contract in all relevant assemblies and to enable it per method one at a time, and fixing the contracts of that method. In order to fix them you may need to add some Contract.Assume or null checks and empty string checks in the calling methods. Anyway, this is how to start the process... 

Project configurations:

1. Download and install Code Contract static checker and binary rewriter in your Visual Studio: https://visualstudiogallery.msdn.microsoft.com/1ec7db13-3363-46c9-851f-1ce455f66970 
2. You may install the Code Contracts Editor Extensions to see contracts in tooltip and intellisense, but I have been getting reproducible VS crashes on some tooltips. You may want to skip it for now. 
3. In Project Properties -> Code Contracts, enable Perform Static Contract Checking. 
4. In Project Properties -> Code Contracts, make sure Check in background and Show squigglies are also enabled. 
5. In Project Properties -> Code Contracts, add an SQL server for caching: for eg, (localdb)\V11.0 
6. In Project Properties -> Code Contracts, slide the warning level to "hi".

Adding contracts in your code:

1. Disable contracts in all relevant assemblies using the following attribute in the AssemblyInfo.cs file: [assembly: ContractVerification (false )] 
2. Start with a class that has little or no dependencies on other classes. 
3. Enable contract on one method in the class chosen in Step 2 using the following attribute: [ContractVerification (true)] 
4. Add contracts such as Contract.Requires and Contract.Ensures in the target method (chosen in Step 3). I suggest starting with simple null checks and empty string checks. 
5. In your calling methods you may have to add some if-else null checks, array bound checks, empty string checks, or whatever else is needed to satisfy the contracts of the target method (the callee). 
6. If at any point inside a target method a contract cannot be verified statically, use Contract.Assume. (for eg. library calls that don't support contracts) 
7. Add contracts to the other methods/properties in the selected class. (Remember to enable ContractVerification for the method) 
8. Repeat the above steps for other classes.

Design by Contract in other languages:

There are many 3rd party libraries that provide support for Design by Contract in languages such as C++, Java, JavaScript and others. Most of these libraries provide runtime contract validation. Static validation in popular languages/frameworks is rare. The .Net framework happens to be the first popular framework that has built-in support for DbC. In the Wikipedia page for Design by Contact you will find a list of 3rd party libraries for other languages: https://en.wikipedia.org/wiki/Design_by_contract.

There has also been talks about incorporating Contracts in the next version of C++ (2017). Here's an interview with Bjarne Stroustrup where he would like to see Contracts in C++17: https://isocpp.org/files/papers/D4492.pdf 

User Manual: http://research.microsoft.com/en-us/projects/contracts/userdoc.pdf 
How the static checker works: http://research.microsoft.com/en-US/projects/contracts/cccheck.pdf