Dafny Loop Invariant Not Maintained By The Loop

Question

My task is to initialise an 8x8 matrix and ensure that all elements inside the matrix are set to zero. I am also required to use while loops and loop invariants for the implementation. My implementation looks like this:

method initMatrix(a: array2<int>)
    modifies a
    // require an 8 x 8 matrix
    requires a.Length0 == 8 && a.Length1 == 8
    // Ensures that all rows in the matrix are zeroes
    ensures forall row, col :: 0 <= row < a.Length0 && 0 <= col < a.Length1 ==> a[row, col] == 0
{
  var row : nat := 0;
  while(row < a.Length0)
    invariant 0 <= row <= a.Length0
    invariant forall i,j :: 0 <= i < row && 0 <= j < a.Length1 ==> a[i,j] == 0
  {
    var col : nat := 0;
    while(col < a.Length1)
      invariant 0 <= row <= a.Length0
      invariant 0 <= col <= a.Length1
      invariant forall i,j :: i == row && 0 <= j < col ==> a[i,j] == 0
    {
        a[row, col] := 0;
        col := col + 1;
    }
    row := row + 1;
  }
}

Logically, I think that all my quantifiers are correct. However, Dafny thinks that my loop invariant in the outer while loop

invariant forall i,j :: 0 <= i < row && 0 <= j < a.Length1 ==> a[i,j] == 0

is not being maintained by the loop.

I first suspected that the problem existed in my implementation. So I first ran the method without any pre and post conditions and printed all the elements in the array; the output was a matrix full of zeroes.

To be doubly sure that it is replacing all elements and not just using the zeroes from when the matrix was instantiated, I initialised all elements in the matrix to 1s and printed out all values inside it. The result was the same - all elements in the matrix were 1s.

From this experiment, I can conclude that the problem does not exist in my implementation but how I was defining my specifications.

I stepped through my algorithm by hand and found that it should logically work however, I think my understanding of how quantifiers work in loop invariants in Dafny may be skewed.

What exactly is happening when the condition 0 <= i < row && 0 <= j < a.Length1 is false? On the first iteration, the variable row is equal to 0, which does not satisfy the condition 0 <= i < row. Does it go through the first row and check if all elements in that row are zeroes or does it skip it?

Now what happens when it reaches the statement row := row + 1; on the initial iteration? Does the loop invariant invariant forall i,j :: 0 <= i < row && 0 <= j < a.Length1 ==> a[i,j] == 0 use the value of row upon entry (which is zero) or does it use the incremented value of row (1)?

Answer 1

The reason is that your inner loop's invariant is not strong enough. It only talks about the case where i == row, but doesn't say anything about what you've already accomplished for i < row.

Because of the way loop invariants work, Dafny essentially "forgets" this information since you don't "remember" it in the inner loop invariant.

You can fix your program by strengthening the inner loop invariant to talk about i < row. For example, as follows:

invariant 
  forall i,j :: 
    ((0 <= i < row && 0 <= j < a.Length1) || (i == row && 0 <= j < col)) ==> 
    a[i,j] == 0

which says that a is zero in all previous rows before row in all columns of those rows, and also in row, but then only up to column col.

---

Let me also take this opportunity to address a few other questions you asked when describing your debugging process.

What exactly is happening when the condition 0 <= i < row && 0 <= j < a.Length1 is false? On the first iteration, the variable row is equal to 0, which does not satisfy the condition 0 <= i < row. Does it go through the first row and check if all elements in that row are zeroes or does it skip it?

It "skips it". If some formula A is false, then A ==> B is true, without even looking at B.

Now what happens when it reaches the statement row := row + 1; on the initial iteration? Does the loop invariant invariant forall i,j :: 0 <= i < row && 0 <= j < a.Length1 ==> a[i,j] == 0 use the value of row upon entry (which is zero) or does it use the incremented value of row (1)?

The loop invariant is required to be true at the top of each loop. When you first enter the loop (before even evaluating the branch condition) it must be true. Also, after each execution of the body, it must be true.

In other words, it uses the incremented value of row (which is 1 after the first execution of the loop body).

---

Finally let me also comment on loop invariants more generally and how to debug them.

First, let me introduce James's First Law of Dafny Verification (which I just made up):

Just because Dafny reports a verification error doesn't mean the program is wrong.

Dafny's error messages (mostly) remind you of this Law, by using phrases like "might not hold", as in

This loop invariant might not be maintained by the loop.

Indeed, your example program was actually correct, as you demonstrated by actually running it. When run, it printed all zeroes, as expected. Yet Dafny still reported an error.

This is a price we pay for attacking undecidable problems like program verification. When using Dafny, your job is to convince it that your program is correct. When Dafny reports an error, it merely indicates that Dafny is not yet convinced.

Now, back to loop invariants. Why isn't Dafny convinced? Dafny verified three things about loop invariants.

1. Precondition from before the loop implies loop invariant (i.e., the loop invariant holds on entry).
2. Loop invariant is preserved by the body.
3. Loop invariant implies postcondition after the loop.

The hard one is usually #2. Dafny checks #2 in a kind of strange and unintuitive way, if you're not used to program verification. Dafny tries to prove that from an arbitrary state satisfying the loop invariant such that the loop's branch condition is true, if you then execute one iteration of the loop, then the loop invariant still holds.

The key here is arbitrary. It does not check that "every iteration of the loop that starts in a state that could actually happen during an execution of the program preserves the loop invariant". No. It checks that executions starting from arbitrary states preserve the loop invariant.

Returning to your example program, you've got a doubly nested loop. Dafny says it wasn't convinced that one of the outer loop's invariants was preserved by an execution of the outer loops body. What is the outer loops body? It's an execution of a bunch of iterations of the inner loop? How does Dafny reason about the inner loop? Only via its loop invariants.

So when proving #2 about the outer loop, the post condition for the inner loop is that it need to re-establish the outer loop invariant, which, mind you, says something about all rows up to row. Dafny then tries to prove this assuming only the inner loop invariant (and the negation of the loop's branch condition), which only talks about row row. Since the state is otherwise unconstrained, we can see why Dafny isn't convinced.