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

class List0 {
  var rep: seq<int>;
  
  method init()
    requires acc(rep);
    ensures acc(rep);    
  {
    rep := [0];
  }

  method get(i) returns (v)
    requires acc(rep);
    requires 0 <= i && i < |rep|;
    ensures acc(rep);
  {
    v := rep[i];
  }
}

class List1 refines List0 {
  var sub: seq<List1>;
  var data: int;
    
  replaces rep by acc(sub) && acc(data) && acc(sub[*].sub) && acc(sub[*].data) &&
    /** valid */ |sub| >= 0 &&
    (forall i in [0..|sub|] :: sub[i] != null && sub[i].sub == sub[i+1..]) &&
    /** coupling */ |sub| + 1 == |rep| &&
    (forall i in [0..|sub|] :: sub[i].data == rep[i+1]) &&
    data == rep[0]
    
  refines init()
  {
    data := 0;
    sub := nil<List1>;
  }

  refines get(i) returns (v)    
  {
    if (i == 0) {
      v := data;
    } else {
      var next:List1 := sub[0];
      call v := next.get(i-1);
      //v := sub[i-1].data;
    }
  }
}