Chalice/tests/general-tests/quantifiers.chalice


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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59

class A {
  var f: int;
}

class Quantifiers {  
  var bamboo: seq<A>;

  method test1(a: seq<int>, b: int) 
    requires b in a;
    requires b > 0;
  {
    assert exists j in a :: true && j > 0;
    assert exists j:int :: 0 <= j && j < |a| && a[j] > 0;
    assert forall j in a :: exists k in a :: k > 0;
  }

  method test2(a: seq<A>)
    requires rd(a[*].*);
    requires |a| > 0;
    requires forall i in a :: i != null && i.f > 0;
  {
    assert a[0].f > 0;
    assert forall j: A :: j in a && j != null ==> j.f > 0;
    assert exists j: A :: j in a && j != null && j.f > 0;
  }

  method test3(a: seq<A>)
    requires |a| > 0;
    requires acc(a[*].f);
  {
    var c := new A;
    assert c != a[0];
  }
}

class Functions {
  var x: int;
  var y: int;

  function test1(): int
    requires acc(this.*);
  {
    x + y
  }

  function test2(): int
    requires acc(x) && acc(y);
  { 
    x + y
  }

  function test3(a: seq<A>): int
    requires acc(a[*].f);
    requires forall x in a :: x != null;
    requires forall i,j in [0..|a|] :: i != j ==> a[i] != a[j];
  {
    |a| == 0 ? 0 : a[0].f + test3(a[1..])
  }
}