代码合同:为什么在课堂外不考虑某些不变量? [英] Code Contracts: Why are some invariants not considered outside the class?
问题描述
考虑这种不可变的类型:
Consider this immutable type:
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
参数值以遵守先前的合约不变式
- There is a contract invariant which ensures the
Path
property can never benull
- The constructor checks the
path
argument value to respect the previous contract invariant
此时,Setting
实例永远不能具有null
Path
属性.
At this point, a Setting
instance can never have a null
Path
property.
现在,看看这种类型:
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
字段上),在静态检查期间无法满足(参见上面的注释).听起来很奇怪,因为很容易证明这一点:
Basically, it has its own contract invariant (on _path
field) that can't be satisfied during static checking (cf. comment above). That sounds a bit weird to me, since it's easy to prove it:
-
settings
是不可变的 -
settings.Path
不能为null(因为Settings具有相应的协定不变式) - 因此通过将
settings.Path
分配给_path
,_path
不能为空
settings
is immutablesettings.Path
can't be null (because Settings has the corresponding contract invariant)- so by assigning
settings.Path
to_path
,_path
can't be null
我在这里错过了什么吗?
Did I miss something here?
推荐答案
检查代码合同论坛,我发现
After checking the code contracts forum, I found this similar question with the following answer from one of the developers:
我认为您遇到的行为是由正在进行的某些方法间推断引起的.静态检查器首先分析构造函数,然后分析属性和方法.分析Sample的构造函数时,它不知道msgContainer.Something!= null,因此会发出警告.解决此问题的一种方法是,在构造函数中添加一个假设msgContainer.Something!= null,或者最好在Something中添加后置条件!= null.
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.
换句话说,您的选择是:
So in other words, your options are:
-
使
Settings.Path
属性显式而不是自动,并在后备字段上指定不变式.为了满足您的不变性,您需要向属性的集合访问器添加一个前提条件:Contract.Requires(value != null)
.
Make the
Settings.Path
property explicit instead of automatic, and specify the invariant on the backing field instead. In order to satisfy your invariant, you will need to add a precondition to the property's set accessor:Contract.Requires(value != null)
.
您可以选择使用Contract.Ensures(Contract.Result<string>() != null)
将后置条件添加到get访问器,但是静态检查器不会以任何一种方式进行投诉.
You can optionally add a postcondition to the get accessor with Contract.Ensures(Contract.Result<string>() != null)
, but the static checker will not complain either way.
将Contract.Assume(settings.Path != null)
添加到Program
类的构造函数中.
Add Contract.Assume(settings.Path != null)
to the constructor of the Program
class.
这篇关于代码合同:为什么在课堂外不考虑某些不变量?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!