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

// fold/unfold in various combinations
class FUFU
{
  var value:int;
  var next:FUFU;
  
  predicate inv { acc(value) }
  
  predicate tinv { acc(value) && acc(next) && (next!=null ==> next.tinv) }
  
  function get():int
    requires tinv;
  { unfolding tinv in value }

  method fufu()
    requires acc(value);
  {
    fold inv;
    unfold inv;
    fold inv;
    unfold inv;
  }
  
  method fuf()
    requires acc(value);
  {
    fold inv;
    unfold inv;
    fold inv;
  }  
  
  method uf()
    requires inv;
  {
    unfold inv;
    fold inv;
  }
  
  method fu()
    requires acc(value);
  {
    fold inv;
    unfold inv;
  }
  
  method t()
    requires tinv && unfolding tinv in next!=null;
    ensures tinv && unfolding tinv in next!=null;
  {
    unfold tinv;
    unfold next.tinv;
    fold next.tinv;
    fold tinv;
  }
}