I am trying to create a method in Dafny that lets me enter the contents of one array into another. For instance, given Array1= [1,2,3], Array2 = [6,7,8,9,0], and index = 1, the output array would be [1,6,7,8,9,0,2,3] as the method inserts the contents of Array2 to Array1 given an insertion index.
The code is listed below:
method insertArrayIntoIndex(a: array<int>, index: int, add_these: array<int>) returns (result: array<int>)
requires 0 <= index < a.Length;
ensures result.Length == a.Length + add_these.Length;
ensures forall i :: 0 <= i < index ==> a[i] == result[i];
ensures forall i :: 0 <= i < add_these.Length ==> add_these[i] == result[i + index];
ensures forall i :: index <= i < a.Length ==> a[i] == result[i + add_these.Length];
{
result := new int[a.Length + add_these.Length];
// copy first part in
var pos := 0;
while (pos < index)
invariant 0 <= pos <= index
invariant 1 <= pos < index ==> result[pos-1] == a[pos-1]
{
result[pos] := a[pos];
pos := pos + 1;
}
// copy in the addition
pos := 0;
while (pos < add_these.Length)
invariant 0 <= pos <= add_these.Length
invariant 1 <= pos < add_these.Length ==> result[index + pos-1] == add_these[pos-1]
{
result[index + pos] := add_these[pos];
pos := pos + 1;
}
// copy the last part in
pos := index;
while (pos < a.Length)
invariant index <= pos <= a.Length
invariant index < pos < a.Length ==> result[pos-1 + add_these.Length] == a[pos-1]
{
result[pos + add_these.Length] := a[pos];
pos := pos + 1;
}
}
I'm having trouble writing the proper loop invariants to get the code working. I've tried adding assertions at the end of each section to prove each part is working as shown below but I'm not sure why they are failing. Any help would be greatly appreciated. I've also added additional assertions inside the first section but they all seem to pass which confuses me on why the assertions outside fail.
method insertArrayIntoIndex(a: array<int>, index: int, add_these: array<int>) returns (result: array<int>)
requires 0 <= index < a.Length;
ensures result.Length == a.Length + add_these.Length;
ensures forall i :: 0 <= i < index ==> a[i] == result[i];
ensures forall i :: 0 <= i < add_these.Length ==> add_these[i] == result[i + index];
ensures forall i :: index <= i < a.Length ==> a[i] == result[i + add_these.Length];
{
result := new int[a.Length + add_these.Length];
// copy first part in
var pos := 0;
while (pos < index)
invariant 0 <= pos <= index
invariant 1 <= pos < index ==> result[pos-1] == a[pos-1]
{
result[pos] := a[pos];
assert result[pos] == a[pos];
assert pos >1 ==> result[pos-1] == a[pos-1];
assert forall i :: 0 <= i < pos ==> result[i] == a[i];
pos := pos + 1;
}
assert forall i :: 0 <= i < index ==> a[i] == result[i];
// copy in the addition
pos := 0;
while (pos < add_these.Length)
invariant 0 <= pos <= add_these.Length
invariant 1 <= pos < add_these.Length ==> result[index + pos-1] == add_these[pos-1]
{
result[index + pos] := add_these[pos];
pos := pos + 1;
}
assert forall i :: 0 <= i < add_these.Length ==> result[index + i] == add_these[i];
// copy the last part in
pos := index;
while (pos < a.Length)
invariant index <= pos <= a.Length
invariant index < pos < a.Length ==> result[pos-1 + add_these.Length] == a[pos-1]
{
result[pos + add_these.Length] := a[pos];
pos := pos + 1;
}
assert forall i :: index <= i < a.Length ==> result[add_these.Length + i] == a[i];
}
Dafny uses loop invariant to reason about loops. Let's understand what this entails.
Let's say you have written following loop
idx := 0;
while idx < a.Length
invariant 0 <= idx <= a.Length
{
a[idx] := 1;
idx := idx + 1;
}
After loop, facts that are available to dafny to reason about rest of
program is 0 <= idx <= a.Length && idx >= a.Length (second part is
loop termination condition). Inside loop, you can add assert a[idx] == 1
after assignment and it will verify. But
assert forall m :: 0 <= m < a.Length ==> a[m] == 1
after loop will n't verify as there is no invariant to prove this fact.
Let's say we want to prove that all elements of array is equal to 1 and we write following program
idx := 0;
while idx < a.Length
invariant 0 <= idx <= a.Length
invariant 1 <= idx <= a.Length ==> a[idx-1] == 1
{
a[idx] := 1;
idx := idx + 1;
}
Facts that is available to dafny after loop is
0 <= idx <= a.Length && 1 <= idx <= a.Length ==> a[idx-1] == 1 && idx >= a.Length.
Using above, it is not possible to arrive that
assert forall m :: 0 <= m < a.Length ==> a[m] == 1 . In fact it is possible only
to prove last element is equal to 1.
We need to ask dafny to remember using forall.
idx := 0;
while idx < a.Length
invariant 0 <= idx <= a.Length
invariant forall m :: 0 <= m < idx ==> a[m] == 1
{
a[idx] := 1;
idx := idx + 1;
}
After loop, fact that are available to dafny is
forall m :: 0 <= m < idx ==> a[m] == 1 && idx >= a.Length && 0 <= idx <= a.Length.
Now it is possible to prove forall m :: 0 <= m < a.Length ==> a[m] == 1
Taking care of these, this is how you can verify your insert function
method insert(a: array<int>, idx: int, b: array<int>)
returns (r: array<int>)
requires 0 <= idx < a.Length
ensures r.Length == a.Length + b.Length
ensures forall m :: 0 <= m < idx ==> r[m] == a[m]
ensures forall m :: 0 <= m < b.Length ==> r[idx + m] == b[m]
ensures forall m :: idx <= m < a.Length ==> r[b.Length + m] == a[m]
{
var i := 0;
r := new int[a.Length + b.Length];
while i < idx
invariant 0 <= i <= idx
invariant forall m :: 0 <= m < i ==> r[m] == a[m]
{
r[i] := a[i];
i := i + 1;
}
if b.Length != 0 {
i := 0;
while i < b.Length
invariant 0 <= i <= b.Length
invariant forall m :: 0 <= m < i ==> r[idx + m] == b[m]
invariant forall m :: 0 <= m < idx ==> r[m] == a[m]
{
r[idx + i] := b[i];
i := i + 1;
}
}
i := idx;
while i < a.Length
invariant idx <= i <= a.Length
invariant forall m :: 0 <= m < idx ==> r[m] == a[m]
invariant forall m :: 0 <= m < b.Length ==> r[idx + m] == b[m]
invariant forall m :: idx <= m < i ==> r[b.Length + m] == a[m]
{
r[b.Length + i] := a[i];
i := i + 1;
}
return;
}