序列

序列是一种表示有序列表的内置Dafny类型。它们可以用来表示许多有序集合，包括列表、队列、堆栈等。序列是一种不可变的值类型:它们一旦创建就不能被修改。从这个意义上说，它们类似于Java和Python等语言中的字符串，只是它们可以是任意类型的序列，而不仅仅是字符。序列类型如下:

   seq<int>

例如，对于一个整数序列。例如，这个函数将一个序列作为参数:

predicate sorted(s: seq<int>)
{
   forall i,j :: 0 <= i < j < |s| ==> s[i] <= s[j]
}

序列的长度写成|s|，如上量词所示。使用与数组相同的方括号语法访问序列的特定元素。还请注意，该函数不需要读取子句来访问序列。这是因为序列不是存储在堆上的;它们是值，因此函数在访问它们时不需要声明。序列最强大的属性是注释和函数可以创建和操作序列。例如，另一种表示排序性的方法是递归:如果第一个元素比其他元素小，而其余元素都已排序，则整个数组都已排序:

predicate sorted2(s: seq<int>)
{
   0 < |s| ==> (forall i :: 0 < i < |s| ==> s[0] <= s[i]) &&
               sorted2(s[1..])
}

年代的符号(1 . .是将序列切片。它的意思是从第一个元素开始，取元素直到最后。这不会修改s，因为序列是不可变的。相反，它创建了一个新的序列，除了第一个元素之外，所有元素都按相同的顺序排列。这类似于整数的加法，因为原始值没有改变，只是创建了新的值。切片表示法是:

   s[i..j]

在0 <= i <= j <= |s|这个范围中Dafny将强制执行这些索引边界。结果序列将恰好有j-i元素，并且将从元素s[i]开始，如果结果非空，则将连续地遍历序列。这意味着索引j处的元素被排除在切片之外，这反映了用于常规索引的相同的半开区间。

序列也可以使用显示表示法从其元素构造:

 var s := [1, 2, 3];

在这里，我们在一些命令式代码中有一个整数序列变量，其中包含元素1、2和3。这里使用了类型推断来获得序列是整数之一的事实。这种表示法允许我们构造空序列和单例序列:

[] // the empty sequence, which can be a sequence of any type
   [true] // a singleton sequence of type seq<bool>

切片表示法和显示表示法可以用来检查序列的属性:

method m()
{
   var s := [1, 2, 3, 4, 5];
   assert s[|s|-1] == 5; //access the last element
   assert s[|s|-1..|s|] == [5]; //slice just the last element, as a singleton
   assert s[1..] == [2, 3, 4, 5]; // everything but the first
   assert s[..|s|-1] == [1, 2, 3, 4]; // everything but the last
   assert s == s[0..] == s[..|s|] == s[0..|s|]; // the whole sequence
}
   var s := [1, 2, 3, 4, 5];
   assert s[|s|-1] == 5; //access the last element
   assert s[|s|-1..|s|] == [5]; //slice just the last element, as a singleton
   assert s[1..] == [2, 3, 4, 5]; // everything but the first
   assert s[..|s|-1] == [1, 2, 3, 4]; // everything but the last
   assert s == s[0..] == s[..|s|] == s[0..|s|] == s[..]; // the whole sequence

到目前为止，对序列最常见的操作是获取第一个和最后一个元素，以及获取除第一个和最后一个元素以外的所有元素，因为这些通常用于递归函数，如上面的sorted2。除了通过访问或切片来解构序列外，序列还可以使用加号(+)进行连接: 但是Z3定理证明者不会意识到这一点，除非它被一个声明事实的断言提示(关于为什么这是必要的更多信息，请参阅引理/归纳法)。 序列还支持in和!in操作符，用于测试序列中的包含情况:

method m()
{
   var s := [1, 2, 3, 4, 5];
   assert 5 in s;
   assert 0 !in s;
}
   assert 5 in s; // using s from before
   assert 0 !in s;

这还允许我们在不关心索引的情况下，对序列中的元素进行量化。例如，我们可以要求一个序列只包含该序列的下标元素:

method m()
{
   var p := [2,3,1,0];
   assert forall i :: i in p ==> 0 <= i < |s|;
}
   var p := [2,3,1,0];
   assert forall i :: i in p ==> 0 <= i < |s|;

这是序列中每个单独元素的属性。如果我们想让多个元素相互关联，就需要量化指标，如第一个例子所示。

有时我们想使用序列来模拟数组的可更新特性。虽然我们不能改变原来的序列，但我们可以创建一个新序列，其中除了更新的元素外，所有元素都是相同的:

method m()
{
   var s := [1,2,3,4];
   assert s[2 := 6] == [1,2,6,4];
}
   s[i := v] // replace index i by v in seq s

当然，下标i必须是数组的下标。这个语法只是可以通过常规切片和访问操作完成的操作的快捷方式。你能填写下面的代码吗?

function update(s: seq<int>, i: int, v: int): seq<int>
   requires 0 <= index < |s|
   ensures update(s, i, v) == s[i := v]
{
   s[..i] + [v] + s[i+1..]
   // This works by concatenating everything that doesn't
   // change with the singleton of the new value.
}
function update(s: seq<int>, i: int, v: int): seq<int>
   requires 0 <= index < |s|
   ensures update(s, i, v) == s[i := v]
{
   // open in the editor to see the answer.
}

你也可以用数组的元素组成一个序列。这是使用与上面相同的“slice”表示法完成的:

method m()
{
   var a := new int[3]; // 3 element array of ints
   a[0], a[1], a[2] := 0, 3, -1;
   var s := a[..];
   assert s == [0, 3, -1];
}
 var a := new int[3]; // 3 element array of ints
   a[0], a[1], a[2] := 0, 3, -1;
   var s := a[..];
   assert s == [0, 3, -1];

为了获得数组的一部分，可以像常规切片操作一样给出边界:

method m()
{
   var a := new int[3]; // 3 element array of ints
   a[0], a[1], a[2] := 0, 3, -1;
   assert a[1..] == [3, -1];
   assert a[..1] == [0];
   assert a[1..2] == [3];
}
   assert a[1..] == [3, -1];
   assert a[..1] == [0];
   assert a[1..2] == [3];

因为序列支持in和!in，这个操作为我们提供了一种简单的方法来表示“element not in array”属性，即将这个转变为

forall k :: 0 <= k < a.Length ==> elem != a[k]

这个：

elem !in a[..]

此外，边界很容易包括:

forall k :: 0 <= k < i ==> elem != a[k]

和以下这个是一样的：

elem !in a[..i]