Chalice/tests/refinements/SpecStmt.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

class Test {
  var x: int;
  method m(a:int) returns (b:int) 
  {
    var c := 0;
    ghost const d,c [d == c];
    var b [b == 0];  
    var e [e == a];   
    assert d == c;
    assert e == a;
    assert b == 0;
    assert c == 0; // error 
  }

  method n() 
    requires acc(x);
  {
    x := 0;
    const y [acc(x), acc(x) && x == old(x) + 1 && y == x];
    assert y == 1;
    const v [acc(x), acc(x) && v == old(x) + 1];
    assert v == 2;
    const z [z == 1];
    ghost var t [z == 1, true];     
    assert false; // reachable 
  }

  method o()  
  {
    var z [acc(x) && z == 0]; // unimplementable
    x := z;
    assert x == 0;
    assert false; // reachable
  }
}