Test/dafny0/Comprehensions.dfy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43

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

datatype D = A | B;
// 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;
  PrintSet(q);
  q := set b: bool | true :: if b then 3 else 7;
  var d := set b:D | true;
  var test := forall d:D :: d == A || d == B;
  PrintSet(q);
  var m := set k | k in q :: 2*k;
  PrintSet(m);
  PrintSet(set k | k in q && k % 2 == 0);
  var sq := [30, 40, 20];
  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";
}