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 endcurlybrace anyway).
There is no reason to require arr to be of non0 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 0length 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
