summaryrefslogtreecommitdiff
path: root/Test/VSI-Benchmarks/b6.dfy
blob: fda9ca7483e5eac243ca9852c33b634cd2748856 (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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135

class Collection<T> {
  ghost var footprint:set<object>;
  var elements:seq<T>;
  
  function Valid():bool
    reads this, footprint;
  {
    this in footprint
  }
  
  method GetCount() returns (c:int)
    requires Valid();
    ensures 0<=c;
  {
    c:=|elements|;
  }
  
  method Init()
    modifies this;
    ensures Valid() && fresh(footprint -{this});
  {
    elements := [];
    footprint := {this}; 
  }
  
  method GetItem(i:int ) returns (x:T)
    requires Valid();
    requires 0<=i && i<|elements|;
    ensures elements[i] ==x;
  {
    x:=elements[i];
  }
  
  method Add(x:T )
    requires Valid();
    modifies footprint;
    ensures Valid() && fresh(footprint - old(footprint));
    ensures elements == old(elements) + [x];
  {
    elements:= elements + [x];
  }
  
  method GetIterator() returns (iter:Iterator<T>)
    requires Valid();
    ensures iter != null && iter.Valid();
    ensures fresh(iter.footprint) && iter.pos == -1;
    ensures iter.c == this;
  {
      iter:= new Iterator<T>.Init(this);
  }
  
}

class Iterator<T> {
 
  var c:Collection<T>;
  var pos:int;
  
  ghost var footprint:set<object>;
  
  function Valid():bool
    reads this, footprint;
  {
    this in footprint && c != null && -1 <= pos && null !in footprint
  }
  
  method Init(coll:Collection<T>)
    requires coll != null;
    modifies this;
    ensures Valid() && fresh(footprint - {this}) && pos == -1;
    ensures c == coll;
  {
    c := coll;
    pos := -1;
    footprint := {this}; 
  }
  
  method MoveNext() returns (b:bool)
    requires Valid();
    modifies footprint;
    ensures fresh(footprint - old(footprint)) &&  Valid()  && pos == old(pos) + 1;
    ensures b == HasCurrent() && c == old(c);
  {
    pos := pos+1;
    b := pos < |c.elements|;
  }
  
  function HasCurrent():bool //???
    requires Valid();
    reads this, c;
  {
    0 <= pos && pos < |c.elements|
  }
 
  method GetCurrent() returns (x:T)
    requires Valid() && HasCurrent();
    ensures c.elements[pos] == x;
  {
    x := c.elements[pos];
  }
} 

class Client
{

  method Main()
  {
    var c := new Collection<int>.Init();
    c.Add(33);
    c.Add(45);
    c.Add(78);
    
    var s := [];
    
    var iter := c.GetIterator();
    var b := iter.MoveNext();
    
    while (b)
      invariant iter.Valid() && b == iter.HasCurrent() && fresh(iter.footprint);
      invariant c.Valid() && fresh(c.footprint) && iter.footprint !! c.footprint; //disjoint footprints
      invariant 0 <= iter.pos && iter.pos <=|c.elements| && s == c.elements[..iter.pos] ;
      invariant iter.c == c;
      decreases |c.elements| - iter.pos;
    {   
      var x := iter.GetCurrent();
      s := s + [x];
      b := iter.MoveNext();
    }
    
    assert s == c.elements; //verifies that the iterator returns the correct things
    c.Add(100);
  }
  
}