为不执行代码合同的代码验证后置条件

我正在学习如何通过Contract.Requires()和Contract.Ensures()尽我所能注释我现有的代码。

修复了实际上由我造成的警告后，我开始注意到框架中的许多方法不能确保他们的发布条件。 这关系到我，因为静态检查器现在给我误报可能违反我的先决条件。

不实施代码合同的方法的一个例子：

CultureInfo.GetCultureInfo(string)

正如文件所述：

空输入将导致不变的文化对象。

错误的输入将导致异常。

在任何情况下它都不会返回null 。 不过，我不能使用这个：

Contracts.Requires(culture != null)

如果我这样做，静态检查器给我这个：

CodeContracts：需要未经证实的：culture！= null

那么，我该怎么做？ 忽略警告并写下带有指向文档链接的评论？ 还是有办法证明其他人写的方法的后置条件？

编辑

做出假设似乎会让分析仪闭嘴，但直到下一次我写同一行代码。

var culture = CultureInfo.GetCultureInfo("en");

Contract.Assume(culture != null);

MyPreconditionalMethod(culture);

我查看了[ContractClassFor()]属性，但它需要相互握手。 ：

---

而不是Contracts.Requires(culture != null) ，你可以尝试Contracts.Assume(culture != null) 。 这给了静态分析器一个暗示，在你的代码执行的那一刻， culture不会为空。 在对代码进行进一步分析时，静态分析器将使用此假设。

更新

所以，如果你有一个方法，说：

public int DoSomething(SomeObject o, int i)
{
    Contract.Requires(o != null);
    Contract.Requires(i > 0);
    // You could combine the conditionals in the Requires: o != null && i > 0

    Contract.Ensures(/* some post condition */);

    int returnValue = 0;
    // Do some stuff

    return returnValue;
}

public void SomeMethodThatDoesSomething(int i)
{
    Contract.Requires(i > 0)

    // Do some stuff
}

public void SomeMethodThatCoordinatesActivities()
{
    int result = DoSomething(new SomeObject(), 10);

    Contract.Assume(result > 0);
    SomeMethodThatDoesSomething(result);
}

静态分析器将无法证明SomeMethodThatCoordinatesActivities中的result大于0 ，因此您将得到一份contract requires unproven: i警告。 通过在调用方法中使用Contract.Assume ，您可以给静态分析器一个提示，假设在那个时候，调用SomeMethodThatDoesSomething时result将大于0 ，并且不会给出unproven警告。

上面的代码中需要注意的一点是，如果我实际上在方法DoSomething上提供了以下后置条件：

Contract.Ensures(Contract.Result<int>() > 0);

那么我不需要在SomeMethodThatCoordinatesActivities调用Contract.Assumes(...) ，因为我告诉过静态分析器，当DoSomething返回时，结果会大于0 ，因此不需要做出任何假设。 静态分析器知道这将是真实的，并且永远不会给出unproven警告。

链接地址: http://www.djcxy.com/p/23745.html

上一篇: Proving post conditions for code that does not implement Code Contracts

下一篇: Code contracts static checking does not seem to be working