不变式失败，但在循环验证之前断言

问题描述

在下面的程序中，循环的最后一个不变式无法验证。但是，如果我将其作为while循环之前的断言，条件将得到验证。如果我添加字段ia不变，那么它也会验证。为什么需要这个？读取权限不应该暗含吗？我可以想象old与循环的循环前状态/状态破坏之间发生了怪异的相互作用，但这并没有向我解释为什么它会失败。可能是错误吗？

domain VCTArray[CT] {
  function loc(a: VCTArray[CT],i: Int): CT
  
  function alen(a: VCTArray[CT]): Int
}

//  a field 
field ia: VCTArray[Ref]

//  a field 
field item: Int

method negatefirst(diz: Ref)
requires diz != null
requires acc(diz.ia,1/2)
requires alen(diz.ia) > 0 ==> acc(loc(diz.ia,0).item,write)
{
  // Verifies just fine
  assert alen(diz.ia) > 0 ==> (old(loc(diz.ia,0).item) == old(loc(diz.ia,0).item))
  while (false)
    invariant acc(diz.ia,1/4) 
    // invariant diz.ia == old(diz.ia) // Adding this invariant allows the program to verify
    invariant alen(diz.ia) > 0 ==> acc(loc(diz.ia,write)
    // Error: insufficient permission to acces loc(diz.ia,0).item
    invariant alen(diz.ia) > 0 ==> (old(loc(diz.ia,0).item)) 
  { 
    
  }
}

我的芯片版本：

$ ./silicon.sh --help
Silicon 1.1-SNAPSHOT (d45da1d7+)

解决方法

您观察到的行为是硅和碳之间的known difference，确实令人困惑。

这是硅中发生的事情：循环体本质上是隔离验证的，即以模块方式进行验证：不变变量以空状态被吸入，然后是循环保护器；然后验证身体。吸入最后一个不变式时，假定其左侧alen(diz.ia) > 0（在一条路径上），而其右侧old(loc(diz.ia,0).item) == old(loc(diz.ia,0).item)被吸入（尝试）。现在，回想一下正在进行的验证是在一个新状态下单独进行的：因此，当前状态下的diz.ia可能与diz.ia状态下的old引用的对象不同。如果是这样，那么alen(diz.ia) > 0（当前状态）并不意味着old(alen(diz.ia) > 0)，因此字段old(loc(diz.ia,0).item)可能不可访问。因此，假设引用在这两个状态之间没有变化，即invariant diz.ia == old(diz.ia)，则使程序验证。

这是验证循环体的纯粹主义者的方式；在实践中，隔离并不是那么严格：两个验证者将关于局部变量的知识框架化为循环，因为（在语法上）未在循环体中分配给变量。这是一个示例：

method test() {
  var i: Int := 0
  var j: Int := 0
  
  while (true)
  {
    assert i == 0 // Verified
    assert j == 0 // Rejected
    j := j
  }
}

碳走得更远，并且还将关于字段的知识构建到循环主体中，对于这些字段，周围的验证范围（例如包含循环的方法主体）保留了某些权限：

field f: Int

method test(r: Ref,p: Perm) {
  inhale none < p
  inhale acc(r.f,p) && r.f == 0
  
  while (true)
    invariant acc(r.f,p/2) // Verified in Carbon,rejected by Silicon
  {
    assert r.f == 0
  }
}

如果您将不变式的权限更改为p（或在循环之前将exhale acc(r.f,p); inhale acc(r.f,p)破坏了字段的值），则上述内容将按Carbon的形式进行验证，但不再进行验证。

最重要的是：Viper团队应确定“正确”的语义，并确保两个验证者都遵守该语义。