Invariants on auto-properties?

Question

Hi,

Is it possible for me to define invariants on auto properties?
E.g.

1	public int Foo { get; set; }
2
3	[ContractInvariantMethod]
4	protected void ObjectInvariant()
5	{
6	Contract.Invariant(Foo >= 0);
7	}

Thanks, Matthias

Answer 1

Hi Matthias, thanks for giving Code Contracts a spin and asking questions!

In principle, you can write this invariant. Runtime checking will happily check it on the auto setter. Now, the issue of course is that anyone can violate the invariant by calling the setter with a negative value.

Now that is not so good, as an object invariant is an implementation contract and clients observing the requires on your methods should not be able to violate these invariants.

Thus, you would really need a precondition on the Foo setter to require value != null. Now given that it is an auto property, you can't write the contract due to the absence of a body.

So, to fix this, unfortunately, you would have to make the property explicit in order to write the contract.

One thing we might want to consider is for the contracts extraction to automatically lift your invariant to a preconditoin on the setter and a post condition on the getter. The trickyness with such automagics is that you might now write something like the following:

  Contract.Invariant( Foo >= Bar);

we would have to make sure all this works properly in general and has reasonable semantics.

---

Cheers, -MaF (Manuel Fahndrich)

Answer 2

Hi Manuel,

Thank you for your reply. I am (and have been) aware of the problem that the properties get/set are only methods and therefore should require a precondition (on set).

automagics sound nice but as you said: they must fit in every case. Perhaps there will be a way for such an approach - this would be really nice.

~ Matthias