viper-lang - 在毒蛇中乘以通配符有什么意义吗？

Question

VerCors 中的一个错误生成了一些银色，看起来像:

field f: Int

method test(n: Int, x: Ref)
requires n == 100
requires acc(x.f, wildcard * n)    
{}

Viper 似乎接受了这一点，但我不明白这意味着什么，如果有的话。

Answer 1

直观地说，这意味着被调用者获得了一个很小(但非零)的权限——乘以 n。实际上，这应该与仅仅获得少量(即 acc(x.f, wildcard) )没有什么不同，尽管人们可以设计人为的情况，可能涉及 perm ，其中有所不同。
底线:这个例子确实有点令人困惑，语义也不完全明显，但一切都很好定义。