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

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.

>Solution :

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.