Кодовые контракты: предупреждение о верхнем пределе доступа к массиву при сопоставлении с массивом 2d

Question

Добрый день.

Я тестирую контракты на код C#.
Я работал над некоторыми реализациями матриц и хотел использовать кодовые контракты для выполнения арифметической проверки (например, когда применяется умножение матрицы).

Для того, чтобы хранить данные, использую одномерный массив и получить доступ к данным, как это:

values[r * TotalColumns + c] 

г: строка для доступа
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 

всегда верно с заданными предпосылками и инварианты.

При добавлении договора.Пожалуйста, процесс проверки прекратит восклицание.

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

Вывод:
Хотя Кодовые контракты хорошо для простых проверок (границ и т.д.), он нуждается в помощи от разработчика при проверке более сложных формул.