I recently ran into a problem when trying to use Code Contracts on Auto-Implemented Properties (i.e. Automatic Properties) combined with a C# interface.

I started with a normal interface IScriptInvokerImpl where I wanted to define a method for running a PowerShell script and a public property for the PowerShell instance being used:

public interface IScriptInvokerImpl
{
  PowerShell Powershell { get; }

  bool RunPowershell(string pathToScriptFile, Dictionary<string, object> parameters, ref List<object> scriptResult);
}

A first implementation

So a first implementation of the interface might look like this:

public class ScriptInvokerImpl : IScriptInvokerImpl
{
  public PowerShell Powershell { get; }

  public bool RunPowershell(string pathToScriptFile, Dictionary<string, object> parameters, ref List<object> scriptResult)
  {
    Contract.Requires(File.Exists(pathToScriptFile));
    Contract.Requires(null != parameters);
    Contract.Requires(null != scriptResult);
    Contract.Requires(null != Powershell);
    Contract.Ensures(null != scriptResult);

    var scriptInvokerImplPowerShellResult = Powershell
      .AddCommand(pathToScriptFile)
      .AddParameters(parameters)
      .Invoke();

    // example result evaluation
    return null != scriptInvokerImplPowerShellResult ? true : false;
  }
}

Introducing interface contracts

However, having these pre- and post-conditions on the actual implementation is not what I really want, so I have to define an abstract ‘contract’ class for the interface:

[ContractClassFor(typeof(IScriptInvokerImpl))]
public abstract class ContractClassForIScriptInvokerImpl : IScriptInvokerImpl
{
  PowerShell IScriptInvokerImpl.Powershell
  {
    get
    {
      Contract.Ensures(null != Contract.Result<PowerShell>());

      return default(PowerShell);
    }
  }

  public bool RunPowershell(string pathToScriptFile, Dictionary<string, object> parameters, ref List<object> scriptResult)
  {
    Contract.Requires(File.Exists(pathToScriptFile));
    Contract.Requires(null != parameters);
    Contract.Requires(null != scriptResult);
    Contract.Ensures(null != scriptResult);

    return default(bool);
  }
}

Note that I moved the pre-condition check of the Powershell property as a post-condition check to the body of the auto-implemented property itself. And of course I also have to annotate the interface with [ContractClass(typeof(ContractClassForIScriptInvokerImpl))] as well to make that contract work.

The problem

So far, so good. However, I also want to have a constructor on my implementation to allow for a PowerShell instance to be injected into the the class.

public class ScriptInvokerImpl : IScriptInvokerImpl
{
  public PowerShell Powershell { get; private set; }

  public ScriptInvokerImpl()
  {
    Powershell = PowerShell.Create();
  }

  public ScriptInvokerImpl(PowerShell powershell)
  {
    Powershell = powershell;
  }
}

This surely does work as expected. There is only a nuisance that I will get an exception as a post-condition when trying to access the Powershell property on a get operation if the constructor would have been called with a null reference on the powershell parameter. I certainly could add another pre-condition check as a Contract.Requires(null != powershell); to the constructor, but in case I have more occurrences where I set the PowerShell auto-implemented property I would have to repeat that code over and over again.

And here comes the actual problem: it is neither possible to add this constraint in the interface contract as the private setter is not (and cannot be) part of the interface:

PowerShell IScriptInvokerImpl.Powershell
{
  get
  {
    Contract.Ensures(null != Contract.Result<PowerShell>());

    return default(PowerShell);
  }
  private set
  {
    Contract.Requires(null != value);
  }
}

>> Error: ‘IScriptInvokerImpl.Powershell.set’ adds an accessor
>> not found in interface member ‘IScriptInvokerImpl.Powershell’
>>
>> Error: The modifier ‘private’ is not valid for this item

Nor is it possible to expand the body of the private setter of the auto-implemented property while leaving the body of the getter empty:

public PowerShell Powershell 
{ 
  get; 
  private set
  {
    Contract.Requires(null != value);
  }
}

>> Error: ‘ScriptInvokerImpl.Powershell.get’ must declare a body
>> because it is not marked abstract, extern, or partial

Option 1: Backing field

Adding a body to the getter only works when adding an explicit backing field for this property (which then in turn is not an auto-implemented property any more):

private PowerShell _Powershell;
public PowerShell Powershell 
{ 
  get
  {
    return _Powershell;
  }
  private set
  {
    Contract.Requires(null != value);
  }
}

This will lead us to the problem that direct access to the field is again not covered by a contract and will allow for possible null references.

Option 2: ContractInvariantMethod

There is a solution for that by using [ContractInvariantMethod] on the class implementation like this:

[ContractInvariantMethod]
private void ContractInvariantMethod() 
{
  Contract.Invariant(null != this.Powershell);
}

