seq<int> 和 array<int> 之间的 Dafny 区别

Question

• 我似乎无法区分 dafny 的 seq<int> 和 array<int>。
• 它们是否对应于它们的 SMT 实体？ （不确定，因为 dafny 中的数组有 .Length）

Answer 1

序列是（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 被更新为 new 序列，索引 1 更新为值为 7。正如预期的那样，x 在y 的整个操作过程中保持不变。

第二种方法使用数组。由于数组是堆分配的并且可以别名，当我们分配y := x 时，我们进入一个世界，其中x 和y 是堆中同一数组的两个不同名称。这意味着如果我们通过y 修改数组，我们将看到通过x 读取的结果。

回答你的第二个问题，Dafny 级别的序列和数组并不直接对应 SMT 级别的同名事物。 Dafny 的编码根本不使用 SMT 级别的序列或数组。相反，一切都是通过未解释的函数编码的。我认为这主要是出于历史原因，我不知道是否有人在 Dafny 的背景下认真研究过序列的 SMT 理论。我可以说当前的编码已经针对求解器性能进行了非常仔细的调整。