method to get subarray of array

May 29, 2014 at 11:58 PM
Edited May 30, 2014 at 12:00 AM
I have a method to get the sub-array of an array, but it does not verify. I can't figure it out. Any ideas?
method GetSubArray(arr: array<int>, startidx: int, finishidx: int) returns (newarr: array<int>)
  requires arr != null && arr.Length > 0;
  requires 0 <= startidx <= finishidx < arr.Length;
  ensures newarr != null && newarr.Length == (finishidx - startidx + 1);
  
  // Might not hold. Why???
  ensures forall j: int :: 0 <= j < newarr.Length ==> newarr[j] == arr[j+startidx];
{
  var len := finishidx - startidx + 1;
  assert len > 0;
  newarr := new int[len];
  var i:int := 0;
  var idx := startidx;
  assert 0 <= idx <= finishidx < arr.Length;
  
  while (idx <= finishidx && i < newarr.Length)
    invariant 0 <= idx <= arr.Length;
    invariant 0 <= i <= newarr.Length;
    decreases len - i;
  {
    if (i < newarr.Length && idx < arr.Length) {
      newarr[i] := arr[idx];
    }
    idx := idx + 1;
    i := i + 1;
  }
  
  // Postcondition might not hold on this path. Why???
  return newarr;
}
May 30, 2014 at 7:23 AM
Edited May 30, 2014 at 7:29 AM
Your loop invariant is not strong enough. I think that Dafny does not look inside the loop body when trying to verify the method post condition, so your loop invariant must be strong enough to prove the post condition when the loop exits.

Spoiler VVV
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
  while (idx <= finishidx && i < newarr.Length)
    invariant 0 <= idx <= arr.Length;
    invariant 0 <= i <= newarr.Length;
    invariant idx == startidx + i;
    invariant forall j: int :: 0 <= j < i ==> newarr[j] == arr[j + startidx];
    decreases len - i; 
Marked as answer by rustanleino on 6/10/2014 at 6:42 PM
Coordinator
Jun 11, 2014 at 2:09 AM
A few other remarks.

Your if test
if (i < newarr.Length && idx < arr.Length)
will always succeed. (If you want Dafny to confirm what I'm saying, add an assert of this condition in front of the if statement and see it pass.)

The two conjuncts in your while test
while (idx <= finishidx && i < newarr.Length)
are equivalent (which you can confirm by adding invariant idx <= finishidx <==> i < newarr.Length; to your loop invariant).

The last line of your method body:
  return newarr;
is not necessary. It is a shorthand for assigning the given expression (newarr) to the output parameter (also newarr) and then returning (which happens at the end-curly-brace anyway).

There is no reason to require arr to be of non-0 length or to disallow finishidx + 1 == startidx. If I would write it, I would use the start and finish pointers to say that every from (and including) start up to (but not including) finish is copied, which simplifies the various expressions you write (in particular, you can easily accommodate the 0-length cases and you don't need any +1 expressions.

Here is your program if you act on these changes:
method GetSubArray(arr: array<int>, start: int, finish: int) returns (newarr: array<int>)
  requires arr != null;
  requires 0 <= start <= finish <= arr.Length;
  ensures newarr != null && newarr.Length == finish - start;
  ensures forall j: int :: 0 <= j < newarr.Length ==> newarr[j] == arr[j + start];
{
  var len := finish - start;
  assert len >= 0;
  newarr := new int[len];
  var i, idx := 0, start;
  while i < newarr.Length
    invariant 0 <= i <= newarr.Length;
    invariant idx == start + i;
    invariant forall j: int :: 0 <= j < i ==> newarr[j] == arr[j + start];
    decreases len - i; 
  {
    newarr[i] := arr[idx];
    i, idx := i + 1, idx + 1;
  }
}
You may have written this program in order to learn more about loop invariants. But Dafny lets you implement this GetSubArray method without a loop (which means: no need for a loop invariant!), using the aggregate statement forall:
method GetSubArray(arr: array<int>, start: int, finish: int) returns (newarr: array<int>)
  requires arr != null;
  requires 0 <= start <= finish <= arr.Length;
  ensures newarr != null && newarr.Length == finish - start;
  ensures forall j: int :: 0 <= j < newarr.Length ==> newarr[j] == arr[j + start];
{
  newarr := new int[finish - start];
  forall j | 0 <= j < newarr.Length {
    newarr[j] := arr[j + start];
  }
}
Rustan