量化权限和通配符的预期错误或不完整？

Question

考虑以下 Viper 程序：

field f: Int

method g(r: Ref, N: Int)
  requires forall tid: Int :: 0 <= tid && tid < N ==> acc(r.f, wildcard)
{
  // Got error: insufficient permission for r.f
  assert 0 < N ==> acc(r.f, wildcard)
}

method h(r: Ref, N: Int)
requires 0 < N ==> acc(r.f, wildcard);
{
  assert 0 < N ==> acc(r.f, wildcard)
  assert 0 < N ==> acc(r.f, wildcard) && acc(r.f, wildcard)
  // Got error: receiver of r.f might not be injective
  assert forall tid: Int :: 0 <= tid && tid < N ==> acc(r.f, wildcard)
}

直觉上，失败的断言应该成立。是否存在导致断言失败的通配符权限的微妙方面，或者这是一个完整性问题？

^{（最初以 an issue 的形式提交给 Viper 的后端之一，但由于解释可能有助于其他人避免类似的陷阱而复制到此处）}

Answer 1

失败有不同的根本原因，但两者都是意料之中的。

错误“接收者可能不是单射的”

出于技术原因（详见this paper），形状的量化权限断言

forall x :: c(x) ==> acc(e(x).f)

在 e(x) 中

必须是单射。 IE。对于 x 的两个不同实例，表达式 e(x) 计算为两个不同的接收者。你的断言并非如此

forall tid: Int :: 0 <= tid && tid < N ==> acc(r.f, wildcard)

因此出现错误消息。

如果您想知道为什么 method g 的先决条件没有得到相同的错误：由于先决条件是吸入的，Viper 假设（这可能在未来改变）它很好-定义，即接收器是内射的。如果你调用 g，那么你会得到同样的错误：

method caller(r: Ref, N: Int) {
  g(r, N) // receiver r.f might not be injective
}

所以g的当前前提基本上是假的（因为r在x中不是单射的）。如果您想知道为什么 Viper 不能（还）在前提条件之后立即证明错误，请继续阅读。

错误“权限不足”

忽略关于接收器注入性的不合理假设，那么这个错误是由于触发：量词

forall tid: Int :: 0 <= tid && tid < N ==> acc(r.f, wildcard)

不允许 Viper 为您选择任何触发器，因为有效触发器 (i) 不得包括解释函数（从 SMT 求解器的角度来看），但 (ii) 它们必须包括所有量化变量。在这里，这排除了子表达式，例如 0 <= tid（解释函数），但也排除了 r.f（未提及量化变量 tid）。基本上没有定义 SMT 求解器如何处理没有触发器的量词；在这里，它根本没有实例化。

在这种情况下你唯一真正的选择（除了信仰）是添加一个人为的触发器。这里有两个例子：

/* ------------- Example 1 ------------- */

domain dummy {
  function T(n: Int): Bool
  axiom T_always_true { forall n: Int :: T(n) }
}

method g1(r: Ref, N: Int)
  requires (forall tid: Int :: {T(tid)} 0 <= tid && tid < N ==> acc(r.f, wildcard))
{
    assert T(0) // Must mention T(_) somewhere to trigger quantifier
    assert 0 < N /* && T(0) */ ==> acc(r.f, wildcard)
}

/* ------------- Example 2 ------------- */

function id(r: Ref, n: Int): Ref { r }

method g2(r: Ref, N: Int)
  requires (forall tid: Int :: {id(r, tid)} 0 <= tid && tid < N ==> acc(id(r, tid).f, wildcard))
{
    assert 0 < N ==> acc(id(r, 0).f, wildcard)
}

顺便说一句，强烈建议始终明确添加触发器。一方面，因为它迫使人们思考触发器和触发策略（不同的公理如何相互作用以及何时应该实例化）。另一个原因是 Viper 采用尽力而为的方法来选择量词，但对于复杂的交互量词，您不应该依赖 Vipers 启发式方法。

如果您对触发器有更多疑问，请告诉我。 Viper tutorial 还有一个关于量词的部分，并引用了一篇关于触发器的好论文。

错误“接收器可能不是单射的”（续）

随着触发问题的解决，我们现在可以让 Viper 在 g:

的正文中证明错误

method g(r: Ref, N: Int)
  requires (forall tid: Int :: 0 <= tid && tid < N ==> acc(id(r, tid).f, wildcard))
{
  assume 2 < N
  assert id(r, 0) == id(r, 1)
  assert false // holds, because the malformed precondition is inhaled
}

量化权限和通配符的预期错误或不完整？

Expected error or incompleteness with quantified permissions and wildcards?

formal-verification

assertion

viper-lang

错误“接收者可能不是单射的”

错误“权限不足”

错误“接收器可能不是单射的”（续）