Are Code contracts worth anything?

Question

I don't want to insult anyone, but has anyone ever gotten anything useful out of using code contracts? Well, maybe except a massive head ache. I've only tried Code contracts on a small library of mine, and all I felt was I kept repeating over and over again, that the parameters were != null. Then after stating some parameter p was != null, Then, sigh, I had to prove that a property e on p was != null. Finally, I ran into a situation where I had to prove some obscure situation I never figured out. And what did I get out of all my troubles? Nothing!

Now I know the documentation states that using statical analysis is a straneous endavour, however, this begs the question if anyone ever felt they'd gained anything from using code contracts? I know the Eiffel language and the history and motivations for contracts in general. However, I find it difficult to believe I have to wrestle so much just to be able to avoid an occasional NullReferenceException.

Your thoughts are appreciated.

Answer 1

In clean code you need those checks anyways. And why not do them in a way that creates the documentation of that for you? The code itself looks clearer, and it's machine readable too, so that info ends up in the documentation automatically.

The requires clauses replace the parameter checking =>throw exception stuff. And the ensures clauses replace some Debug.Asserts

You don't need to use the static prover if you don't want to.

I'd like having a version of the static prover which tries to prove that there are situations where the contracts are violated, and trying to prove there are none. And doing that doesn't treat other functions as blackboxes only defined by their contract. So you don't need to work that much.

Answer 2

My $.02:

I don't know if there's a clear "right" answer to this question. They do make your code more robust against bad input, but it also makes your code not fail fast in the event of weird calling behavior. Or if your code does eventually fail, it fails somewhere that's unrelated to the null-check that blew up, which makes it a bit more of a chore to track down where stuff blew up.

So to me, it's really a question of whether or not you want to fail fast and hard (i.e. you let that NULL ptr blow the system up so you can post-mortem debug and hopefully resolve the issue) or try to recover from whatever weird error resulted in a bad argument in the first place.

If caller and callee both consist of code I wrote, I prefer to fail fast. If it's code I'm going to distribute for other people to use, I prefer to check the arguments and return an error code (e.g. check for null, return E_POINTER). Internally, if my code fails fast then debugging is typically a lot easier.

Answer 3

Though I've never used them and just read the documentation for them, there's one obvious benefit -- explicit, readable, self-documenting code.

It also encourages defensive coding. If you aren't validating your inputs or checking your outputs, then there's probably no value in them for your project.

Consider the following:

   if (myObject == null) 
      throw new ArgumentNullException("myObject");

becomes

   Contract.Requires(myObject != null);

Code Contracts makes the requirements explicit in code so you get self-documenting code (and this is using them with just pre-conditions).

Your code may not doing any input validation or output checking now but as it gets used, it will.

Answer 4

And what did I get out of all my troubles? Nothing!

They are not for you, they are for users of your library.
You might never reap the benefits yourself, as you probably know your lib very well.

Answer 5

I've experimented with code contracts a fair amount on some internal libraries and my general sense of them at this point is:

• The process of reasoning about and writing the contracts has helped me to identify boundary case issues in my code, particularly as I started writing contracts with index validation.

• The biggest benefit I saw with contracts was when I fully specified a library with contracts, from bottom to top. Rigorously writing and statically proving contracts has a tendency to push responsibility upward, until you reach a natural point to do validation, at the public interface. The contracts on all the sub-components helps to build confidence that your top layer is performing all of the necessary validation to ensure that they are working correctly.

• The syntax is rather clunky, due to the cross-language nature of the current implementation of Contracts. I really hope that the Spec# concept of non-nullable reference types gets incorporated into C# eventually, as that will cover a large percentage of the contract usage.

• The static prover is sophisticated, but there are limits to its ability to reason. When you push up against those limits, you can go through a lot of gymnastics to try to make things prove. There's definitely a point of diminishing returns here.

• It feels wrong at first to force things to prove by adding Assume clauses, but sometimes, while writing out the Assume, I suddenly realized that there really was some underlying assumption required for the logic, which I had simply taken for granted. I think there's value in being explicit about your assumptions and it's just a bonus that these assumptions take part in the static analysis.

• The contracts do combine nicely with Pex, which is a great way to discover the bewildering variety of odd boundary cases you're not covering with your code. The contracts tell Pex what not to worry about and Pex helps you to find new cases to cover with your contracts.

• My net sense is that contracts are a very positive development, but still a bit too awkward for me to deploy with code I'm writing for clients. I plan to continue experimenting with them for internal code and I'm hopeful that both the syntax and static analysis will improve with time.