[Dafny] failed to verify forall expressions on local variables

Nov 8, 2012 at 1:57 AM

Hi,

Dafny complains that the loop cannot maintain the first loop invariant in the following code (the full set of code is at http://rise4fun.com/Dafny/gwqZ):

method PrepareFlush() returns (ret: array)
  requires Valid();
  modifies Pages.Repr;
  ensures Valid();
  ensures fresh(ret);
{
  var pages : array := Pages.Seal(Handle);
  var len := pages.Length;

  assert forall j :: 0 <= j < len ==> pages[j] != null && pages[j].CurrentState == 4 && pages[j].Valid();

  var res := new WriteBackEntry[len];
  var i := 0;

  assert forall j :: 0 <= j < len ==> pages[j] != null && pages[j].CurrentState == 4 && pages[j].Valid();

  while (i < len)
    invariant forall j :: 0 <= j < len ==> pages[j] != null && pages[j].CurrentState == 4 && pages[j].Valid();
    invariant fresh(res);
    modifies res;
  {
    res[i] := new WriteBackEntry.Init(pages[i].Buffer.Location, pages[i].Location);
    i := i + 1;
  }

  return res;
}

...
method Seal(handle: IntPtr) returns (ret : array)
  requires Valid();
  modifies Repr, Spine;
  ensures Valid();
  ensures Head == null && Length == 0;
  ensures ret != null && fresh(ret) && forall i :: 0 <= i < ret.Length ==> ret[i] != null && ret[i].CurrentState == 4 && ret[i].Valid();
  ensures Repr == {this} && Spine == [];

 

It seems that the Dafny thinks that the contents of the array pages have been changed due to the construction of the WriteBackEntry in the loop.

However, both res and pages are local, freshly allocated arrays, and they have different types (array<WriteBackEntry> vs. array<CachePage>).

I thought specifying fresh(ret) && frest(pages) should help but I had no luck.

What's the correct specification I should add into the program to verify it?

Thanks!