viper-lang - 双重权限吸入导致意外验证

Question

我无法理解 Viper 的某些行为，恕我直言，这似乎是一个错误。

由于缺少对bar.val_int分配的权限，以下代码无法验证。这完全有道理。

field val_int: Int
method foo() {
   var bar: Ref
   inhale acc(bar.val_int)
   exhale acc(bar.val_int)
   bar.val_int := 2
}

然而，以下代码验证成功：

field val_int: Int
method foo() {
   var bar: Ref
   inhale acc(bar.val_int)
   inhale acc(bar.val_int)
   exhale acc(bar.val_int)
   exhale acc(bar.val_int)
   bar.val_int := 2
}

事实上，可以添加任意数量的呼气，只要顶部有两个吸气（以获得完全权限），代码将始终验证。这是一个错误，故意的，还是我错过了正在发生的一些奇怪的事情？

我原以为第二次吸气没有效果，因为堆位置已经拥有完整的权限。但是，即使以某种方式双重写入权限是有帮助的（这应该是非法的？），那么至少我希望这两个exhale语句撤销这些权限，在分配时再次没有权限。

标签： viper-lang

Answer 1

对字段位置的写入/完全权限是排他性的，即 Viper 逻辑的隐式不变量是，给定单个 location x.f，总权限x.f最多为write/ 1。另请参阅Viper 教程，尤其是有关独占权限的本小节。

由于这个不变量，从你的第二个片段中吸入的顺序——和吸入基本上是“只是”许可感知假设

inhale acc(bar.val_int)
inhale acc(bar.val_int)

因此等价于

assume false

一旦假设为 false （如果您从操作上考虑，这意味着“此代码和后续代码不可访问”），之后遵循哪些 Viper 语句并不重要。特别是，没有任何呼气顺序会被认为是错误的。

在证明规则中思考

如果您更习惯于在演绎证明规则中思考，请考虑以下与命题逻辑中的矛盾相关的证明规则

   A ∧ ¬A                    A ∧ ¬A 
 ----------     or even:   ----------
   false                       B

它说false来自A ∧ ¬A，或者更确切地说，任何结论B都来自这样的矛盾。

基本上，Viper 的分离逻辑实例包括以下相关规则：

   acc(x.f, p)  acc(x.f, q)
 ------------------------------ if 1 < p + q
             false

该规则捕获了上述逻辑的不变量，即字段xf的权限不得超过完全/写入权限，即 1。

在您的情况下，两次吸气建立了必要的前提，因此 Viper 得出错误的结论。