Invariant失败，但在循环验证之前断言

Question

在下面的程序中，循环的最后一个不变量无法验证。但是，如果我把它作为断言放在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, 0).item, write)
// Error: insufficient permission to acces loc(diz.ia, 0).item
invariant alen(diz.ia) > 0 ==> (old(loc(diz.ia, 0).item) == old(loc(diz.ia, 0).item)) 
{ 

}
}

我的硅版本：

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

Answer 1

您观察到的行为是硅和碳之间的已知差异，这确实会令人困惑。

以下是硅中发生的事情：回路体本质上是孤立验证的，即模块化验证：不变量在空状态下被吸入，然后是回路保护；则验证身体。当吸入最后一个不变量时，假设其左侧alen(diz.ia) > 0(在一条路径上(，而右侧old(loc(diz.ia, 0).item) == old(loc(diz.ia, 0).item)(试图(被吸入。现在，回想一下，正在进行的验证是在一个新状态下孤立地进行的：因此，当前状态下的diz.ia可能不会引用与old状态中的diz.ia相同的对象。如果是，则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
}
}

Carbon更进一步，还将有关字段的知识框架到循环体中，对于周围验证范围(例如包含循环的方法体(保留一些权限的字段：

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中按原样进行验证，但不再验证。

一句话：毒蛇队应该决定；右"；语义，并确保两个验证器都遵守它。