双态谓词Preserved参数分配证明失败的原因与解决方法

错误原因 #

双态谓词的参数默认需要满足前后两个状态都处于已分配状态。你在循环里虽然能保证当前状态的sieve已分配，但Dafny没办法自动确认修改前的旧状态中sieve同样已分配——毕竟你刚对sieve做了赋值操作，Dafny需要明确的声明来允许参数引用旧状态中可能未分配的表达式。

解决办法 #

按照错误提示的指引，在双态谓词的sieve参数前加上new关键字即可，修改后的代码如下：

twostate predicate Preserved(new sieve: array<bool>, i: nat) 
    requires 2 <= i < sieve.Length
    reads sieve
{
    i*i < sieve.Length && multiset(old(sieve[..i*i])) == multiset(sieve[..i*i])
}

添加new后，Dafny会放宽对旧状态中sieve的分配校验要求，允许它引用旧状态里可能未分配的表达式，这样就能通过证明了。

内容的提问来源于stack exchange，提问作者Hath995