代码契约：为什么一些不变量在课堂之外没有被考虑？考虑这个不可变类型：publicclassSettings{publicstringPath{get;私有集；}[ContractInvariantMethod]privatevoidObjectInvariants(){Contract.Invariant(Path!=null);}公共设置（字符串路径）{合同。需要（路径！=空）；路径=路径；}}此处需要注意两点：此时，Setting实例永远不能具有空Path属性。现在，看看这个类型：publicclassProgram{privatereadonlystring_path;[ContractInvariantMethod]privatevoidObjectInvariants(){Contract.Invariant(_path!=null);}publicProgram(Settingssettings){Contract.Requires(settings!=null);_path=设置.Path;}//<------"CodeContracts:invariantunproven:_path!=null"}基本上，它有自己的契约不变量（在_path字段上），在静态检查期间不可满足（见上面的注释）。这对我来说听起来有点奇怪，因为很容易证明：我在这里遗漏了什么吗？查看CodeContracts论坛后，我发现了一个类似的问题，其中一位开发人员给出了以下答案：我认为您遇到的行为是由正在进行的某些方法间推理引起的。静态检查器首先分析构造函数，然后是属性，然后是方法。在分析Sample的构造函数时，它不知道msgContainer.Something！=null，因此它会发出警告。解决的办法就是在构造函数中加一个假设的msgContainer.Something！=null，或者更好的后置条件！=null被添加到Something。换句话说，您的选择是：使Settings.Path属性显式而不是自动的，并在支持字段上指定不变量。为了满足您的不变量，您需要向属性的set访问器添加一个前提条件：Contract.Requires(value!=null)。您可以选择使用Contract.Ensures(Contract.Result()!=null)向get访问器添加后置条件，但静态检查器不会以任何方式抱怨。将Contract.Assume(settings.Path!=null)添加到Program类的构造函数中。不变量不适用于私人成员，这就是为什么您实际上不能以这种方式拥有它的原因，希望这会有所帮助。以上是C#学习教程：代码契约：为什么有些不变量在课堂之外没有考虑？如果所有分享的内容对你有用，需要进一步了解C#学习教程，希望大家多多关注。本文收集自网络，不代表立场。如涉及侵权，请点击右侧联系管理员删除。如需转载请注明出处：
