c# – 代码合同:为什么一些不变量不被考虑在课外?
考虑这个不可变的类型:
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字段),在静态检查期间不能满足(参见上面的注释).这对我来说听起来有点怪异,因为它很容易证明: >设置是不可变的 我在这里错过了什么吗? 解决方法
在查看了
code contracts forum之后,我发现了
this similar question,其中一位开发人员的答案如下:
所以换句话说,你的选择是: >将Settings.Path属性设置为显式而不是自动,并在备份字段上指定不变量.为了满足您的不变量,您需要为该属性的set访问器添加一个前提条件:Contract.Requires(value!= null). 您可以选择使用Contract.Ensures(Contract.Result< string>()!= null)将getCondition添加到get访问器,但静态检查器不会以任何方式抱怨.>将Contract.Assume(settings.Path!= null)添加到Program类的构造函数. (编辑:李大同) 【声明】本站内容均来自网络,其相关言论仅代表作者个人观点,不代表本站立场。若无意侵犯到您的权利,请及时与联系站长删除相关内容! |