.NET 4 Code Contracts

Note My opinion is not based on some kind of “attachment” to Spec#. Everything I know about Spec# and Code Contracts I know from public sources, and myself I have not used either of these technologies.

Nowadays, a lot of time is spent by Microsoft people telling us how cool the new .NET 4 will be (if I would be in bad mood now I would say that they should f$#@ng go and fix .NET 3.5 SP1 as well as billion other broken things they already have before starting to work on “newer and more improved” stuff). Three most prominent features talked about are support for dynamic languages, addition of the dynamic type to C#, and something called Code Contracts. While I do not have anything to say about dynamic languages (as I do not use them, and, to be honest, do not see much value in them, but this is completely irrelevant to this post and in general – I am not interested in flaming here), and about the new dynamic type in C# (which by the way is not bad, but I am a bit afraid of the extent of its potential misuse), I do have an opinion about the Code Contracts.

Microsoft Research has technology called Spec#. It is fairly stable and developed programming system that consists of programming language, its compiler, and static program verifier, and allows design-by-contract approach (I would say much like that of Eiffel, or even more powerful) among other offered features. Spec# team says, “A unique feature of the Spec# programming system is its guarantee of maintaining invariants in object-oriented programs in the presence of callbacks, threads, and inter-object relationships”. Spec# language is similar to C# (well, it is C# with some extensions indeed, and there is even “C# compatibility mode”, so that Spec# program can be compiled by “normal” C# compiler).

So, what’s the deal? Instead of sticking to Spec#, and finalizing its development and support in tools (especially that Spec# was really warmly accepted by development community), Microsoft invented the Code Contracts. And nothing would be wrong if it would offer anything new or improved compared to Spec#. Unfortunately, quite contrary, it is really big step backwards. The biggest problem in the Code Contracts, as I see it, is that contracts are specified in the method bodies, completely missing the whole point of design by contract how it is understood by e.g. Eiffel or Spec#. For example, how in heaven are you going to specify contracts for interfaces? (you cannot have method bodies in interfaces, right?) Of course, Microsoft guys will come with some ugly trick/hack here, and will allow contract specifications in interfaces, but how ugly that solution will be?

Then, there come aesthetic factors, closely related to code readability. A quick demo…

   string GetDescription(int x)
   {
      Contract.Requires(x > 0);
      Contract.Ensures(Contract.Result() != null);
      ...
      return SomeString;
   }

That was Code Contracts. Yay, how beautiful! (NOT!!!!!) Compare to the same in Spec#:

   string! GetDescription(int x)
      requires x > 0;
   {
      ...
      return SomeString;
   }

First of all, here the contract is clear from the method declaration, and there is no need to read the method body to get it. Notice string! syntax which specifies non-nullable string (all types can have ! added to them to specify that declared objects cannot be nulls) and eliminates the need for Ensures clause, and then clean and concise requires x > 0 clause. That’s it! Nothing more is needed!!! And here is a bit more elaborated sample, which shows both requires and ensures clauses:

   void int BinarySearch (int[]! a, int value)
      requires a.Length > 0;
      ensures result < a.Length;
      ensures a[result] == value;
   {
      ...
   }

Cool, isn’t it? Add to it invariants:

   class Word
   {
      private string! line; int start, length;
      public string ToString()
      {
         return line.Substring(start, length);
      }
      invariant 0 <= start && 0 <= length;
      invariant start + length <= line.length;
   }

ability to specify contracts on interfaces (look at those forall and old things!):

   interface IList
   {
      int Count { get; }
      T this[int i] { get; }
      public void Add(T x)
         ensures Count == old(Count) + 1;
         ensures forall{int i in (0:old(Count)); this[i] == old(this[i])};
         ensures this[old(Count)] == x;
   }

and other nice and powerful features, and you have really nice development environment that simplifies your life and helps you to write verifiable and correct code. But no! That would be way too simple and way too good, and instead we will get ugly Code Contracts. AAAaaa!!! I want Spec# baaaack!!!!

Now, as I said in the beginning of this post, I do not have hands-on experience with either of these technologies. But I believe that being more or less 20 years in the software development business is giving me enough experience to make a “high-view” judgment on technologies based on minimal data and “6th sense” (or gut-feeling, or instinct, or …). And my 6th sense is telling (yelling?) me that Code Contracs as they are proposed by Microsoft are not something that I will ever become excited about (as opposed to Microsoft’s Spec#).

Advertisements

5 thoughts on “.NET 4 Code Contracts

  1. Hi

    I think you missed the whole point of going the API way of supporting code contracts. By supporting code contracts through an API all .Net languages gets the power of code contracts for free. I do agree that the Spec# syntax is nicer – but the power behind is the same (I expect).

    And well, if code contracts turns out to be a huge success I guess that Anders will create some nice syntactic suger for it…

    :-) Thomas Jøhnk

  2. Well, I did not miss that point, but I think that the price of the API approach as opposed to the “proper” language integration is way too high. In fact, it might so high and the “newborn-baby” can be born dead. On the other end, with Spec# you do not need more than CLR 2.0 to run it, so, obviously, it is possible to do nice design-by-contract within the boundaries of the current runtime environment while not resorting to BCL.

  3. “Spec# syntax is nicer – but the power behind is the same (I expect).”

    Maybe…but then what’s the solution for interfaces or/and invariants with method-based CC?

  4. boj said: “Maybe…but then what’s the solution for interfaces or/and invariants with method-based CC?”

    EXACTLY! That’s my point too. But, unfortunately, Microsoft seems to somehow “deteriorate” nowadays rather quickly, so I see no hope – we will get API-base contracts and we can forget about Spec#. :(

  5. I reckon this is at least one step down from using something like PostSharp to add DBC to my code. I mean, suppose I sprinkle these Contract.Whatever calls all over the place, but then decide that a particular requirement – one that has been added to 100 places in my code – needs to be updated. How will Code Contracts handle that? At least, with PostSharp I can centralize some aspects so their management is handled from one location. :) So I’m gonna be a bit sceptical about this one…

Leave a Reply

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

WordPress.com Logo

You are commenting using your WordPress.com 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