summaryrefslogtreecommitdiff
path: root/Test/dafny0/ListContents.dfy
blob: 01d8b63bb080b6cd85baff48fbc9f3e8e5b29932 (plain)
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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
class Node<T> {
  var list: seq<T>;
  var footprint: set<Node<T>>;

  var data: T;
  var next: Node<T>;

  function Valid(): bool
    reads this, footprint;
  {
    this in this.footprint && null !in this.footprint &&
    (next == null ==> list == [data]) &&
    (next != null ==>
        next in footprint && next.footprint <= footprint &&
        this !in next.footprint &&
        list == [data] + next.list &&
        next.Valid())
  }

  method Init(d: T)
    modifies this;
    ensures Valid() && fresh(footprint - {this});
    ensures list == [d];
  {
    data := d;
    next := null;
    list := [d];
    footprint := {this};
  }

  method SkipHead() returns (r: Node<T>)
    requires Valid();
    ensures r == null ==> |list| == 1;
    ensures r != null ==> r.Valid() && r.footprint <= footprint;
    ensures r != null ==> r.list == list[1..];
  {
    r := next;
  }

  method Prepend(d: T) returns (r: Node<T>)
    requires Valid();
    ensures r.Valid() && fresh(r.footprint - old(footprint));
    ensures r.list == [d] + list;
  {
    r := new Node<T>;
    r.data := d;
    r.next := this;
    r.footprint := {r} + this.footprint;
    r.list := [r.data] + this.list;
  }

  method ReverseInPlace() returns (reverse: Node<T>)
    requires Valid();
    modifies footprint;
    ensures reverse != null && reverse.Valid();
    ensures fresh(reverse.footprint - old(footprint));
    ensures |reverse.list| == |old(list)|;
    ensures (forall i :: 0 <= i && i < |old(list)| ==> old(list)[i] == reverse.list[|old(list)|-1-i]);
  {
    var current := next;
    reverse := this;
    reverse.next := null;
    reverse.footprint := {reverse};
    reverse.list := [data];

    while (current != null)
      invariant reverse != null && reverse.Valid();
      invariant reverse.footprint <= old(footprint);
      invariant current == null ==> |old(list)| == |reverse.list|;
      invariant current != null ==>
        current.Valid() &&
        current in old(footprint) && current.footprint <= old(footprint) &&
        current.footprint !! reverse.footprint &&
        |old(list)| == |reverse.list| + |current.list| &&
        (forall i :: 0 <= i && i < |current.list| ==> current.list[i] == old(list)[|reverse.list|+i]);
      invariant
        (forall i :: 0 <= i && i < |reverse.list| ==> old(list)[i] == reverse.list[|reverse.list|-1-i]);
    {
      var nx := current.next;
      assert nx != null ==> (forall i :: 0 <= i && i < |nx.list| ==> current.list[1+i] == nx.list[i]);

      // ..., reverse, current, nx, ...
      assert current.data == current.list[0];
      current.next := reverse;
      current.footprint := {current} + reverse.footprint;
      current.list := [current.data] + reverse.list;

      reverse := current;
      current := nx;
    }
  }
}