代码契约静态检查无法正常工作？

Question

我在构造函数 CodeTypes 中创建了一个带有代码契约的类，它有一个字符串属性列表。

Contract.Requires(type == CodeTypes.AdmitDx1 || type == CodeTypes.AdmitDx2
|| type == CodeTypes.AdmitDx3 || type == CodeTypes.DX 
|| type == CodeTypes.CPT || type == CodeTypes.HCPCS
|| type == CodeTypes.PX);

之后，在我使用此类的地方出现了警告，因为放入了不同的值。到目前为止一切顺利。

然后我找到了一段有抱怨的代码，添加了与 if 语句相反的内容并引发了异常。

警告仍然存在。

然后我在 if 语句的对面添加了一个 return 语句。

警告仍然存在。

然后，我在其中添加了一个大的 if/else，只有在满足合同中的条件时才调用该类。

警告仍然存在。

然后我用带有该条件的 if 语句包围合同。

警告消失了。

这是怎么回事？我预计第 3 个选项会起作用，而且我真的很想使用选项 1。解决此问题的最佳方法是什么？

编辑调用代码，合约存在于 CreateCodeFromType 的构造函数中：

//Type is an XElement that is passed into the method as a parameter
    if (type == null || (type.Value != CodeTypes.AdmitDx1 && type.Value != CodeTypes.AdmitDx2
    && type.Value != CodeTypes.AdmitDx3 && type.Value != CodeTypes.DX
    && type.Value != CodeTypes.CPT && type.Value != CodeTypes.HCPCS
    && type.Value != CodeTypes.PX))
    {
    throw new ValidationException("Type is invalid.");
    }
    else
    {
    var newCode = (new CreateCodeFromType(type.Value).CreateCode(term.Value));
    }

Answer 1

如果您提到的“其他代码段”位于另一个方法中，而不是构造函数中，那么您必须将参数保存到构造类型的字段中。在这种情况下，静态检查器无法在不满足条件时基于抛出或返回来检查任何内容，因为满足条件后，另一个线程可能会更改字段，从而导致条件失败。要防止在这种情况下出现警告，请使用 ContractInvariantMethodAttribute。

如果这段代码仍在构造函数中，我想不出静态检查器无法省略警告的任何原因（但话又说回来，如果您已经有了 Contract.Requires< /code> 前提条件？）。在这种情况下，我会责怪静态检查器的缺陷，就像斯蒂芬一样。

编辑：给出的例子我可以看到出了什么问题。

我说过静态检查器不能保证任何字段，因为其他线程可能会弄乱这些字段。 type.Value 是一个字段，因此静态检查器警告您可能违反合同是合乎逻辑的。我什至希望在您声称它消失的情况下出现警告（或者我误解了您）。为了解决这个问题，创建一个局部变量，然后你就得到了静态检查器可以推理的东西。
因此，请尝试以下操作：

if (type == null) throw new ArgumentNullException();
var xElementValue = type.Value;
if(xElementValue != CodeTypes.AdmitDx1 && xElementValue != CodeTypes.AdmitDx2
&& xElementValue != CodeTypes.AdmitDx3 && xElementValuee != CodeTypes.DX
&& xElementValue != CodeTypes.CPT && xElementValue != CodeTypes.HCPCS
&& xElementValue != CodeTypes.PX) throw new ValidationException("Type is invalid.");
//And now you should be able to give xElementValue as argument without receiving warnings. 

或者，如果您想使用合同，请使用

Contract.Requires(type != null);
var xElementValue = type.Value;
Contract.Requires(xElementValue == CodeTypes.AdmitDx1 || xElementValue== CodeTypes.AdmitDx2
|| xElementValue== CodeTypes.AdmitDx3 || xElementValue== CodeTypes.DX 
|| xElementValue== CodeTypes.CPT || xElementValue== CodeTypes.HCPCS
|| xElementValue == CodeTypes.PX);

“我希望这些解决方案中的任何一个都不会出现警告”。

Answer 2

静态检查器并不完美。它仍在开发中，即使完成后，它也无法了解一切。。

现在，您可以使用Contract.Assume 并传递条件向静态检查器提供提示。

另外，请及时了解 CC 版本的最新情况。目前版本为 1.4.31130.0，并计划很快发布另一个版本。在开发过程中，静态检查器在每个版本中都看到了增量改进。