Chalice/tests/examples/list-reverse.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

class Node {
  var next : Node;
  var val : int;

  predicate list {
    acc(next) && acc(val) && (next!=null ==> next.list)
  }
  
  function vals() : seq<int>
    requires list
  {
    unfolding list in (next == null ? [val] : [val] ++ next.vals())
  }

  function reverse_vals() : seq<int>
    requires list
  {
    unfolding list in (next == null ? [val] : next.reverse_vals() ++ [val])
  }

  method reverse_in_place() returns (r:Node)
    requires list;
    ensures r != null && r.list;
    ensures r.vals() == old(this.reverse_vals());
  {
    var l : Node := this;
    r := null;

    while (l != null) 
      invariant l!=null ==> l.list;
      invariant r!=null ==> r.list;
      invariant old(this.reverse_vals()) == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
    { 
      var y: Node;
      unfold l.list;
    
      y := l.next;
      l.next := r;
      r := l;
      fold r.list;
      l := y;
    }
  }
}