双态谓词无法证明参数已分配

Question

在分配了布尔数组后的循环内部，不变式

allocated(sieve)

报告 true，但是在赋值后尝试在筛数组上断言 Preserved 谓词会断言以下错误。为什么会报告此错误以及如何解决它？

    twostate predicate Preserved(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])
    }

无法证明参数 'sieve' 的索引 0 处的参数在二态函数的先前状态中分配 - 如果在参数声明前添加 'new'，如 'new sieve: array'，则参数可以引用表达式可能在前一个状态中未分配

Answer 1

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

应该可以。