property invariant incorrectly applied to backing field.

Question

Code contracts (1.4.5109.0) doesn't seem to notice the null reference exception in the following code. My brief investigations seem to indicate that if a field is set from the getter, then any invariant applied to the property also applies to the field.

	public class Functastic
	{
		public int Get()
		{
			return foo.GetHashCode();
		}

		object Foo
		{
			get { return foo ?? (foo = new object()); }
		}

		object foo;

		[ContractInvariantMethod]
		void ObjectInvariant()
		{
			Contract.Invariant(Foo != null);
		}
	}

Answer 1

Hi,

Invariants are intended to provide global internal post-conditions against private state, thus they are typically applied to fields, not properties.  Think of an invariant as defining the same post-condition in every method.

If your intention was to define a post-condition on Foo, then simply define a post-condition on Foo.

object Foo
{
	get
	{
		Contract.Ensures(Contract.Result<object>() != null);

		return foo ?? (foo = new object());
	}
}

Note that you can define invariants for automatic properties simply because there's no other way to define public post-conditions for them, but it's not the same thing.  In the following example, the invariant actually defines a public post-condition on Foo, but only because Foo is an automatic property and is public.

public object Foo { get; private set; }

[ContractInvariantMethod]
void ObjectInvariant()
{
	Contract.Invariant(Foo != null);
}

- Dave

---

http://davesexton.com/blog

Answer 2

I personally prefer to use ensures over invariant where possible as it keeps the contract with the property, but it seems some people prefer using invariant (presumably because it's easier to type - particularly with long-winded/compound return types). The issue is that code contracts allows using invariant on properties like this, but then does not handle it correctly. It's a bit disappointing to get null reference exceptions on our test system like this after code contracts has given it the green light.

Answer 3

Here's the reason why CC does not warn about it. If you evaluate your invariant, it has a side effect of setting the foo field. So if you use runtime checking, you don't get the

cnull deref, as the constructor will run the invariant at the end to check it, and it will succeed. From then on, foo is non null. Thus is simply the classic problem of having side effects in your assertions that your code depends on, but then you turn off the assertion checki,g and your code fails.

---

Cheers, -MaF (Manuel Fahndrich)