集合

Dafny的集合为有限集set，无限集iset，下面是它们的一些例子。

method m2(){
   var s1 := {1, 2, 3};
   var s2 := {1, 3, 6};
   assert s1 + s2 == {1, 2, 3, 6}; // set union
   assert s1 * s2 == {1, 3}; // set intersection
   assert s1 - s2 == {2}; // set difference

   assert s2 - {1} in (iset s3 : set<int> | forall x :: x in s3 ==> x % 3 == 0); // 集合的另一种形式
}

集合的并、交、差可以用+, *, -来表示

集合的另一种表现形式是set x: T | p(x) :: f(x),即该集合的元素x类型为T，满足p(x)，并应用f(x)。这里给出的例子中的集合含义是：该无限集的所有元素是整型集合，且对于任意的元素(称之为s3)都有：该整型集合中的元素能被3整除。由于s2 - {1}的结果为{3, 6}显然属于该集合，故该断言正确。