[Dafny]Cannot verify the assertion which is the loop invariant

Apr 20, 2013 at 3:01 PM
I specified the LCP problem: (http://rise4fun.com/Dafny/QPa8).

I think we translate a while statement (while(E) invariant J; {S}) as:
  assert J;
  havoc xs;
  assume J;
  if (E){ 
     S; 
     assert J;
     assume false;
  } else {}
Hence I would like to know why I cannot verify the assertion which is exactly the loop invariant.

According the execution traces at the end, I think the assertion (assertion1) below failed at anon23:
assert (forall z#5: int :: true ==> 0 <= z#5 && z#5 < result#3 ==> $Unbox(read($Heap, a#0, IndexField(x#1 + z#5))): int == $Unbox(read($Heap, a#0, IndexField(y#2 + z#5))): int);
However, the assertion(assertion2) below has been asserted in the loop head at anon0:
assert $w0 ==> (forall z#4: int :: true ==> 0 <= z#4 && z#4 < result#3 ==> $Unbox(read($Heap, a#0, IndexField(x#1 + z#4))): int == $Unbox(read($Heap, a#0, IndexField(y#2 + z#4))): int);
I am thinking assertion2 would be taken as an assumption in the following proof, which could entail assertion1. Therefore I am confused why the assertion1 failed.

Execution traces:
anon0:
    $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: $o != null && read($Heap, $o, alloc) ==> false);
    // ----- assignment statement ----- C:\Docs\2013SpringWork\paperreview\lcp.dfy(11,10)
    assume true;
    assume true;
    result#3 := 0;
    assume {:captureState "C:\Docs\2013SpringWork\paperreview\lcp.dfy(11,10)"} true;
    // ----- while statement ----- C:\Docs\2013SpringWork\paperreview\lcp.dfy(12,3)
    $PreLoopHeap0 := $Heap;
    $decr0$init$0 := _System.array.Length(a#0) - result#3;
    havoc $w0;
    goto anon25_LoopHead;

  anon25_LoopHead:
    assume $w0 ==> (0 <= result#3 ==> true) && (0 <= result#3 && result#3 + x#1 <= _System.array.Length(a#0) ==> true) && (0 <= result#3 && result#3 + x#1 <= _System.array.Length(a#0) && result#3 + y#2 <= _System.array.Length(a#0) ==> true);
    assert $w0 ==> 0 <= result#3;
    assert $w0 ==> result#3 + x#1 <= _System.array.Length(a#0);
    assert $w0 ==> result#3 + y#2 <= _System.array.Length(a#0);
    assert $w0 ==> x#1 != y#2;
    assume $w0 ==> (forall z#4: int :: true ==> (0 <= z#4 ==> true) && (0 <= z#4 && z#4 < result#3 ==> true));
    assert $w0 ==> (forall z#4: int :: true ==> 0 <= z#4 && z#4 < result#3 ==> $Unbox(read($Heap, a#0, IndexField(x#1 + z#4))): int == $Unbox(read($Heap, a#0, IndexField(y#2 + z#4))): int);
    assume (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(old($Heap), $o, alloc) ==> read($Heap, $o, $f) == read($PreLoopHeap0, $o, $f));
    assume $HeapSucc($PreLoopHeap0, $Heap);
    assume (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read($PreLoopHeap0, $o, alloc) ==> read($Heap, $o, $f) == read($PreLoopHeap0, $o, $f) || $_Frame[$o, $f]);
    assume _System.array.Length(a#0) - result#3 <= $decr0$init$0 && (_System.array.Length(a#0) - result#3 == $decr0$init$0 ==> true);
    goto anon25_LoopDone, anon25_LoopBody;

  anon25_LoopBody:
    assume {:partition} true;
    goto anon26_Then, anon26_Else;

  anon26_Else:
    assume {:partition} $w0;
    goto anon13;

  anon13:
    assert a#0 != null;
    goto anon32_Then, anon32_Else;

  anon32_Then:
    assume {:partition} x#1 + result#3 < _System.array.Length(a#0);
    assert a#0 != null;
    goto anon15;

  anon15:
    goto anon33_Then, anon33_Else;

  anon33_Then:
    assume {:partition} x#1 + result#3 < _System.array.Length(a#0) && y#2 + result#3 < _System.array.Length(a#0);
    assert a#0 != null;
    assert 0 <= x#1 + result#3 && x#1 + result#3 < _System.array.Length(a#0);
    assert a#0 != null;
    assert 0 <= y#2 + result#3 && y#2 + result#3 < _System.array.Length(a#0);
    goto anon17;

  anon17:
    assume (x#1 + result#3 < _System.array.Length(a#0) ==> true) && (x#1 + result#3 < _System.array.Length(a#0) && y#2 + result#3 < _System.array.Length(a#0) ==> true);
    goto anon34_Then, anon34_Else;

  anon34_Else:
    assume {:partition} x#1 + result#3 < _System.array.Length(a#0) && y#2 + result#3 < _System.array.Length(a#0) && $Unbox(read($Heap, a#0, IndexField(x#1 + result#3))): int == $Unbox(read($Heap, a#0, IndexField(y#2 + result#3))): int;
    goto anon19;

  anon19:
    assume {:captureState "C:\Docs\2013SpringWork\paperreview\lcp.dfy(12,3): loop entered"} true;
    $decr0$0 := _System.array.Length(a#0) - result#3;
    // ----- assert statement ----- C:\Docs\2013SpringWork\paperreview\lcp.dfy(18,5)
    havoc z#13;
    goto anon35_Then, anon35_Else;

  anon35_Then:
    assume {:partition} 0 <= z#13;
    goto anon21;

 anon21:
    goto anon36_Then, anon36_Else;

anon36_Then:
    assume {:partition} 0 <= z#13 && z#13 < result#3;
    assert a#0 != null;
    assert {:subsumption 0} 0 <= x#1 + z#13 && x#1 + z#13 < _System.array.Length(a#0);
    assert a#0 != null;
    assert {:subsumption 0} 0 <= y#2 + z#13 && y#2 + z#13 < _System.array.Length(a#0);
    goto anon23;

  anon23:
    assume (forall z#5: int :: true ==> (0 <= z#5 ==> true) && (0 <= z#5 && z#5 < result#3 ==> true));
    assert (forall z#5: int :: true ==> 0 <= z#5 && z#5 < result#3 ==> $Unbox(read($Heap, a#0, IndexField(x#1 + z#5))): int == $Unbox(read($Heap, a#0, IndexField(y#2 + z#5))): int);
    // ----- assignment statement ----- C:\Docs\2013SpringWork\paperreview\lcp.dfy(20,12)
    assume true;
    assume true;
    result#3 := result#3 + 1;
    assume {:captureState "C:\Docs\2013SpringWork\paperreview\lcp.dfy(20,12)"} true;
    assert 0 <= $decr0$0 || _System.array.Length(a#0) - result#3 == $decr0$0;
    assert _System.array.Length(a#0) - result#3 < $decr0$0;
    assume (0 <= result#3 ==> true) && (0 <= result#3 && result#3 + x#1 <= _System.array.Length(a#0) ==> true) && (0 <= result#3 && result#3 + x#1 <= _System.array.Length(a#0) && result#3 + y#2 <= _System.array.Length(a#0) ==> true);
    assume (forall z#4: int :: true ==> (0 <= z#4 ==> true) && (0 <= z#4 && z#4 < result#3 ==> true));
    goto anon25_LoopHead;
Apr 24, 2013 at 1:17 AM
Hi Yuyan,

The problem you have encountered has to do with triggering. But before I explain it, let me just remark about the loops. My remark is that I think it's much easier to understand the problem from just look at the Dafny code itself, without going into the details of how loops are translated from Dafny into Boogie (and, as you have included above, even inside Boogie when Boogie cuts back-edges). To get started debugging your program in the context of Dafny, you don't need to know the translation of loops; you just need to know that a loop invariant is assumed on entry to the loop body (and is checked again at the end of the loop body).

Here's the issue you have encountered. You have a loop invariant that you have written as follows:
invariant (forall z :: 0 <= z  && z < result ==> a[x+z] == a[y+z]);
While I think this is the most natural (and most symmetric) way to express this property, it doesn't work well with Z3. The reason is that, to use this quantifier, Z3 wants to instantiate it, and it instantiates quantifiers based on matching patterns. As expressed here, the quantifier has no matching pattern, and therefore Z3 is not able to make use of it.

I cannot give full justice to understanding matching patterns here, but let me say what matters in this situation. The matching pattern is a term that includes the bound variable (z), is larger than the bound variable itself (that is, z is not a valid matching pattern), and is not so large that it includes an interpreted symbol (here, +). Intuitively, if there were a matching pattern T(z), then if Z3 happened to encounter a term of the form T(m) for some term m, then it would instantiate the quantifier with z := m.

To rewrite your loop invariant so that Z3 can find a matching pattern for it, you can write:
invariant forall z :: x <= z < x + result ==> a[z] == a[z-x+y];
Here, the term a[z] is a good matching pattern. If you change your loop invariant to this one, then your program will verify (even without the assert in the loop body).

See http://rise4fun.com/Dafny/XKuk.

Rustan
Apr 24, 2013 at 1:51 PM
Hi Rustan,

After checking some information about e-matching, it is making lots of sense to me. I appreciate your detailed explaination.

Thanks
Yuyan
Oct 23, 2013 at 4:55 PM
Hi Rustan,

I (more or less) understood the e-matching problem you explained to Yuyan, but I can not fix what is the problem with the following version

method lcp(a: array<int>, x: int, y: int) returns(result: int)
requires a != null;
requires 0 <= x < a.Length;
requires 0 <= y < a.Length;
requires x != y;
ensures 0 <= result;
ensures result <= a.Length - x && result <= a.Length - y;
// New formulation of post-condition
ensures result>=1 ==> a[x..x+result-1] == a[y..y+result-1];
ensures result == a.Length - x || result == a.Length - y || a[x+result] != a[y+result];

{
result := 0;
while(x + result < a.Length && y + result < a.Length && a[x+result] == a[y+result])
    invariant 0 <= result && result + x <= a.Length && result + y <= a.Length && x != y;
    // New formulation of invariant:
    invariant result == 0 || (result>=1 && a[x .. x+result-1] == a[y .. y+result-1]) ;
    decreases a.Length - result;
      { 
        result := result + 1;
      }
}

Thanks,
Paqui Lucio
Nov 12, 2014 at 7:18 PM
The following version is also correct:
method lcp (a: array<int>, x: int, y: int) returns(result: int)
  requires a != null;
  requires 0 <= x && x < a.Length;
  requires 0 <= y && y < a.Length;
  requires x != y;
  ensures 0 <= result;
  ensures result <= a.Length - x && result <= a.Length - y;
  ensures result == a.Length - x || result == a.Length - y || a[x+result] != a[y+result];
{
result := 0;
while(x + result < a.Length && y + result < a.Length && a[x+result] == a[y+result])
    invariant 0 <= result && result + x <= a.Length && result + y <= a.Length && x != y;
    invariant result == 0 || (result>=1 && a[x .. x+result] == a[y .. y+result]) ;
      { 
        result := result + 1;
      }
}
Nov 12, 2014 at 7:31 PM
Edited Nov 12, 2014 at 7:37 PM
.... and in this version http://rise4fun.com/Dafny/XDbdh the contract is better specified (in my opinion).
Paqui
Nov 12, 2014 at 11:10 PM
Hi Paqui,

Am I understanding it correctly that, since your final version above works, you are happy? That is, did you figure out the issue yourself? (Since it's verifying, I'm not sure if any question remains about it.)

Thanks,
Rustan
Nov 13, 2014 at 9:06 AM
Hi Rustan,
Yes you are right, I just wanted to communicate this solution.
Thanks,
Paqui