How do Code Contracts know that ToString overrides should not return null?

Question

I am using the Microsoft Code Contracts extension with C #. When I write a class with an overridden implementation of ToString that returns null, it correctly identifies the problem:

I assumed this was due to the fact that Microsoft uses code contracts directly and they added a call to Contract.Ensures to Object.ToString . However, when I look at the Object.ToString source code , I don't see any contracts (I see other contracts, but not the one I'm looking for). How do Code Contracts determine that a ToString should not return null?

Answer 1

This is the internal definition of the System.Object contract code: (link) . As you can see, they defined ToString() with this restriction:

 Contract.Ensures(Contract.Result<string>() != null); 

To answer your question, Code Contracts knows that it is not null due to the definition of an internal contract.