This works well, however we than have the getter property checked twice (once because of the Contract.Ensures constraint in the contract class of the interface and once because of the Contract.Invariant statement in the class implementation itself, where the latter is being evaluated first upon method exit). Though this is only a simple null check in our case I don’t see this as a viable option either.

The Solution

So we have two options:

1. Use a private backing field with the possible pitfall that the class can still access the field directly without any constraints applied to it (which would require some discipline of the programmer not to do this)
2. Use a ContractInvariant method and have parameter checks being applied twice (plus a special behaviour which I talk about at the end of the post)

So in the end we cannot use auto-implemented properties with interfaces with non-public access modifiers. I would opt towards Option 2 because of performance reasons and the final solution with a private backing field might look like this:

• The interface IScriptInvokerImpl

// interface
[ContractClass(typeof(ContractClassForIScriptInvokerImpl))]
public interface IScriptInvokerImpl
{
  PowerShell Powershell { get; }

  bool RunPowershell(string pathToScriptFile, Dictionary<string, object> parameters, ref List<object> scriptResult);
}

• The code contract for the interface as abstract class ContractClassForIScriptInvokerImpl

[ContractClassFor(typeof(IScriptInvokerImpl))]
public abstract class ContractClassForIScriptInvokerImpl : IScriptInvokerImpl
{
  PowerShell IScriptInvokerImpl.Powershell
  {
    get
    {
      Contract.Ensures(null != Contract.Result<PowerShell>());

      return default(PowerShell);
    }
  }

  public bool RunPowershell(string pathToScriptFile, Dictionary<string, object> parameters, ref List<object> scriptResult)
  {
    Contract.Requires(File.Exists(pathToScriptFile));
    Contract.Requires(null != parameters);
    Contract.Requires(null != scriptResult);
    Contract.Ensures(null != scriptResult);

    return default(bool);
  }
}

• The actual implementation of ScriptInvokerImpl

public class ScriptInvokerImpl : IScriptInvokerImpl
{
  public ScriptInvokerImpl()
  {
    Powershell = PowerShell.Create();
  }

  public ScriptInvokerImpl(PowerShell powershell)
  {
    Powershell = powershell;
    isInternalPowerShellInstance = true;
  }

  private PowerShell _Powershell;
  public PowerShell Powershell 
  { 
    get
    {
      return _Powershell;
    }
    private set
    {
      Contract.Requires(null != value);

      _Powershell = value;
    }
  }

  public bool RunPowershell(string pathToScriptFile, Dictionary<string, object> parameters, ref List<object> scriptResult)
  {
    var scriptInvokerImplPowerShellResult = Powershell
      .AddCommand(pathToScriptFile)
      .AddParameters(parameters)
      .Invoke();

    // example result evaluation
    return null != scriptInvokerImplPowerShellResult ? true : false;
  }
}

Side note about ContractInvariant checks

There is a fundamental difference between using Contract.Requires and Contract.Ensures in getter and setter methods of properties with a backing field and using a Contract.Invariant method annotation for an auto-implemented property. The constraints on the getter and setter methods are checked on EVERY access whereas the invariant is only checked AT THE END of the method that accesses the property.

So the following code would NOT throw an exception:

public class ContractInvariantExample
{
  public int NonZeroNumber { get; set; }

  [ContractInvariantMethod]
  private void ContractInvariantMethod()
  {
    Contract.Invariant(0 != NonZeroNumber);
  }

  public ContractInvariantExample()
  {
    NonZeroNumber = 0;  ///< will not throw a contract exception
    NonZeroNumber = 42;
  }
}

In the example above we assign the property NonZeroNumber a value of 0 and subsequently a value of 42. The first assignment is clearly a violation of the contract and its statement: Contract.Invariant(0 != NonZeroNumber);. However, as the contract is only checked after the method (the constructor in this case) executed and returns, the invariant holds true.

In contrast to this example where we have a private backing field for the property:

public class ContractInPropertyBodyExample
{
  private string _NonEmptyString;
  public string NonEmptyString
  {
    get 
    {
      Contract.Ensures(string.IsNullOrEmpty(Contract.Result<string>()));

      return _NonEmptyString; 
    }
    set 
    {
      Contract.Requires(string.IsNullOrEmpty(value));

      _NonEmptyString = value; 
    }
  }

  public ContractInPropertyBodyExample()
  {
    NonEmptyString = "";  ///< will throw a contract exception
    NonEmptyString = "tralala";
  }
}

Here we first clear the contents of the string and then assign it the value of tralala. However as the constraint Contract.Requires is checked immediately while trying to set the property an exception is thrown before a new (valid) value can be assigned.
So if you want to make sure your constraints are ALWAYS valid use properties with backing fields along with explicit pre- and post-conditions inside the body of the property accessors.

For more information see 2.3.1 Invariants on Automatic Properties.

If you want to test for yourself have a look at the test cases in this example: