CODEWITHSUNDEEP
matrixdafnyformal-verificationproof-of-correctness
carbonaramerchant
carbonaramerchant

Reputation: 15

Proving correctness of Matrix Addition

I want to prove the correctness of 2D matrix addition in Dafny (using the VSCode extension) with the aim of identifying SMT-proveable loop invariants. I believe this should be fairly straight forward as the computations only involve addition.

My implementation involves 2 loops. An outer loop iterating over the rows. And an inner loop iterating over the columns. Dafny is throwing errors regarding my outer loop invariant.

I believe I have not 'helped' Dafny enough with reasoning about the invariant. However I am unsure with how to proceed.

Below is my implementation. Without the assertion at the end of the outer loop, Dafny reports this invariant could not be proved to be maintained by the loop. When I include the assertion of the invariant at the end of the outer loop body, Dafny reports assertion might not hold.

method Order2Addition(m1: array2<int>, m2: array2<int>, m3: array2<int>)
    requires m1 != m3 && m2 != m3
    requires m1.Length0 == m2.Length0 == m3.Length0 && m1.Length1 == m2.Length1 == m3.Length1
    ensures CorrectMatrixAddition(m1, m2, m3)
    modifies m3
    {
        var rows: int := m1.Length0;
        assert(rows == m2.Length0 && rows == m3.Length0);
        var cols: int := m1.Length1;
        assert(cols == m2.Length1 && cols == m3.Length1);
        var i: int := 0;
        while (i < rows)
            invariant 0 <= i <= rows
            // All rows up to row i-1 are correct
            invariant forall i':int, j':int :: 0 <= i' < i && 0 <= j' < cols ==> m3[i', j'] == m1[i', j'] + m2[i', j']
            decreases rows - i
            modifies m3
        {
            var j: int := 0;
            while (j < cols)
                invariant 0 <= j <= cols
                // All column values on row i, up to column j-1 are correct
                invariant forall j': int :: 0 <= j' < j ==> m3[i, j'] == m1[i, j'] + m2[i, j'] 
                decreases cols - j
                modifies m3
            {
                m3[i, j] := m1[i, j] + m2[i, j];
                j := j + 1;
            }
            i := i + 1;
            assert(forall i':int, j':int :: 0 <= i' < i && 0 <= j' < cols ==> m3[i', j'] == m1[i', j'] + m2[i', j']);
        }
    }

predicate CorrectMatrixAddition(m1: array2<int>, m2: array2<int>, m3: array2<int>)
    requires m1.Length0 == m2.Length0 == m3.Length0 && m1.Length1 == m2.Length1 == m3.Length1
    requires m1 != m3 && m2 != m3
    reads m1, m2, m3
{
    forall i: int, j: int {:trigger m3[i,j]} ::  0 <= i < m1.Length0 && 0 <= j < m1.Length1 ==> m3[i, j] == m1[i, j] + m2[i, j]
}

Upvotes: 0

Views: 54

Answers (2)

Rustan Leino
Rustan Leino

Reputation: 2097

The reason your program does not verify is that the inner loop also needs the invariant that "All rows up to row i-1 are correct". (My book "Program Proofs" discusses this point in section 14.1.1.)

You can also shorten many things. The following is a version that verifies:

method Order2Addition(m1: array2<int>, m2: array2<int>, m3: array2<int>)
  requires m1 != m3 && m2 != m3
  requires m1.Length0 == m2.Length0 == m3.Length0 && m1.Length1 == m2.Length1 == m3.Length1
  ensures CorrectMatrixAddition(m1, m2, m3)
  modifies m3
{
  var rows, cols := m1.Length0, m1.Length1;
  var i := 0;
  while i < rows
    invariant 0 <= i <= rows
    // All rows up to row i-1 are correct
    invariant forall i', j' :: 0 <= i' < i && 0 <= j' < cols ==> m3[i', j'] == m1[i', j'] + m2[i', j']
  {
    var j := 0;
    while j < cols
      invariant 0 <= j <= cols
      // All column values on row i, up to column j-1 are correct
      invariant forall i', j' :: 0 <= i' < i && 0 <= j' < cols ==> m3[i', j'] == m1[i', j'] + m2[i', j']
      invariant forall j' :: 0 <= j' < j ==> m3[i, j'] == m1[i, j'] + m2[i, j'] 
    {
      m3[i, j] := m1[i, j] + m2[i, j];
      j := j + 1;
    }
    i := i + 1;
  }
}

predicate CorrectMatrixAddition(m1: array2<int>, m2: array2<int>, m3: array2<int>)
  requires m1.Length0 == m2.Length0 == m3.Length0 && m1.Length1 == m2.Length1 == m3.Length1
  reads m1, m2, m3
{
  forall i, j :: 0 <= i < m1.Length0 && 0 <= j < m1.Length1 ==> m3[i, j] == m1[i, j] + m2[i, j]
}

You can also use for loops instead of the while loops, if you prefer.

In fact, you can also do this example in Dafny without any loops at all, which saves you having to write any loop invariants (but I suppose that won't help your goal of trying to identify SMT-solvable loop invariants). You can replace the body of the method with this aggregate statement:

  forall i, j | 0 <= i < m1.Length0 && 0 <= j < m1.Length1 {
    m3[i, j] := m1[i, j] + m2[i, j];
  }

Upvotes: 0

Hath995
Hath995

Reputation: 1300

Not quite sure what is going wrong with your implementation. My guess would be you might have the wrong index specified somewhere or the wrong range.

I have a similar implementation here

I applied your predicate to that method and it didn't immediately verify because of your precondition that the arrays be different, by relaxing/removing that require it then verified.

Arrays are mutable in Dafny and using them requires understanding the frame system which is painfully under-documented. Unless you really need the mutability using datatypes rather than arrays will make your life easier.

There are a few useful examples of using the frame system on the Dafny blog but the general gist of it is that everything that changed must be specified and everything that is unchanged must be specified, also it only applies to heap objects like arrays or classes, it does not apply to variables using primitive or immutable types. Here is an implementation of the sieve of Eratosthenes as an example.

Upvotes: 0

Related Questions