The use of arrays in a recursive function in Dafny leads to verification failure

Question

The following code, assert f(arr, 2) == 0;, fails to verify.

function f(bs:array<int>, hi:nat) : nat
{
  if hi==0 then 0 else f(bs, hi-1)
}

method Main() {
  var arr := new int[3][1, 1, 1];
  assert f(arr, 2) == 0;
}

Moreover, I found that:

• When I add a new hint assert f(arr, 0) == 0;, it can pass the verification.
• Or when I use a sequence (seq), it can also pass.

I really can't understand what the reason is.

Answer 1

Ordinarily, Dafny automatically unrolls a function once. That's enough to prove each of the first two assertions in your updated example. In most cases in verification, this is enough, because if you don't know the values of the parameters, the proofs are symbolic and usually done by induction in one form or another.

In the third assertion, function f needs to be unrolled 6 times in order to determine that the result value is 0. The verifier is not doing that automatically, so you have to help it along. For example, you could write the Main method as

method Main() {
  var arr := new int[5][1, 1, 1, 1, 1];
  assert f(arr, 0) == 0;
  assert forall i:: 0< i<=arr.Length ==> f(arr, i)==f(arr, i-1);
  calc {
    f(arr, arr.Length);
  ==  // by the definition of f
    f(arr, arr.Length - 1);
  ==
    f(arr, arr.Length - 2);
  ==
    f(arr, arr.Length - 3);
  ==
    f(arr, arr.Length - 4);
  ==
    f(arr, arr.Length - 5);
  ==
    0;
  }
  assert f(arr, arr.Length) == 0;
}

In general, this is what you'd need to do.

Advanced:

However, Dafny does actually help you out a little more. In some cases, it unrolls a function call twice, and in some cases, it can even continue unrolling the function until it stops. The latter happens when the parameters passed to the function are literals, or at least when the arguments that affect termination are literals. The arr.Length argument is known to equal the literal 5, but the argument arr is not a literal. So, for starters, Dafny would need to be told that termination of f depends only on the hi argument, not on bs. By default, Dafny gives you decreases bs, hi for f, but if you write decreases hi, then Dafny will know that termination depends only on hi. This may still not work automatically with the array argument, but it does work if you use a sequence instead of an array. (Sequences may be easier, because they are value types.) For example, the following program verifies automatically:

function f(bs: seq<int>, hi: nat): nat
  requires hi <= |bs|
  decreases hi
{
  if hi == 0 then 0 else f(bs, hi - 1)
}

method Main() {
  var arr := new int[5][1, 1, 1, 1, 1];
  assert f(arr[..], 0) == 0;
  assert forall i :: 0 < i <= arr.Length ==> f(arr[..], i) == f(arr[..], i - 1);
  assert f(arr[..], arr.Length) == 0;
}

(If you're interested in the details of how this works, see https://leino.science/papers/krml237.pdf.)

So, the verifier can be more automatic in some cases, but I would still suggest keeping "the verifier unrolls each function call just once" in mind as a rule of thumb.

Answer 2

According to Dafny's documentation:

The other situation that requires a termination proof is when methods or functions are recursive. Similarly to looping forever, these methods could potentially call themselves forever, never returning to their original caller. When Dafny is not able to guess the termination condition, an explicit decreases clause can be given along with pre- and postconditions, as in the unnecessary annotation for the fib function:

function fib(n: nat): nat
  decreases n
{
  if n == 0 then 0
  else if n == 1 then 1
  else fib(n - 1) + fib(n - 2)
}

As before, Dafny can guess this condition on its own, but sometimes the decreasing condition is hidden within a field of an object or somewhere else where Dafny cannot find it on its own, and it requires an explicit annotation.

So you can change your code to

function f(bs:array<int>, hi:nat) : nat
  decreases hi
{
  if hi==0 then 0 else f(bs, hi-1)
}

method Main() {
  var arr := new int[3][1, 1, 1];
  assert f(arr, 2) == 0;
}

for it to work.

Answer 3

function f(bs:array<int>, hi:nat) : nat
  decreases hi
  requires 0 <= hi <= bs.Length
  requires bs.Length > 1
  reads bs

{
  if hi==0 then 0 else f(bs, hi-1)
}

method Main() {
  var arr := new int[5][1, 1, 1, 1, 1];
  assert f(arr, 0) == 0;
  assert forall i:: 0< i<=arr.Length ==> f(arr, i)==f(arr, i-1);
  assert f(arr, arr.Length) == 0;
}

assert f(arr, arr.Length) == 0; the verification failed..

@enzo