.NET 4 Code Contracts: do I need to include the same contracts twice?

Question

Let's say I have a method public void Foo(string bar) that the caller should not call with a null value of bar. Let's say I also have a method, call it private void FooImpl(string bar), that does the actual work of Foo. It's, of course, FooImpl that really requires non-nullness of bar, even though Foo is the public interface. And lets say I want to enforce this non-nullness using the .NET 4.0 code contracts.

Where do I put the contract?

If I do this:

public void Foo(string bar)
{
  this.FooImpl(bar);
}

private void FooImpl(string bar);
{
  Contract.Requires<ArgumentNullException>(bar != null);

  // Something that requires non-nullness, e.g.:
  bar.Contains("test");
}

then the static checker complains that Foo is calling FooImpl with a possibly-null value, and suggests I add the non-null contract to Foo. OK, so I guess I can't delegate my contract-checking/exception-throwing to the implementation methods.

But if I try to put it in the public interface, i.e.:

public void Foo(string bar)
{
  Contract.Requires<ArgumentNullException>(bar != null);

  this.FooImpl(bar);
}

private void FooImpl(string bar);
{
  bar.Contains("test");
}

then the static checker complains that FooImpl is calling Contains on a possibly-null value---even though the only place from which FooImpl is ever called in the code is from Foo, which itself ensures that it will never call FooImpl with a null value.

---

So, do I need to include the same contract twice? Or should I just ignore the static checker? I know it's kind of a source of busywork and shouldn't be relied upon, but I would hope that it had some way of handling this basic, and presumably common, scenario.

Answer 1

To appease the static checker, I'd probably use Contract.Assume() on the inner function, rather than the normal Contract functions, so it wouldn't be an exact copy of the existing contract - you don't want or need an actual runtime check when in that inner function.

As to why its not smart enough to deduce that this function is only called from one other place, I'm not sure.

Answer 2

Short answer: Yes.

You should add preconditions everywhere you want Code Contracts to prevent things like nullreference exceptions. This sometimes means it will look like you are adding the same contracts twice.

In this particular case, it's obvious to you that FooImpl is only called from a method which already has a precondition.

However, the static checker evaluates the FooImpl method independently from other methods. In this example you just pass the bar value from Foo ( where you know bar is not null ), but the static checker has no certainty that you didn't manipulate bar, possibly causing it to be null.

Also, you should consider that in the future you might have calls to the FooImpl method from methods which do not have a precondition to check whether or not bar is null. You'd want to have the static checker prevent nullreference exceptions from happening in those cases too.