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

Question

Good day.

I'm testing out C# code contracts.
I've been working on some matrix implementations, and wanted to use code contracts to do arithmetic checking (eg. when is a matrix multiplication valid).

In order to store the data, I use a one dimensional array and access the data like this:

values[r * TotalColumns + c]  

r: row to access
c: column to access

My problem is:
Code contracts thinks that this access might be above the upper bounds of the array.
I think that I've given enough information, in order for the system to validate that this is not possible (see example bellow).

My question is:
Can you take a look at my example code and explain to me, what I did wrong and why Code Contracts still thinks that this array acces is unsafe?
The code in question is in the GetValue method and marked with a comment.

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

Answer 1

After some trial and error, I found the solution.
It seems, that Code Contracts validation process is not able to verify, that the formula

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

is always true with the given preconditions and invariants.

Solution:
By adding a Contract.Assume, the validation process stops exclaiming.

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

Conclusion:
While Code Contracts is good for simple verifications (boundary, etc.), it needs help from the developer when verifying more complex formulas.