Superfluous Code Contracts suggestions

Question

I have the following method:

static bool TextEquals(string text, char[] array, int start, int length)
{
    Contract.Requires(text != null);
    Contract.Requires(text.Length != length
                      || text.Length == 0
                      || (array != null && start >= 0 && start < array.Length));

    if (text.Length != length)
    {
        return false;
    }

    for (var i = 0; i < text.Length; ++i)
    {
        if (text[i] != array[start + i])
        {
            return false;
        }
    }

    return true;
}

However, Code Contracts is suggesting I add the following:

Contracts.Requires(text.Length == 0 || array != null || start < array.Length);
Contracts.Requires(text.Length == 0 || start < 0 || start < array.Length);

I am not seeing the added benefit of these two additional requirements. What path(s) are covered that the already existing requirements do not cover?

In particular, I do not see the case array == null && start < array.Length, which would be allowed by the first suggestion.

Is there any way to remove such suggestions?

Answer 1

I'm not quite sure what cases the new suggestions are trying to cover, but it seems to be a result of the static analyser having a hard time with your ORed clause.

It's a good idea to keep the Contract.Requires expressions as simple as possible, both to help the static analyser and to make it easier for human readers.

In this example, the following set of Requires clauses doesn't cause any additional suggestions to be raised:

Contract.Requires(text != null);
Contract.Requires(array != null);
Contract.Requires(start >= 0);
Contract.Requires(start <= array.Length - length);
Contract.Requires(length >= 0);

These are stricter than your originals, but don't seem unreasonable for callers.

In particular, notice that start <= array.Length - length is needed to prevent an array overflow on array[start + i]; the original condition start < array.Length is not sufficient, and might well be the root of your problem.

As an aside, if you're willing to use LINQ, you could rewrite this method more succinctly as follows:

static bool TextEquals2(string text, char[] array, int start, int length)
{
    Contract.Requires(text != null);
    Contract.Requires(array != null);
    Contract.Requires(start >= 0);
    Contract.Requires(length >= 0);

    return text.SequenceEqual(array.Skip(start).Take(length));
}