dafny - 如何处理“验证不确定”错误

Question

我有一种方法会导致错误“验证不确定”。目前尚不清楚为什么验证是不确定的。似乎没有超时，也没有迹象表明哪些验证条件无法证明。简而言之：这是什么意思？

我使用的是 2.0.0 版。我不记得在 1.9.7 版本中看到此消息。

我遇到问题的特定方法是。

function c( n : int, r : int ) : int
    requires 0 <= r <= n
{
    if( r==0 ) then 1
    else if( r==n ) then 1
    else c(n-1, r-1) + c( n-1, r )
}

method combinations1Row( m : array2<int>, i : int )
    requires m != null
    requires m.Length0 == m.Length1 
    requires var N := m.Length0 ; 0 <= i < N ;
    requires forall n,r : int :: 0 <= r <= n < i ==> m[n,r] == c(n,r)
    modifies m
    ensures forall n,r : int :: 0 <= r <= n <= i ==> m[n,r] == c(n,r)
{
    var N := m.Length0 ;
    var j := 0 ;
    while( j <= i )
        invariant 0 <= j <= i+1
        invariant forall n,r : int :: 0 <= r <= n < i ==> m[n,r] == c(n,r)
        invariant forall r : int :: 0 <= r < j ==> m[i,r] == c(i,r)
    {
        if( j==0 ) { m[i,j] := 1 ; }
        else if( j==i ) { m[i,j] := 1 ; }
        else { m[i,j] := m[i-1,j-1] + m[i-1,j] ; }
        assert m[i,j] == c(i,j) ;
        assert forall r : int :: 0 <= r <= j ==> m[i,r] == c(i,r) ;
        j := j+1 ;
    }
    assert j==i+1 ;
}