不变集可能会有所不同 [英] Invariant set may vary
问题描述
一种将整数数组的负元素复制到另一个数组中的方法具有以下属性：结果中的元素集是原始数组中元素的子集，在复制过程中保持不变。
下面的代码中的问题是，一旦我们在结果数组中写入内容，Dafny就会以某种方式忘记原来的集合是不变的。
如何解决此问题？
方法copy_neg（a：array< int> ;, b：array< int>）
需要！= null&& b！=空&& a！= b
需要a.Length == b.Length
修改b
{
var i：= 0;
var r：= 0;
ghost var sa：= set j | 0< = j< a.Length :: a [j];
而我< a。长度
不变0 <== r <= i <= a。长度
不变sa ==设置j | 0< = j< a.Length :: a [j]
{如果a [i]< 0 {
assert sa == set j | 0< = j< a.Length :: a [j]; // OK
b [r]：= a [i];
assert sa == set j | 0< = j< a.Length :: a [j]; // KO！
r：= r + 1;
}
i：= i + 1;
}
}
编辑
按照 James Wilcox的答案，用序列谓词代替集合包含是最有效的方法。 p>
这里是完整的规范（适用于具有不同元素的数组）。后置条件必须在循环不变式中详细说明，并且愚蠢的断言保留在循环的中间，但是所有的虚变量都消失了，这很好。
方法copy_neg（a：array< int> ;, b：array< int>）
返回（r：nat）
需要！= null&& ; b！=空&& a！= b
需要a.Length< = b.Length
修改b
确保0< = r< = a.Length
确保forall x | x in a [..] :: x< 0< ==> x in b [.. r]
{
r：= 0;
var i：= 0;
而我< a。长度
不变0< = r< = i&=; a。长度
不变forall x | x in b [.. r] :: x< 0
全部不变x | x在[..i]&& x ＜ 0 :: x in b [.. r]
{
如果a [i]< 0 {
b [r]：= a [i];
断言forall x | x in b [.. r] :: x< 0;
r：= r + 1;
}
i：= i + 1;
}
}
此确实令人困惑。我将在下面说明为什么Dafny难以证明这一点，但首先让我给出一些方法来解决这个问题。
第一个解决方法
一种通过验证的方法是在 b [r]行之后插入以下。 forall 语句： a [i];
forall x | x in sa
确保x in set j | 0< = j< a.Length :: a [j]
{
var j：| 0< = j<长度&& x == old（a [j]）;
断言x == a [j];
}
forall 语句证明 sa< =设置j | 0< = j< a.Length :: a [j] 。我将回到为什么它在下面起作用的地方。
第二种解决方法
通常，在推理数组时Dafny，最好使用 a [..] 语法将数组转换为数学序列，然后使用该序列。如果确实需要使用元素的 set ，则可以使用 set x |。 x in a [..] ，与使用 set j |相比，您会有更好的时间。 0< = j< a.Length :: :: a [j] 。
系统地替换 set j | 0< = j< a.Length :: a [j] ，其中 set x | x in a [..] 使您的程序进行验证。
第三种解决方案
建立一个级别来指定您的方法，看来您实际上并不需要提及所有元素的集合。取而代之的是，您可以这样说： b 的每个元素都是 a 的元素。或者，更正式地将 forall x | x in b [..] :: x in a [..] 。这对于您的方法来说不是一个有效的后置条件，因为您的方法可能未填写所有 b 。由于我不确定您的其他约束条件是什么，因此我将留给您。
说明
将元素类型为 A 的达菲集转换为Boogie映射 [A] Bool ，其中元素映射为true如果它在集合中。诸如 set j的理解| 0< = j< a.Length :: a [j] 被翻译为Boogie映射，其定义涉及一个存在量词。这种特殊的理解转化为将 x 映射到
的地图j | 0< = j< a.Length :: x == read（$ Heap，a，IndexField（j））
其中 read 表达式是 a [j] 的Boogie转换，尤其是使堆显式。 / p>
因此，为了证明某个元素在由理解定义的集合中，Z3需要证明一个存在量词，这很难。 Z3使用 triggers 来证明此类量词，Dafny告诉Z3在尝试时使用触发器 read（$ Heap，a，IndexField（j））证明这个量词。事实证明这不是一个很好的触发器选择，因为它提到了堆的当前值。因此，当堆发生更改时（即，在更新 b [r] 之后），触发器可能不会触发，并且您得到的证明失败。
Dafny允许您使用 {：trigger} 属性来自定义用于集合理解的触发器。不幸的是，在达夫尼级别没有太多选择可以触发。但是，在Boogie / Z3级别上对该程序的合理触发将只是 IndexField（j）（尽管这通常对于此类表达式来说是一个糟糕的触发，因为它过于笼统）。如果Dafny不另行通知，则Z3本身将推断出该触发。您可以说出 {：autotriggers false} 来摆脱困境，就像这样
不变sa ==设置j {：autotriggers false} | 0< = j< a.Length :: a [j]
此解决方案不令人满意，并且需要详细了解Dafny的内部构造。但是，既然我们已经了解了它，我们还可以理解我提出的其他解决方法。
对于第一个解决方法，证明通过了，因为 forall 语句提到 a [j] ，这是触发器。这使Z3成功证明了存在性。
对于第二种解决方法，我们简化了集合理解表达式，使其不再引入存在性量词。相反，理解 set x |将[[..] 中的x转换为将 x 映射至
x in a ...
（忽略详细信息） a [..] 的翻译方式）。这意味着Z3永远不必证明存在性，因此可以通过其他类似的证明。
第三个解决方案的工作原理类似，因为它不使用任何理解，因此没有问题的存在量词/
A method that copies the negative elements of an array of integers into another array has the property that the set of elements in the result is a subset of the elements in the original array, which stays the same during the copy.
The problem in the code below is that, as soon as we write something in the result array, Dafny somehow forgets that the original set is unchanged. How to fix this?
method copy_neg (a: array<int>, b: array<int>)
requires a != null && b != null && a != b
requires a.Length == b.Length
modifies b
{
var i := 0;
var r := 0;
ghost var sa := set j | 0 <= j < a.Length :: a[j];
while i < a.Length
invariant 0 <= r <= i <= a.Length
invariant sa == set j | 0 <= j < a.Length :: a[j]
{
if a[i] < 0 {
assert sa == set j | 0 <= j < a.Length :: a[j]; // OK
b[r] := a[i];
assert sa == set j | 0 <= j < a.Length :: a[j]; // KO!
r := r + 1;
}
i := i + 1;
}
}
Edit
Following James Wilcox's answer, replacing inclusions of sets with predicates on sequences is what works the best.
Here is the complete specification (for an array with distinct elements). The post-condition has to be detailed a bit in the loop invariant and a dumb assert remains in the middle of the loop, but all ghost variables are gone, which is great.
method copy_neg (a: array<int>, b: array<int>)
returns (r: nat)
requires a != null && b != null && a != b
requires a.Length <= b.Length
modifies b
ensures 0 <= r <= a.Length
ensures forall x | x in a[..] :: x < 0 <==> x in b[..r]
{
r := 0;
var i := 0;
while i < a.Length
invariant 0 <= r <= i <= a.Length
invariant forall x | x in b[..r] :: x < 0
invariant forall x | x in a[..i] && x < 0 :: x in b[..r]
{
if a[i] < 0 {
b[r] := a[i];
assert forall x | x in b[..r] :: x < 0;
r := r + 1;
}
i := i + 1;
}
}
This is indeed confusing. I will explain why Dafny has trouble proving this below, but first let me give a few ways to make it go through.
First workaround
One way to make the proof go through is to insert the following forall statement after the line b[r] := a[i];.
forall x | x in sa
ensures x in set j | 0 <= j < a.Length :: a[j]
{
var j :| 0 <= j < a.Length && x == old(a[j]);
assert x == a[j];
}
The forall statement is a proof that sa <= set j | 0 <= j < a.Length :: a[j]. I will come back to why this works below.
Second workaround
In general, when reasoning about arrays in Dafny, it is best to use the a[..] syntax to convert the array to a mathematical sequence, and then work with that sequence. If you really need to work with the set of elements, you can use set x | x in a[..], and you will have a better time than if you use set j | 0 <= j < a.Length :: a[j].
Systematically replacing set j | 0 <= j < a.Length :: a[j] with set x | x in a[..] causes your program to verify.
Third solution
Popping up a level to specifying your method, it seems like you don't actually need to mention the set of all elements. Instead, you can get away with saying something like "every element of b is an element of a". Or, more formally forall x | x in b[..] :: x in a[..]. This is not quite a valid postcondition for your method, because your method may not fill out all of b. Since I'm not sure what your other constraints are, I'll leave that to you.
Explanations
Dafny's sets with elements of type A are translated to Boogie maps [A]Bool, where an element maps to true iff it is in the set. Comprehensions such as set j | 0 <= j < a.Length :: a[j] are translated to Boogie maps whose definition involves an existential quantifier. This particular comprehension translates to a map that maps x to
exists j | 0 <= j < a.Length :: x == read($Heap, a, IndexField(j))
where the read expression is the Boogie translation of a[j], which, in particular, makes the heap explicit.
So, to prove that an element is in the set defined by the comprehension, Z3 needs to prove an existential quantifier, which is hard. Z3 uses triggers to prove such quantifiers, and Dafny tells Z3 to use the trigger read($Heap, a, IndexField(j)) when trying to prove this quantifier. This turns out to not be a great trigger choice, because it mentions the current value of the heap. Thus, when the heap changes (ie, after updating b[r]), the trigger may not fire, and you get a failing proof.
Dafny lets you customize the trigger it uses for set comprehensions using a {:trigger} attribute. Unfortunately, there is no great choice of trigger at the Dafny level. However, a reasonable trigger for this program at the Boogie/Z3 level would be just IndexField(j) (though this is likely a bad trigger for such expressions in general, since it is overly general). Z3 itself will infer this trigger if Dafny doesn't tell it otherwise. You can Dafny to get out of the way by saying {:autotriggers false}, like this
invariant sa == set j {:autotriggers false} | 0 <= j < a.Length :: a[j]
This solution is unsatisfying and requires detailed knowledge of Dafny's internals. But now that we've understood it, we can also understand the other workarounds I proposed.
For the first workaround, the proof goes through because the forall statement mentions a[j], which is the trigger. This causes Z3 to successfully prove the existential.
For the second workaround, we have simplified the set comprehension expression so that it no longer introduces an existential quantifier. Instead the comprehension set x | x in a[..], is translated to a map that maps x to
x in a[..]
(ignoring details of how a[..] is translated). This means that Z3 never has to prove an existential, so the otherwise very similar proof goes through.
The third solution works for similar reasons, since it uses no comprehensions and thus no problematic existential quantifiers/
这篇关于不变集可能会有所不同的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
