Chalice/tests/predicates/test.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 List
{
  var value:int;
  var next:List;
  
  predicate inv { acc(value) && acc(next) && (next!=null ==> next.inv) }
  
  function len():int
    requires inv;
  {
    unfolding inv in (next==null) ? 1 : (1+next.len())
  }
  
  predicate P { acc(value,50) }
  
  method skip()
    requires P; ensures P
  {}
  
  method goo()
    requires acc(value);
  {
    // mask: value=100, secmask: -
    fold P;
    // mask: value=50,p=100, secmask: value=50
    call skip();
    // mask: value=50,p=100, secmask: -
    fold P;
    // mask: value=0,p=200, secmask: value=50
    fork t:=skip();
    // mask: value=0,p=100, secmask: -
    assert unfolding P in value==old(value);
  }

}