Dafny: rotated region of an array method verification

Question

this proof gives an infinite loop in Dafnys' verifier:

// Status: verifier infinite loop
// rotates a region of the array by one place forward
method displace(arr: array<int>, start: nat, len: nat) returns (r: array<int>)
  requires arr != null
  requires start + len <= arr.Length
  // returned array is the same size as input arr
  ensures r != null && r.Length == arr.Length
  // elements before the start of the region are unchanged
  ensures arr[..start] == r[..start]
  // elements after the end of the rhe region are unchanged
  ensures arr[(start + len)..] == r[(start + len)..]
  // elements in the region are skewed by one in a positive direction and wrap
  // around
  ensures forall k :: 0 <= k < len
                 ==> r[start + ((k + 1) % len)] == arr[start + k]
{
    var i: nat := 0;
    r := new int[arr.Length];
    // just make a copy of the array
    while i < arr.Length
      invariant i <= arr.Length
      invariant forall k: nat :: k < i ==> r[k] == arr[k]
    {
        r[i] := arr[i];
        i := i + 1;
    }

    i := 0;
    // rotate the region
    while i < len
      invariant 0 <= i <= len
      invariant arr[..start] == r[..start]
      invariant arr[(start + len)..] == r[(start + len)..]
      invariant forall k :: 0 <= k < i 
                ==> r[start + ((k + 1) % len)] == arr[start + k]
    {
        r[start + ((i + 1) % len)] := arr[start + i];
        i := i + 1;
    }
}

which points to some sort of undecidability issue or is it? Is there a better way to present this problem to avoid the infinite loop?

previous version:

method displace(arr: array<int>, start: nat, len: nat) returns (r: array<int>)
  requires arr != null
  requires start + len <= arr.Length
  // returned array is the same size as input arr
  ensures r != null && r.Length == arr.Length
  // elements before the start of the region are unchanged
  ensures arr[..start] == r[..start]
  // elements after the end of the rhe region are unchanged
  ensures arr[(start + len)..] == r[(start + len)..]
  // elements in the region are skewed by one in a positive direction and wrap around
  ensures forall k :: start <= k < (start + len)
                 ==> r[start + (((k + 1) - start) % len)] == arr[k]
{
    var i: nat := 0;
    r := new int[arr.Length];

    while i < arr.Length
      invariant i <= arr.Length
      invariant forall k: nat :: k < i ==> r[k] == arr[k]
    {
        r[i] := arr[i];
        i := i + 1;
    }

    i := start;

    while i < (start + len)
      invariant start <= i <= (start + len)
      invariant arr[..start] == r[..start]
      invariant arr[(start + len)..] == r[(start + len)..]
      invariant forall k :: start <= k < i
                ==> r[start + (((k + 1) - start) % len)] == arr[k]
    {
        r[start + (((i + 1) - start) % len)] := arr[i];
        i := i + 1;
    }
}

What do you mean by infinite loop? Do you mean that the Dafny verification step times out? Have you tried some of the Dafny command line arguments - particularly the "keep going splits" options? — lexicalscope, Jan 13 '16 at 22:00
um, no I had no idea such an argument existed or what it does, but I am just a noob... I meant that running dafny like this './dafny blah/displace.dfy' from a prompt on linux seems to run for one hell of a long time. — vivichrist, Feb 03 '16 at 02:07
Usually you should pass a value to the timeout option when running Dafny from the command line. My experience has been that almost all procedures that are going to verify do so relatively quickly. Most lemmas I have written will verify within 10seconds, a few take up to 60seconds, almost never do they take more than 60seconds but still verify within the time I am willing to wait. I pretty much never want to run Dafny without setting a timeout. — lexicalscope, Feb 03 '16 at 09:36

score 1 · Accepted Answer · edited May 23 '17 at 10:28

Non-linear arithmetic is not decidable. So I suspect that using the % operator to define rotation is the root cause of your problem. Below is a version, that does verify, that defines rotation using only linear integer arithmetic.

See also How does Z3 handle non-linear integer arithmetic?

predicate rotated(o:seq<int>, r:seq<int>) 
  requires |o| == |r|
{
  (forall i :: 1 <= i < |o| ==> r[i] == o[i-1]) &&
  (|o| > 0 ==> r[0] == o[|o|-1])  
}

// Status: verifier infinite loop
// rotates a region of the array by one place forward
method displace(arr: array<int>, start: nat, len: nat) returns (r: array<int>)
  requires arr != null
  requires start + len <= arr.Length
  ensures r != null && r.Length == arr.Length
  ensures arr[..start] == r[..start]
  ensures arr[(start + len)..] == r[(start + len)..]
  ensures rotated(arr[start .. start+len], r[start .. start+len])
{
    var i: nat := 0;
    r := new int[arr.Length];
    while i < start
      invariant i <= start
      invariant forall k: nat :: k < i ==> r[k] == arr[k]
    {
        r[i] := arr[i];
        i := i + 1;
    }

    assert arr[..start] == r[..start];

    if len > 0 {
      r[start] := arr[start+len-1];

      assert r[start] == arr[start+len-1];

      i := start+1;
      while i < start+len
        invariant start < i <= start+len
        invariant arr[..start] == r[..start]
        invariant r[start] == arr[start+len-1]
        invariant forall k: nat :: start < k < i ==> r[k] == arr[k-1]
      {
          r[i] := arr[i-1];
          i := i + 1;
      }
    }

    assert rotated(arr[start .. start+len], r[start .. start+len]);

    i := start+len;
    while i < arr.Length
      invariant start+len <= i <= arr.Length
      invariant arr[..start] == r[..start]
      invariant rotated(arr[start .. start+len], r[start .. start+len])
      invariant forall k: nat :: start+len <= k < i ==> r[k] == arr[k]
    {
        r[i] := arr[i];
        i := i + 1;
    }
}

http://rise4fun.com/Dafny/aysI

Dafny: rotated region of an array method verification

1 Answers1