问题描述
以下程序无法验证：
field f: Int
method m(g: Ref,i: Int)
requires acc(g.f,i * wildcard)
{
assert acc(g.f,i * wildcard)
}
我第一次偶然发现 i 是一个更复杂的表达式（特别是一个抽象函数）。当你把 i 变成一个常数时，它会验证。 Carbon 报告了 https://github.com/viperproject/carbon/issues/376 中报告的错误。我之前可能已经报告过此错误的根本原因，但我不确定，所以我想我会提出问题。这是一个错误，还是（预期的）不完整？
将“i > 0”添加为requires子句会导致示例验证，我不太明白。如果我需要大于 0，我会期望一个格式良好的错误，或者没有“i > 0”子句的通过......？
解决方法
有趣的例子！观察到的行为可能令人惊讶，但可以解释。在我们详细介绍之前，先了解一下背景：当吸入可访问性谓词 acc(R,P) 时，对于某些资源 R 和权限表达式 p，假设 none ≤ p。包含 none 是因为对 R 的许可可能是有条件的，例如requires p == (b ? write : none)。
在您的示例中，这会产生 none ≤ i * k1，其中 k1 表示第一个通配符。对于后者，假设为 none < k1 < write。观察到 i == 0 是可能的，在这种情况下 i * k1 将是 none。
对于 assert，引入了第二个通配符 k2。在可以假设 k2 是“小于当前持有的任何读取分数”之前，即在可以假设 none < k2 < perm(g.f) 之前，必须检查 none < perm(g.f)。但是，这失败了：如果 perm(g.f)，none 为 i == 0。