CODEWITHSUNDEEP
arraysverificationdafny
Matthew Garlock
Matthew Garlock

Reputation: 23

Why does this Dafny assertion involving arrays fail?

I am working on a verified implementation of gaussian elimination and I am having problems verifying this super simple method that adds the contents of the array b to the contents of the array a. Here is the code.

method addAssign(a: array<real>, b: array<real>)
   requires a != null && b != null && a.Length == b.Length;
   modifies a
   ensures forall k:: 0 <= k < a.Length ==> a[k] == old(a[k]) + b[k];
{
   var i := 0;
   assert a == old(a);
   while(i < a.Length)
      invariant 0 <= i <= a.Length
      invariant forall k:: i <= k < a.Length ==> a[k] == old(a[k])
      invariant forall k:: 0 <= k < i ==> a[k] == old(a[k]) + b[k];
   {
      assert a[i] == old(a[i]); // dafny verifies this
      a[i] := a[i] + b[i];
      assert a[i] == old(a[i]) + b[i]; // dafny says this is an assertion violation
      i := i + 1;
   }
}

Upvotes: 2

Views: 1912

Answers (1)

John Coleman
John Coleman

Reputation: 51998

(I deleted my first answer since it didn't work).

It seems that the problem is that Dafny detects potential aliasing problems. As an experiment, I first modified your code to get an even easier function which does verify:

method addOne(a: array<real>)
   requires a != null;
   modifies a;
   ensures forall k:: 0 <= k < a.Length ==> a[k] == old(a[k]) + 1.0;
{
   var i := 0;
   assert a == old(a);
   while(i < a.Length)
      invariant 0 <= i <= a.Length
      invariant forall k:: i <= k < a.Length ==> a[k] == old(a[k])
      invariant forall k:: 0 <= k < i ==> a[k] == old(a[k]) + 1.0;
   {
      assert a[i] == old(a[i]); // dafny verifies this
      a[i] := a[i] + 1.0;
      assert a[i] == old(a[i]) + 1.0; // dafny *doesn't* say this is an assertion violation
      i := i + 1;
   }
}

The only difference is that I am using a literal real (1.0) rather than a real drawn from b. Why should that make a difference?

Well suppose that you invoke your method with a call which looks like 

addAssign(a,a)

then in the body of the function b and a both refer to the same array. Suppose, for example, that a[0] is 1.0. Then in the first pass through the loop you execute a[0] := a[0] + b[0].

This sets a[0] to 2.0. But -- it also sets b[0] to 2.0.

But in this situation assert a[0] == old(a[0]) + b[0] is equivalent to

assert 2.0 == 1.0 + 2.0 -- which should fail.

By the way -- the following does verify:

method addAssign(a: array<real>, b: array<real>)
   requires a != null && b != null && a.Length == b.Length;
   modifies a;
   ensures forall k:: 0 <= k < a.Length ==> a[k] == old(a[k]) + old(b[k]);
{
   var i := 0;
   assert a == old(a);
   while(i < a.Length)
      invariant 0 <= i <= a.Length
      invariant forall k:: i <= k < a.Length ==> a[k] == old(a[k])
      invariant forall k:: 0 <= k < i ==> a[k] == old(a[k]) + old(b[k]);
   {
      assert a[i] == old(a[i]); // dafny verifies this
      a[i] := a[i] + b[i];
      assert a[i] == old(a[i]) + old(b[i]); // and also this!
      i := i + 1;
   }
}

Upvotes: 2

Related Questions