public class Settings
{
public string Path { get; private set; }
[ContractInvariantMethod]
private void ObjectInvariants()
{
Contract.Invariant(Path != null);
}
public Settings(string path)
{
Contract.Requires(path != null);
Path = path;
}
}
两件事要注意：
>有一个契约不变式,确保Path属性永远不能为null
>构造函数检查路径参数值以符合先前的契约不变量
此时,设置实例永远不能有空的Path属性.
现在,看看这个类型：
public class Program
{
private readonly string _path;
[ContractInvariantMethod]
private void ObjectInvariants()
{
Contract.Invariant(_path != null);
}
public Program(Settings settings)
{
Contract.Requires(settings != null);
_path = settings.Path;
} // <------ "CodeContracts: invariant unproven: _path != null"
}
基本上,它有自己的契约不变量(在_path字段),在静态检查期间不能满足(参见上面的注释).这对我来说听起来有点怪异,因为它很容易证明：
>设置是不可变的
> settings.Path不能为空(因为设置具有相应的契约不变量)
>所以通过将settings.Path分配给_path,_path不能为空
我在这里错过了什么吗？
解决方法
I think the behavior you are experiencing is caused by some inter-method inference that is going on. The static checker first analyzes the constructors,then the properties and then the methods. When analyzing the constructor of Sample,it does not know that msgContainer.Something != null so it issues the warning. A way to solve it,is either by adding an assumption msgContainer.Something != null in the constuctor,or better to add the postcondition != null to Something.
所以换句话说,你的选择是：
>将Settings.Path属性设置为显式而不是自动,并在备份字段上指定不变量.为了满足您的不变量,您需要为该属性的set访问器添加一个前提条件：Contract.Requires(value！= null).
您可以选择使用Contract.Ensures(Contract.Result< string>()！= null)将getCondition添加到get访问器,但静态检查器不会以任何方式抱怨.>将Contract.Assume(settings.Path！= null)添加到Program类的构造函数.
