代码契约：映射到二维数组时数组访问上限警告

Question

美好的一天。

我正在测试 C# 代码合同。
我一直在研究一些矩阵实现，并想使用代码契约来进行算术检查（例如，矩阵乘法何时有效）。

为了存储数据，我使用一维数组并像这样访问数据：

values[r * TotalColumns + c]

r：要访问的行
c: 要访问的列

我的问题是：
代码契约认为此访问可能超出数组的上限。
我认为我已经提供了足够的信息，以便系统验证这是不可能的（参见下面的示例）。

我的问题是：
你能看看我的示例代码并向我解释一下我做错了什么以及为什么 Code Contracts 仍然认为这个数组访问是不安全的吗？
有问题的代码在 GetValue 方法中并标有注释。

public class Test
{
    [ContractPublicPropertyName("Values")]
    private readonly double[] values;

    [ContractPublicPropertyName("X")]
    private readonly int x;

    [ContractPublicPropertyName("Y")]
    private readonly int y;

    // Getter properties for required contract visibility.
    public double[] Values => this.values;
    public int X => this.x;
    public int Y => this.y;

    public Test(int x, int y)
    {
        Contract.Requires(x > 0);
        Contract.Requires(y > 0);

        Contract.Ensures(this.X == x);
        Contract.Ensures(this.Y == y);
        Contract.Ensures(this.Values.Length == this.X * this.Y);

        this.x = x;
        this.y = y;
        this.values = new double[x * y];
    }

    [Pure]
    public double GetValue(int xIndex, int yIndex)
    {
        Contract.Requires(xIndex >= 0);
        Contract.Requires(yIndex >= 0);
        Contract.Requires(xIndex < this.X);
        Contract.Requires(yIndex < this.Y);

        // Array access might be above the upper bound. 
        // Are you making some assumption on this.Y that the static checker is unaware of?
        return this.values[xIndex * this.Y + yIndex];
    }

    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
        Contract.Invariant(this.X > 0);
        Contract.Invariant(this.Y > 0);
        Contract.Invariant(this.values.Length == this.X * this.Y);
    }
}

谢谢

Answer 1

经过反复试验，我找到了解决方案。
看来，代码合同验证过程无法验证公式

xIndex * this.Y + yIndex < this.values.Length

对于给定的先决条件和不变量始终为真。

解决方案：
通过添加 Contract.Assume，验证过程停止惊呼。

public double GetValue(int xIndex, int yIndex)
{
    Contract.Requires(xIndex >= 0);
    Contract.Requires(yIndex >= 0);
    Contract.Requires(xIndex < this.X);
    Contract.Requires(yIndex < this.Y);

    // Help for Code Contract
    Contract.Assume(xIndex * this.Y + yIndex < this.values.Length);
    return this.values[xIndex * this.Y + yIndex];
}

结论：
虽然 Code Contracts 适用于简单的验证（边界等），但在验证更复杂的公式时需要开发人员的帮助。

代码契约：映射到二维数组时数组访问上限警告

Code contracts: Array access upper bound warning when mapping to 2d array

c#

math

code-contracts