Should You Start Using Contracts?

People on various forums have been talking about Code Contracts and whether they should use them? This is an interesting question and the answer to it usually is “it depends”. But I can help you understand on what it should depend.

A Brief History of Contracts

The idea of contract programming appeared in the 80s in Bertrand Meyer’s mind and was based on mathematical analysis calculations of Hoare and other smart people.

The idea was the following: the software itself can not be correct or incorrect; this concept is applicable only to a “software - expected behaviour” pair. And because expected behavior is usually quite an incomprehensible thing, we want to be able to express this very behavior in a brief and implementation-agnostic way.

Assertions are used to express the expected behavior (aka specification); and to understand what exactly is wrong in the program – the caller or the called code, several types of assertions were added:

Pre-conditions, violations of which indicate a bug in the calling code ("the client is wrong").
Post-conditions, violations of which indicate a bug in the called code ("the service is wrong").
Class invariants, violations of which also indicate a bug in the called code. This is an object-oriented specific thing that allows you to clearly say what a valid state of the object is, in order to not multiply pre-conditions and post-conditions. Here we must remember that the invariant is valid from the moment the object was created until its destruction – a call of the destructor/Dispose method, but may not be valid *inside* the method call. Invariant has to be valid in *visible points*.
Assertions about correct implementation, violations of which also indicate a bug in the called code. These are good old asserts placed around in the wilds of implementation, which simplify bug catching.
Loop invariants, an exotic thing that "proves" the convergence of the loop. They exist only in Eiffel and can be ignored.

The fact that a violation of assertions is a bug is very important, as this means that the program should not be able to recover from the consequences of such an event. In other words, Environment.FailFast can be called, or a rather general exception may occur, the processing of which would be impossible (it's a bug, its fix is to correct the code; there is nothing you can do with it in a catch block).

Contracts and Removed Code.jpg

Since the assertions are not new, then what is the difference between the contracts and the good old asserts? And the difference is that contract programming involves "integration" of assertions in the tools, code, and the brain of the programmer.

Any tool that follows the principles of contract programming should provide the following capabilities:

The ability to set the level of assertions: remove all; leave only pre-conditions; leave pre-conditions and post-conditions; leave all assertions.
Ability to generate documentation and a convenient way to "discover" contracts in runtime. This is tooling!
Ability to prove the correctness of the program at the compilation stage (static verifier).

Any full implementation of "contracts" should have all these characteristics, because as the prophet of contracts Meyer says, the union of all of these ideas is power (although there is an opinion that truth is power!)

A long time has passed since the publication of different ABC books on contract programming and the appearance of such tools, but the idea found only partial application. The reason why is below. Now you can count on your fingers the number of programs with "full implementations", most of which are good for nothing. You have Eiffel with full support of contracts, there are languages with pre-conditions/post-conditions but without the ability to set the behavior of violations during execution and without static verification, and there are a number of tools for .NET and Java.

A Brief History of Code Contracts

Since the idea of contract programming sounds sensible, it is not surprising that scholars in large companies have decided to make their own implementation. In Microsoft three guys from their research unit (aka Microsoft Research) were doing this.

By the beginning of their work on the library, the support for contracts has already been provided in Spec# language, which made it clear that the idea works. But the soundness of the idea is not enough to be able to convince Hejlsberg and the company to add contracts in mainstream languages such as C# / VB. What to do then? A conscious decision was made to make contracts language-agnostic - bind them to the platform and make them available for any .NET language platform (well, as we will learn later, it is rather theoretical).

And what does this mean in terms of implementation? This means that "contracts" should work at IL-level: decompile the existing code, find calls of relevant methods (class methods System.Diagnostics.Contracts.Contract) and rewrite them depending on the user settings to classic assertions, exception throw, or just remove these calls. Or find contracts and try to prove that the program is correct or not (static checker).

It sounds simple enough, and the process of reading and rewriting IL was rather easy back in 2003, before the advent of anonymous methods with closures, before the appearance of iterator blocks and async methods. Now imagine that the three researchers are creating a tool for that must last a decade, when the insides of platforms undergo significant changes, new tools for reading IL appear, and the generated IL itself changes periodically with the addition of new features. Then it becomes clear that a method such as MikesArchitecture is quite normal, that formatting is for cowards, and that you will not be able to understand the logic of the rewriter without soft drugs. Not to mention the static analyzer, which can only be understood (and forgiven?) by a PhD under the influence of something strong and toxic.

Adaptation Within Microsoft

If you look at http://referencesource.microsoft.com, you can find about a thousand links to Contract.Requires and a couple of thousand calls of Contract.EndContractBlock inside .NET Framework. They are still very few, since validation of arguments is everything, and contracts are everything to validate arguments.

BCL code shows that the love for contracts comes and goes, but, nevertheless, it never stays for long (yes, in my current team it came and never left, but hatred for contracts also appears consistently).

The culture in Microsoft is such that there is no possibility to impose tools on teams. If a team likes the tool, then they will use it. If not (and this does not contradict some global standards), the tool will not be used.

Unfortunately for contracts, features of implementation and the "research approach" took their toll. Code Contracts even now have mediocre performance, affect run-time behavior of the "rewritten" code, do not have proper tooling, and do not allow the use of a static analyzer on an industrial scale. The idea is wonderful, but the implementation clearly corresponds with the funds invested in it (although I would say that for the instrument created by three people the result exceeds the invested funds!).

And since there was no adaptation by large departments, there were no additional investments, which could allow to polish the tool. This is a chicken and egg problem in its pure form.

In part 2 of the article we will be looking at the features of Code Contracts.

Sergey Teplyakov
Expert in .Net, С++ and Application Architecture