seq<int>
和的区别array<int>
。.Length
)序列是一个(n个不变的)数学列表。数组是分配给堆的(可变的,可能是别名的)数据结构。
考虑以下两种愚蠢的方法
method Seq()
{
var x := [1, 2, 3];
assert x[1] == 2;
var y := x;
assert y[1] == 2;
y := y[1 := 7];
assert y[1] == 7;
assert x[1] == 2;
}
method Array()
{
var x := new int[3](i => i + 1);
assert x[1] == 2;
var y := x;
assert y[1] == 2;
y[1] := 7;
assert y[1] == 7;
assert x[1] == 7;
}
第一种方法使用序列。由于序列是不可变的,因此y
将更新为新序列,索引1更新为具有值7。正如预期的那样,x
在操作时保持不变y
。
第二种方法使用数组。由于数组是堆分配的并且可以别名,因此当我们分配时y := x
,我们输入一个世界,其中x
和y
是堆中同一数组的两个不同名称。这意味着,如果我们修改via数组y
,我们将在read through中看到反映的结果x
。
为了回答您的第二个问题,Dafny级序列和数组不直接对应于同名的SMT级事物。Dafny的编码根本不使用SMT级别的序列或数组。相反,所有内容都通过未解释的函数进行编码。我认为这主要是出于历史原因,我不知道是否有人在戴夫尼语境下认真研究过SMT序列理论。我可以说,当前的编码已经针对求解器性能进行了精心调整。
本文收集自互联网,转载请注明来源。
如有侵权,请联系[email protected] 删除。
我来说两句