Dafny: added set comprehension expressions

1 files changed, 40 insertions, 0 deletions

diff --git a/Test/dafny0/Comprehensions.dfy b/Test/dafny0/Comprehensions.dfy
new file mode 100644
index 00000000..8629a418
--- /dev/null
+++ b/Test/dafny0/Comprehensions.dfy
@@ -0,0 +1,40 @@
+method M()

+{

+  var numbers := set i | 0 <= i && i < 100;

+  var squares := set i | 0 <= i && i < 100 :: Id(i)*i;  // verifying properties about set comprehensions with a term expression is hard

+

+  assert 12 in numbers;

+  assert Id(5) == 5;

+  assert 25 in squares;

+  assert 200 in numbers;  // error

+}

+

+function method Id(x: int): int { x }  // for triggering

+

+// The following mainly test that set comprehensions can be compiled, but one would

+// have to run the resulting program to check that the compiler is doing the right thing.

+method Main()

+{

+  var q := set i,j | 0 <= i && i < 10 && 0 <= j && j < 3 :: i+j;

+  call PrintSet(q);

+  q := set b: bool | true :: if b then 3 else 7;

+  call PrintSet(q);

+  var m := set k | k in q :: 2*k;

+  call PrintSet(m);

+  call PrintSet(set k | k in q && k % 2 == 0);

+  var sq := [30, 40, 20];

+  call PrintSet(set k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i);

+  var bb := forall k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i == 17;

+}

+

+method PrintSet<T>(s: set<T>) {

+  var q := s;

+  while (q != {})

+    decreases q;

+  {

+    var x := choose q;

+    print x, " ";

+    q := q - {x};

+  }

+  print "\n";

+}