代码契约:映射到2d数组时，数组访问上限警告

本文关键字：数组 访问 警告 代码 映射 2d 契约 | 更新日期: 2023-09-27 18:16:23

大家好。

我正在测试c#代码契约。
我一直致力于一些矩阵实现，并希望使用代码契约来做算术检查(例如。

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

values[r * TotalColumns + c]

r: row访问
C: column to access

我的问题是:
代码契约认为这种访问可能超出了数组的上界。
我认为我已经给出了足够的信息，以便系统验证这是不可能的(参见下面的示例)。 我的问题是:
你能看看我的示例代码，并向我解释，我做错了什么，为什么代码合同仍然认为这个数组访问是不安全的?
有问题的代码位于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);
    }
}

Thank you

代码契约:映射到2d数组时，数组访问上限警告

经过反复试验，我找到了解决办法。
看起来，Code Contracts验证过程无法验证公式

xIndex * this.Y + yIndex < this.values.Length
在给定的前提条件和不变量下

总是为真。


解决方案:通过添加契约。假设验证过程停止惊呼。

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

结论:
虽然代码契约适用于简单的验证(边界等)，但在验证更复杂的公式时，它需要开发人员的帮助。

相关文章：