Code contracts on auto-implemented properties

Is there any way to put contracts on automatically implemented properties in .NET? (And how if the answe开发者_Go百科r is 'Yes')?

(I assume using .NET code contracts from DevLabs)

Yes, this is possible - all that is needed is to add your contract condition to the [ContractInvariantMethod] method in your class, which then adds the equivalent Requires precondition to the automatic setter, and a post condition Ensures is added to the get. From section 2.3.1 of the Reference

As the example illustrates, invariants on auto-properties turn into:

1. A precondition for the setter
2. A postcondition for the getter
3. An invariant for the underlying backing field

And by example:

public int MyProperty { get; private set ;}

[ContractInvariantMethod]
private void ObjectInvariant ()
{
  Contract.Invariant ( this.MyProperty >= 0 );
}

"Is equivalent to the following code:"

private int backingFieldForMyProperty;
public int MyProperty 
{
  get 
  {
    Contract.Ensures(Contract.Result<int>() >= 0);
    return this.backingFieldForMyProperty;
  }

  private set 
  {
    Contract.Requires(value >= 0);
    this.backingFieldForMyProperty = value;
  }
}

[ContractInvariantMethod]
private void ObjectInvariant () 
{
  Contract.Invariant ( this.backingFieldForMyProperty >= 0 );
...

I'm thinking not, but you could easily write a snippet that would do this. If you go this route, here is a free snippet editor that will make the task very easy.

Thanks Porges.

My mistake was that I actually used ReleaseRequires option, which, indeed, deals only with generic version of the method, Requires<T>.

Invariant which is put on an auto-implemented property is really turned into a Requires precondition, but it's not generic - that's why it didn't work using this option.

What to do:

• VARIANT 1. Consider using code snippets and lovely Requires<T> instead of auto-implemented properties - that enables us to use exceptions of desired type.

• VARIANT 2. Change the option ReleaseRequires to Preconditions in the Code Contracts' options and feel free to write invariants on auto-properties - the rewriter tool will automatically change them into the Requires. However, they will be non-generic - that means, in case of contract broken, a ContractException will be thrown and there is no way to change this behaviour.

Thanks everyone for the help!