如何在后置条件中引用前置条件中的通配符权限

【问题标题】：How to refer in postcondition to a wildcard permission in precondition如何在后置条件中引用前置条件中的通配符权限
【发布时间】：2023-01-28 00:27:00
【问题描述】：

如何声明需要通配符权限的方法并返回完全相同的权限。

我想写这样的东西：

field fd:Int

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

但后来我得到一个错误。

Consistency error: Perm and forperm in this context are only allowed if nested under inhale-exhale assertions.

【问题讨论】：

标签： formal-verification viper-lang

【解决方案1】：

方法前置条件和后置条件不得包含 perm()-表达式，因为这些表达式的值在方法调用者评估时会有所不同：如果调用者具有完全权限，则 old(perm(p.fd)) 将评估为完全许可对于来电者即使它只会评估被叫方的通配符数量。

要传递通配符权限数量并获得相同数量的返回值，您可以为该方法提供一个额外的 perm 类型参数，然后让调用者选择一个任意小的权限数量：

field fd:Int

method foo(p:Ref, prm: Perm) returns (res:Int)
    requires prm > none
    requires acc(p.fd, prm)
    ensures acc(p.fd, prm)
    {
      res := p.fd
    }

method caller()
{
    var r: Ref
    r := new(fd)
    var res: Int
    res := foo(r, 1/10)
}

【讨论】：