Static Checker Loses Type Contracts for .NET 4.5

Question

Hi,

The static checker cannot prove some basic FCL contracts when targeting the .NET Framework 4.5.

To repro, first create a new console application in VS 11 Beta and target the .NET Framework 4.0.  (That's 4.0, not 4.5.)  Enable static checking, add the following code and then build the project.

Note that all assertions are proven in the following code when targeting .NET 4.0.

using System;
using System.Diagnostics.Contracts;
using System.Linq;

namespace ConsoleApplication1
{
	class Program
	{
		static void Main()
		{
			var r = Enumerable.Range(1, 10);

			Contract.Assert(r != null);

			var s = new Observable().Subscribe(new Observer());

			Contract.Assert(s != null);
		}
	}

	class Observer : IObserver<int>
	{
		public void OnCompleted()
		{
		}

		public void OnError(Exception error)
		{
			Contract.Assert(error != null);
		}

		public void OnNext(int value)
		{
		}
	}

	class Observable : IObservable<int>
	{
		public IDisposable Subscribe(IObserver<int> observer)
		{
			Contract.Assert(observer != null);

			return new Disposable();
		}
	}

	class Disposable : IDisposable
	{
		public void Dispose()
		{
		}
	}
}

Now open the Properties window for the project, select the Application tab and change the Target Framework field to .NET Framework 4.5.

Rebuild the project and note that this time none of the the assertions related to IObservable<T> and IObserver<T> can be proven.  These interfaces are both defined in the FCL for .NET 4.0 under the System namespace, for which contracts are defined in the following assembly:

C:\Program Files (x86)\Microsoft\Contracts\Contracts\.NETFramework\v4.0\mscorlib.Contracts.dll.

Why aren't the contracts recognized when targeting .NET 4.5?

Also of interest is that the assertion related to Enumerable.Range can be proven by the static checker when targeting .NET 4.5.  Only the observable stuff isn't.

Thanks,
Dave

---

http://davesexton.com/blog