diff options
| author |  RMonahan <unknown> | 2009-10-30 23:52:13 +0000 |
|---|---|---|
| committer | RMonahan <unknown> | 2009-10-30 23:52:13 +0000 |
| commit | cb32052c7ae22c970d5db7dd51881845adfa66d2 (patch) | |
| tree | 2ebc190bc336ed412f6b39c1b131f01644f70faf /Test/VSI-Benchmarks/b6.dfy | |
| parent | 58795baa8bff26cdb4430b90e69395abf52c4161 (diff) | |
Initial version of VSI Benchmarks 1 - 8
Diffstat (limited to 'Test/VSI-Benchmarks/b6.dfy')
| -rw-r--r-- | Test/VSI-Benchmarks/b6.dfy | 139 |
1 files changed, 139 insertions, 0 deletions
diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy new file mode 100644 index 00000000..e5d061d2 --- /dev/null +++ b/Test/VSI-Benchmarks/b6.dfy @@ -0,0 +1,139 @@ +
+class Collection {
+ var footprint:set<object>;
+ var elements:seq<int>;
+
+ 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:int)
+ requires Valid();
+ requires 0<=i && i<|elements|;
+ ensures elements[i] ==x;
+ {
+ x:=elements[i];
+ }
+
+ method Add(x:int )
+ requires Valid();
+ modifies footprint;
+ ensures Valid() && fresh(footprint - old(footprint));
+ ensures elements == old(elements) + [x];
+ {
+ elements:= elements + [x];
+ }
+
+ method GetIterator() returns (iter:Iterator)
+ requires Valid();
+ ensures iter != null && iter.Valid();
+ ensures fresh(iter.footprint) && iter.pos == -1;
+ ensures iter.c == this;
+ {
+ iter:= new Iterator;
+ call iter.Init(this);
+ }
+
+}
+
+class Iterator {
+
+ var c:Collection;
+ var pos:int;
+
+ var footprint:set<object>;
+
+ function Valid():bool
+ reads this, footprint;
+ {
+ this in footprint && c!= null && -1<= pos && !(null in footprint)
+ }
+
+ method Init(coll:Collection)
+ 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:int)
+ requires Valid() && HasCurrent();
+ ensures c.elements[pos] == x;
+ {
+ x:=c.elements[pos];
+ }
+
+}
+
+class Client
+{
+
+ method Main()
+ {
+ var c:= new Collection;
+ call c.Init();
+ call c.Add(33);
+ call c.Add(45);
+ call c.Add(78);
+
+ var iter,b,x, s:= [ ];
+
+ call iter:=c.GetIterator();
+ call b:= iter.MoveNext();
+
+ while (b)
+ invariant b == iter.HasCurrent() && fresh(iter.footprint) && iter.Valid();
+ 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;
+ {
+ call x:= iter.GetCurrent();
+ s:= s + [x];
+ call b:= iter.MoveNext();
+ }
+
+ assert s == c.elements; //verifies that the iterator returns the correct things
+ call c.Add(100);
+ }
+
+}
+
|