集合

笔记

各种类型的集合构成了Dafny验证的核心工具之一。集合表示元素的无序集合，集合中没有重复。与序列一样，集合也是不可变的值类型。这使得它们可以很容易地在注释中使用，而不涉及堆，因为set一旦创建就无法修改。集合的类型为:

  set<int>

例如，对于一组整数。通常，集合几乎可以是任何类型，包括对象。具体集合可以通过使用显示符号来指定:

method m()
{
   var s1 := {}; // the empty set
   var s2 := {1, 2, 3}; // set contains exactly 1, 2, and 3
   assert s2 == {1,1,2,3,3,3,3}; // same as before
   assert s1 != s2;  // sets with different elements are different
   var s3, s4 := {1,2}, {1,4};
}
   var s1 := {}; // the empty set
   var s2 := {1, 2, 3}; // set contains exactly 1, 2, and 3
   assert s2 == {1,1,2,3,3,3,3}; // same as before
   assert s1 != s2;  // sets with different elements are different
   var s3, s4 := {1,2}, {1,4};

例子演示中展示的set正是我们想要的：只包含指定元素。上面我们还看到为集合定义了相等符号，如果两个集合有完全相同的元素，那么它们就是相等的。也可以使用集合运算符从现有的集创建新的集:

method m()
{
   var s1 := {};
   var s2 := {1, 2, 3};
   var s3, s4 := {1,2}, {1,4};
   assert s2 + s4 == {1,2,3,4}; // set union
   assert s2 * s3 == {1,2} && s2 * s4 == {1}; // set intersection
   assert s2 - s3 == {3}; // set difference
}
   assert s2 + s4 == {1,2,3,4}; // set union
   assert s2 * s3 == {1,2} && s2 * s4 == {1}; // set intersection
   assert s2 - s3 == {3}; // set difference

注意，因为集合中的最多只有一个，不能重复。所以得到的并集不会将重复元素计数超过一次。如果两个集合都是有限的，那么通过这些操作符将得到一个有限集，不能生成一个无限集。与算术运算符不同，集合运算符都是有自己定义的。除了通常的集合操作符外，还有一些比较操作符，它们通常具有以下含义:

method m()
{
   assert {1} <= {1, 2} && {1, 2} <= {1, 2}; // subset
   assert {} < {1, 2} && !({1} < {1}); // strict, or proper, subset
   assert !({1, 2} <= {1, 4}) && !({1, 4} <= {1, 4}); // no relation
   assert {1, 2} == {1, 2} && {1, 3} != {1, 2}; // equality and non-equality
}
   assert {1} <= {1, 2} && {1, 2} <= {1, 2}; // subset
   assert {} < {1, 2} && !({1} < {1}); // strict, or proper, subset
   assert !({1, 2} <= {1, 4}) && !({1, 4} <= {1, 4}); // no relation
   assert {1, 2} == {1, 2} && {1, 3} != {1, 2}; // equality and non-equality

与序列一样，集合也支持in和!in操作符来测试元素的成员关系。例如:

method m()
{
   assert 5 in {1,3,4,5};
   assert 1 in {1,3,4,5};
   assert 2 !in {1,3,4,5};
   assert forall x :: x !in {};
}
   assert 5 in {1,3,4,5};
   assert 1 in {1,3,4,5};
   assert 2 !in {1,3,4,5};
   assert forall x :: x !in {};

集合用于一些注释，包括读取和修改子句。在本例中，它们可以是特定对象类型的集合(如链表中的nodes)，也可以是泛型引用类型对象object的集合。尽管它的名字是这样的，但它可以指向任何对象或数组。这对于将函数或方法可能读取或写入的所有不同类型的位置捆绑在一起非常有用。 在decreases子句中使用时，集合按真子集排序。要在decreases子句中使用set，连续的值在某种意义上必须是“相关的”，这通常意味着它们是递归计算的，或类似的。 您可以通过将一个集合与空集合进行比较来测试它是否为空(当且仅当s没有元素时，s =={}为真)。 创建集合的一个有用方法是使用set comprehension。通过将f(x)包含到所有满足p(x)的T类型的x的集合中，它定义了一个新集合:

   set x: T | p(x) :: f(x)

它以一种让人想起全称量词(forall)的方式来定义集合。与限定符一样，该类型通常可以推断出来。与量词相反，bar语法(|)需要将谓词(p)与绑定变量(x)分离。结果集合元素的类型是f(x)的返回值的类型。构造的集合的值是f(x)的返回值:x本身只充当谓词p和函数f之间的桥梁。它通常具有与结果集相同的类型，但它不是必须要相同。作为一个例子:

method m()
{
   assert (set x | x in {0,1,2} :: x + 0) == {0,1,2};
}
   assert (set x | x in {0,1,2} :: x + 0) == {0,1,2};

如果函数是恒等式，那么能以很优美的形式写出表达式

method m()
{
   assert (set x | x in {0,1,2,3,4,5} && x < 3) == {0,1,2};
}
   assert (set x | x in {0,1,2,3,4,5} && x < 3) == {0,1,2};

一般的集合推导中的非恒等函数容易混淆Dafny。例如，以下是正确的，但Dafny无法证明它:

method m()
{
   // assert {0*1, 1*1, 2*1} == {0,1,2};  // include this assertion as a lemma to prove the next line
   assert (set x | x in {0,1,2} :: x * 1) == {0,1,2};
}
assert (set x | x in {0,1,2} :: x * 1) == {0,1,2};

为了帮助Dafny证明这个断言，可以在它前面加上断言assert {0*1, 1*1, 2*1} == {0,1,2};这让Dafny解决了两个断言。

如果没注意，用集合set comprehension将集合规定为无限数量的元素，但集合只允许有有限数量的元素。例如，如果您尝试将set x | x % 2 == 0作为所有偶数的集合，那么您将得到一个错误。(如果你真的想要一个无限集，可以使用iset类型。例如，iset x | x % 2 == 0在ghost环境中是合法的。)为了确保集合推导得到有限集合，Dafny采用了一些启发式方法。创建整数集时，可以通过将整数限定在谓词的至少一个连接词中来完成(类似于0 <= x < n)来实现。要求限定变量在现有集合中也可以，如上面的x in {0,1,2}.