如何在后置条件引用前置通配符权限并声明方法保留该权限

你遇到的错误是因为Dafny的权限系统限制了perm操作符的使用场景——它不能直接在old()表达式中使用，必须放在inhale、exhale这类断言上下文或者ghost变量初始化里。要在后置条件中引用前置的通配符权限，正确的做法是用ghost变量提前捕获进入方法时的具体权限值，再在后置条件中引用这个变量的旧值。

修正后的代码如下：

field fd: Int

method foo(p: Ref) returns (res: Int)
    requires acc(p.fd, wildcard)
    ensures acc(p.fd, old(prevPerm))
    ghost var prevPerm: Perm := perm(p.fd)
{
    res := p.fd
}

代码说明： #

• ghost var prevPerm: Perm := perm(p.fd)：在方法执行前，用ghost变量捕获前置条件中通配符对应的具体权限值。Ghost变量不会影响程序运行，仅用于验证逻辑。
• 后置条件acc(p.fd, old(prevPerm))：通过old(prevPerm)引用进入方法时的初始权限，保证方法返回后，p.fd的权限和调用前完全一致。
• 这样既满足了前置条件对通配符权限的要求，也绕过了perm操作符的使用限制。

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