Ensures Unproven via property when implementing interface

Question

I'm trying what, to me, seems like some fairly basic code contracts code. I've reduced it down to the following problem. The following fails the static analysis, with the message

CodeContracts: ensures unproven: this.Frozen

using System;
using System.Diagnostics.Contracts;

namespace PlayAreaCollection2010
{
    public class StrippedContract : IBasic
    {
        private bool _frozen = false;

        public void Freeze()
        {
            _frozen = true;
        }

        public bool Frozen { get { return _frozen; } }
    }

    [ContractClass(typeof(IBasicContract))]
    public interface IBasic
    {
        void Freeze();
        bool Frozen { get; }
    }

    [ContractClassFor(typeof(IBasic))]
    public abstract class IBasicContract : IBasic 
    {
        #region IBasic Members

        public void Freeze()
        {
            Contract.Ensures(this.Frozen);
        }

        public bool Frozen
        {
            get { return true;}
        }

        #endregion
    }
}

However, the following works fine and satisfies all checks:

using System;
using System.Diagnostics.Contracts;

namespace PlayAreaCollection2010
{
    public class StrippedContract
    {
        private bool _frozen = false;

        public void Freeze()
        {
            Contract.Ensures(this.Frozen);
            _frozen = true;
        }

        public bool Frozen { get { return _frozen; } }
    }

}

CodeContracts: Checked 1 assertion: 1 correct

What do I need to do to satisfy the static checker, when I've placed my contracts in the interface?

Answer 1

In your implementation of IBasic, StrippedContract, you will need to add a post-condition to the Frozen property:

public bool Frozen {
    get {
        Contract.Ensures(Contract.Result<bool>() == this._frozen);
        return _frozen;
    }
}

Alternatively, you could add the -infer command line option to the static checker in the Code Contracts tab of your project's properties. That will allow the static checker to infer this automatically.