Code Contracts & Exception throwing difference

Question

I'm tying to understand Code Contracts advantages. I've wrote following code (from PEX + Code Contract introduction) to dig it.

public static string TrimAfter(string value, string suffix)
        {
            // <pex>
            Contract.Requires(suffix != (string)null);
            Contract.Requires
                (value.IndexOf(suffix) >= 0 && value.Length >= value.IndexOf(suffix));
            Contract.Requires(value != (string)null);
            // </pex>

            int index = value.IndexOf(suffix);
            if (index < 0)
                return value;

            return value.Substring(0, index);
        }

I called this method with nulls arguments and it was compiled. So it is not clear for me why it is better then throwing Exceptions. Could you guys explain me if Code Contracts really has any additional features? :) Thanks in advance.

Answer 1

1. Depending on your edition of VS(Premium or Ultimate if I remember correctly) you can get compile-time checking.
   The problem with this it is quite a bit of work to make the static checker happy. And I'm not sure if it's worth the effort for most programs. But perhaps a restricted subset such as null-checks could work well.
2. It's possible to automatically generate documentation from it.
3. It's shorter code, making people more likely to use it.
   The main point for me. I'm lazy and if writing checks gets easier I'm more likely to add additional checks. In particual I found the old style argument null checks a bit verbose.
4. You can specify an exception if you want, so you get the same outward behavior as with the old checks.

On the other hand it shouldn't be hard to parse the IL recognizing the old standard pattern for pre-condition checks and use that generate documentation.