Contract.​Requires(ar​gument != null); // superfluous?

Simple question: Is this programming practice superfluous or what do you think? Since the type-system of C# is not equipped to directly express non-nullable reference types one can do it explicitly but it leads to this kind of contract everywhere. It should be possible to deduce these contracts from the source itself.

Perhaps the complement: Contract.Ensures(Contract.Result<T>() != null); is less superfluous.

In Spec# they noticed that this happens a lot, so decided that an exclamation mark after the type of an argument is a shorthand, so 

void foo(object p1) { Contract.Requires(p1 != NULL); dostuff(); } 

is the same as

void foo(object! p1) { dostuff() }

In C# since all reference types are nullable, the requires statement is still necessary if you want the verifier to prove you won't hit null-reference exceptions at runtime.

I'm not convinced about that.

Say for example:

public static IEnumerable<TSource> Repeat(this IEnumerable<TSource> source)
{
    while (true)
        foreach (var e in source)
            yield return e;
}

I say the verifier should be able to infer the precondition that Contract.Requires(source != null).

As for the Spec# reference: the default should be unnullable, i.e. T! would be the default, hence superfluous, hence T, if a reference type should be treated as Spec# T!. Or that's my simple point of view heh.

 I don't have the Code Contracts static verifier running so I don't if it can infer anything by itself.

@exoteric:How do you know that Repeat is not designed to throw a null reference exception when passed a null reference? If that is the behavior desired, you would not want Contract.Requires(source != null). I agree that in most cases you want that inferred, but unless you can infer 100% of the time...

@Frank Hileman: I made it and it isn't! Seriously speaking though, that is an interesting point of view. Have you ever seen code that expects null reference exceptions? Even so, if the static verifier can detect it, you will (hopefully) be warned that the method does not accept nulls statically at verification-time. Run-time you should be able to turn the contracts off and have the same behavior as before. End result is that the calling code is safe-guarded against forwarding null references (wohn't be let thru verification otherwise) and also doesn't have to protect against "DOH" responses from the called method.

@exoteric:

The problem is an IEnumerable is a reference type. So null is a valid input to the function. The function is verified in isolation, and not through its usage.

Solution: Non Null Reference Types but that'll require I think a major change to the CLR.

 Have you ever seen code that expects null reference exceptions?  C# has an operator that expects null.  ?. The null coalescing dot (Edit: That's Nemerle's)  I meant ?? 

VB.NET has IsNothing

@AdamSpeight2008: I seem to remember there is a static verifier for Java that does nullness analysis. That could at least provide warnings so you can clean up your code.

I don't see the CLR has to support anything per se for C# to have non-null references, just metadata - Spec# already does this, right? Non-nullable reference is just typing information that that can be erased like in the good old Java days.

One could argue that given:

o.f(x)

you almost never expect o to be null but x may be null; although fundamentally the whole idea of nullable reference types by default is awkward. I prefer how functional programming languages do it.

The reason that T is nullable and T! is non-nullable is that Spec# is designed on-top of C#, where all objects are nullable, so changing that semantic would break the backwards compatibly. C# chose that because it inherits from C++ where NULL is always a valid pointer and C/C++ doesn't have a concept of non-nullable pointers.

Your idea is basically a good one, but you are underestimating the difficulty of writing a good verifier - the problem with your idea is when we hit either recursive functions, subordinate calls or loop-constructs that can significantly obfuscate the control flow to make verification hard - take the following function for instance:

string Foo(object o)
{
  for(int i = 0; i < 7; i++)
  {
    if(i == 1) { o = new object(); }
    if(i == 2) { return o.ToString(); }
  } 
  throw new NotImplementedException();
}

The verifier would really struggle to prove that in this particular instance it doesn't matter that o can be null (or indeed anything) because by the time o is used it will be guaranteed to be valid. This makes some of the "smarts" that people often want in verifiers hard to implement in worst-case scenarios. The Spec# verifier tries to play it dumb by asking the author to give some hints so that it only has to prove that the contracts are valid, rather than try to compute a minimal requirement for the function.