Proving post conditions for code that does not implement Code Contracts

I'm learning how to design by contract by annotating my existing code with Contract.Requires() and Contract.Ensures() wherever I can.

After fixing the warnings that were actually caused by me, I started to notice that many methods in the framework do not ensure their post conditions. This concerns me, because the static checker is now giving me false positives about possible violations of my preconditions.

An example of a method that doesn't implement Code Contracts:

CultureInfo.GetCultureInfo(string)

As stated by the documentation:

Empty input will result in an invariant culture object.

Bad input will result in an exception.

In no case will it ever return null . Still, I can't use this:

Contracts.Requires(culture != null)

If I do, the static checker gives me this:

CodeContracts: requires unproven: culture != null

So, what do I do? Ignore the warning and write a comment with a link to the documentation? Or is there a way to prove post conditions for a method that someone else wrote?

edit

Making assumptions seems to make the analyzer shut up, but only until the next time that I write the same line of code.

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

Contract.Assume(culture != null);

MyPreconditionalMethod(culture);

I've looked at the [ContractClassFor()] attribute, but it requires a mutual handshake. :

---

Instead of Contracts.Requires(culture != null) , you could try Contracts.Assume(culture != null) . This gives the static analyzer a hint that, at that point in your code's execution, culture will not be null. The static analyzer will use this assumption when making further analysis on your code.

Update

So, if you have a method, say:

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);
}

The static analyzer won't be able to prove that result in SomeMethodThatCoordinatesActivities is greater than 0 , so you'll get a contract requires unproven: i warning. By using Contract.Assume in the calling method, you give a hint to the static analyzer to assume that at that point, result will be greater than 0 when calling SomeMethodThatDoesSomething and the unproven warning will not be given.

One interesting thing to note in the code above is that if I do actually provide the following post condition on the method DoSomething :

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

then I wouldn't need the Contract.Assumes(...) call in SomeMethodThatCoordinatesActivities because I've told the static analyzer that when DoSomething returns, it's result will be greater than 0 , so no assumption needs to be made. The static analyzer knows this will be true, and an unproven warning will never be given.

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

上一篇: 代码合同虚假肯定和压制

下一篇: 为不执行代码合同的代码验证后置条件