Dafny: Verification of the most simple array summation does not work. Can somebody explain me why?-CodePudding

When I have three arrays and c[j] := b[h] a[i]. The verification c[j] == b[h] a[i] does not work. Can somebody please explain me why? It is assured that all indices are in range and all three arrays are int arrays. Here is my code:

method addThreeArrays(a: array<int>, b: array<int>, c: array<int>, h: int, i: int, j: int)
  modifies c
  requires 0 <= h < a.Length
  requires 0 <= i < b.Length
  requires 0 <= j < c.Length
  
  ensures c[j] == a[h]   b[i]
  {
    c[j] := a[h]   b[i];
  }

I expected the "ensures" line to be true. But Dafny gives the error. "Postcondition" might not hold. I just want to understand where my error is. Thank you guys! :)

CodePudding user response：

Since Dafny arrays are allocated on the heap, they are allowed to alias. So it is possible to call your method with, for example, c and a pointing to the same array in memory. Also, it's possible that j == h. In that scenario, the postcondition may not hold since writing to c[j] also wrote to a[h] (since c and a point to the same array and j == h).

You can fix this by adding a precondition that a != c and b != c.

CodePudding user response：

I wrote your example to the Dafny project and how we would solve it using code actions: https://github.com/dafny-lang/dafny/issues/3102

I reproduce the detailed solution here to compute a weakest precondition.

Making the assertion explicit would result in

  {
    c[j] := a[h]   b[i];
    assert c[j] == a[h]   b[i];
  }

Now, we cannot just "move the assert up", because we would otherwise have to reason about the state of the heap after the assignment, and old@ cannot refer to a label defined afterwards yet. So, the next step would be to introduce the label and do the weakest precondition calculus below the assignment

  {
    label before: // Added
    c[j] := a[h]   b[i];
    assert old@before(a[h]   b[i]) == a[h]   b[i]; // Added, now failing
    assert c[j] == a[h]   b[i];
  }

The nice thing about that is that it would help the user discover the "old" syntax in a natural way. Because the weakest precondition now sees two more potentially conflicting references, it could suggest the following code action to remove the reference to the heap after the assignment:

  {
    label before: // Added
    c[j] := a[h]   b[i];
    assert old@before(a[h]   b[i]) == (if a == c && j == h then old@before(a[h]   b[i]) else a[h])   (if b == c && j == i then old@before(a[h]   b[i]) else b[i]); 
    assert c[j] == a[h]   b[i];
  }

Now, because this expression does not refer at all to the heap after the assignment c[j}, the weakest precondition calculus would be able to move this assertion before and remove the old@ expressions.

  {
    assert a[h]   b[i] == (if a == c && j == h then a[h]   b[i] else a[h])   (if b == c && j == i then a[h]   b[i] else b[i]); // Just added, now failing.
    label before:
    c[j] := a[h]   b[i];
    assert old@before(a[h]   b[i]) == (if a == c && j == h then old@before(a[h]   b[i]) else a[h])   (if b == c && j == i then old@before(a[h]   b[i]) else b[i]); 
    assert old@before(a[h]   b[i]) == a[h]   b[i];
    assert c[j] == a[h]   b[i];
  }

and eventually move it to a requires of the method. The user can then refine this weakest precondition so that they only keep a != c && b != c if they wanted to. Or not.