Ensures Unproven via property when implementing interface
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 = tru开发者_Python百科e;
}
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?
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.
精彩评论