Chalice/tests/predicates/FoldUnfoldExperiments.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

class FoldUnfoldExperiments
{
  var x:int;
  var y:int;
  predicate X { acc(x) }
  predicate Y { acc(y) }
  
  function getX():int
    requires X;
  { unfolding X in x }
  
  function getY():int
    requires Y;
  { unfolding Y in y }
  
  method setX(v:int)
    requires X;
    ensures X && getX()==v;
  {
    unfold X; x:=v; fold X;
  }
  
  method check()
    requires acc(x) && acc(y);
    ensures acc(y) && y==2 && X && getX()==3;
  {
    x:=1; y:=2;
    fold X; fold Y;
    call setX(3);
    unfold Y;
  }
}