CodeContracts：数组访问可能高于上限

Question

我从 CodeContracts 收到这些警告：

Array access might be above the upper bound. Did you meant 0 instead of 1?
Array access might be above the upper bound. Did you meant 1 instead of 2?
Array access might be above the upper bound. Did you meant 2 instead of 3?
Array access might be above the upper bound. Did you meant 3 instead of 4?

在这行代码中：

private readonly string[] _addr;

public string AddressLine1
{
    get
    {
        return _addr[0] ?? _addr[1] ?? _addr[2] ?? _addr[3];
    }
}

public string AddressLine2
{
    get
    {
        return _addr[1] ?? _addr[2] ?? _addr[3];
    }
}

public string AddressLine3
{
    get
    {
        return _addr[2] ?? _addr[3];
    }
}

如何告诉 Contracts 分析器这些索引保证在边界内？ _addr 在构造函数中被初始化为 string[4]。

Answer 1

我不知道 Contracts 分析器，但您的代码可能更简洁。您基本上是在重复仅找到第一个非空字符串的代码（如果最后一个元素为空，则无论如何都会返回）。我是使用 LINQ .FirstOrDefault 的粉丝，它可以让您找到与条件匹配的第一个元素（在您的情况下不为空）。如果没有找到这样的元素，它 returns 默认值（对于字符串它是 null）

return _addr.FirstOrDefault(str => str != null);

在此 .NET Fiddle 查看实际效果。

Answer 2

我能够通过向 class 添加一个定义不变量的方法来摆脱这些警告：

[ContractInvariantMethod]
private void AddressInvariants()
{
    Contract.Invariant(_addr.Length == 4);
}

但是，我认为您的代码中也存在错误。

如果_addr[0] == null和_addr[1] != null，则AddressLine1和AddressLine2return的值相同。这似乎是一个错误。

您可以通过使用@ryanyuyu 提到的内容来轻松解决此问题（并消除指定合同不变量的需要）：

public string AddressLine1
{
    get
    {
        // Use the first non-null element.
        return _addr.Where(x => x != null).FirstOrDefault();
    }
}

public string AddressLine2
{
    get
    {
        // Use the second non-null element.
        return _addr.Where(x => x != null).Skip(1).FirstOrDefault();
    }
}

public string AddressLine3
{
    get
    {
        // Use the third non-null element.
        return _addr.Where(x => x != null).Skip(2).FirstOrDefault();
    }
}

Answer 3

当 _addr 是 class 成员时，

ContractInvariantMethod 有效。但是 Contract.Assert() 也适用于局部变量。

static void MyParse(string foo)
{
    string[] split = foo.Split(',');
    Contract.Assert(split.Length == 4);

    string a = split[0];
    string b = split[1];
    string c = split[2];
    string d = split[3];
}

CodeContracts：数组访问可能高于上限

CodeContracts: Array access might be above the upper bound

c#

code-contracts