summaryrefslogtreecommitdiff
path: root/Test/dafny1/UnboundedStack.dfy
blob: 4c3b095a6ecf9c8f9faa46a392a6c6e37b863a14 (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
93
94
95
96
97
98
class UnboundedStack<T> {
  ghost var representation: set<object>;
  ghost var content: seq<T>;
  var top: Node<T>;

  function IsUnboundedStack(): bool
    reads this, representation;
  {
    this in representation &&
    (top == null ==>
      content == []) &&
    (top != null ==>
      top in representation && this !in top.footprint && top.footprint <= representation &&
      content == top.content &&
      top.Valid())
  }

  method InitUnboundedStack()
    modifies this;
    ensures IsUnboundedStack();
    ensures content == [];
  {
    this.top := null;
    this.content := [];
    this.representation := {this};
  }

  method Push(val: T)
    requires IsUnboundedStack();
    modifies this;
    ensures IsUnboundedStack();
    ensures content == [val] + old(content);
  {
    var tmp := new Node<T>;
    call tmp.InitNode(val,top);
    top := tmp;
    representation := representation + top.footprint;
    content := [val] + content;
  }

  method Pop() returns (result: T)
    requires IsUnboundedStack();
    requires content != [];
    modifies this;
    ensures IsUnboundedStack();
    ensures content == old(content)[1..];
  {
    result := top.val;
    top := top.next;
    content := content[1..];
  }

  method isEmpty() returns (result: bool)
    requires IsUnboundedStack();
    ensures result <==> content == [];
  {
    result := top == null;
  }
}

class Node<T> {
  ghost var footprint: set<object>;
  ghost var content: seq<T>;
  var val: T;
  var next: Node<T>;

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

  method InitNode(val: T, next: Node<T>)
    requires next != null ==> next.Valid() && !(this in next.footprint);
    modifies this;
    ensures Valid();
    ensures next != null ==> content == [val] + next.content && 
                             footprint == {this} + next.footprint;
    ensures next == null ==> content == [val] &&
                             footprint == {this};
  {
    this.val := val;
    this.next := next;
    if (next == null) {
      this.footprint := {this};
      this.content := [val];      
    } else {
      this.footprint := {this} + next.footprint;
      this.content := [val] + next.content;      
    }
  }
}