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/b7.dfy | |
| parent | 58795baa8bff26cdb4430b90e69395abf52c4161 (diff) | |
Initial version of VSI Benchmarks 1 - 8
Diffstat (limited to 'Test/VSI-Benchmarks/b7.dfy')
| -rw-r--r-- | Test/VSI-Benchmarks/b7.dfy | 166 |
1 files changed, 166 insertions, 0 deletions
diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy new file mode 100644 index 00000000..13a8ccd2 --- /dev/null +++ b/Test/VSI-Benchmarks/b7.dfy @@ -0,0 +1,166 @@ +// Edited B6 to include GetChar and PutChar
+
+//This is the Queue from Benchmark 3.
+
+//restriction:we assume streams are finite
+//what else can we specify?
+
+
+class Queue<T> {
+ var contents: seq<int>;
+ method Init();
+ modifies this;
+ ensures |contents| == 0;
+ method Enqueue(x: int);
+ modifies this;
+ ensures contents == old(contents) + [x];
+ method Dequeue() returns (x: int);
+ requires 0 < |contents|;
+ modifies this;
+ ensures contents == old(contents)[1..] && x == old(contents)[0];
+ function Head(): int
+ requires 0 < |contents|;
+ reads this;
+ { contents[0] }
+ function Get(i: int): int
+ requires 0 <= i && i < |contents|;
+ reads this;
+ { contents[i] }
+}
+
+class Stream {
+ var footprint:set<object>;
+ var stream:seq<int>;
+ var isOpen:bool;
+
+ function Valid():bool
+ reads this, footprint;
+ {
+ !(null in footprint) && this in footprint && isOpen
+ }
+
+ method GetCount() returns (c:int)
+ requires Valid();
+ ensures 0<=c;
+ {
+ c:=|stream|;
+ }
+
+ method Create() //writing
+ modifies this;
+ ensures Valid() && fresh(footprint -{this});
+ ensures stream == [];
+ {
+ stream := [];
+ footprint := {this};
+ isOpen:= true;
+ }
+
+ method Open() //reading
+ modifies this;
+ ensures Valid() && fresh(footprint -{this});
+ {
+ footprint := {this};
+ isOpen :=true;
+ }
+
+ method PutChar(x:int )
+ requires Valid();
+ modifies footprint;
+ ensures Valid() && fresh(footprint - old(footprint));
+ ensures stream == old(stream) + [x];
+ {
+ stream:= stream + [x];
+ }
+
+ method GetChar()returns(x:int)
+ requires Valid() && 0< |stream|;
+ modifies footprint;
+ ensures Valid() && fresh(footprint - old(footprint));
+ ensures x ==old(stream)[0];
+ ensures stream == old(stream)[1..];
+ {
+ x := stream[0];
+ stream:= stream[1..];
+
+ }
+
+ method AtEndOfStream() returns(eos:bool)
+ requires Valid();
+ ensures eos <==> |stream| ==0;
+ {
+ eos:= |stream| ==0;
+ }
+
+ method Close()
+ requires Valid();
+ modifies footprint;
+ {
+ isOpen := false;
+
+ }
+
+}
+
+
+
+class Client {
+
+
+ method Sort(q: Queue<int>) returns (r: Queue<int>, perm:seq<int>);
+ requires q != null;
+ modifies q;
+ ensures r != null && fresh(r);
+ ensures |r.contents| == |old(q.contents)|;
+ ensures (forall i, j :: 0 <= i && i < j && j < |r.contents| ==>
+ r.Get(i) <= r.Get(j));
+ //perm is a permutation
+ ensures |perm| == |r.contents|; // ==|pperm|
+ ensures (forall i: int :: 0 <= i && i < |perm|==> 0 <= perm[i] && perm[i] < |perm| );
+ ensures (forall i, j: int :: 0 <= i && i < j && j < |perm| ==> perm[i] != perm[j]);
+ // the final Queue is a permutation of the input Queue
+ ensures (forall i: int :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);
+
+
+
+ method Main()
+ {
+ var rd:= new Stream;
+ call rd.Open();
+
+ var q:= new Queue<int>;
+ var ch;
+ while (true)
+ invariant rd.Valid() && fresh(rd.footprint) && fresh(q);
+ decreases |rd.stream|;
+ {
+ var eos:bool;
+ call eos := rd.AtEndOfStream();
+ if (eos)
+ {
+ break;
+ }
+
+ call ch := rd.GetChar();
+ call q.Enqueue(ch);
+ }
+
+ call rd.Close();
+ var perm;
+ call q,perm := Sort(q);
+
+ var wr:= new Stream;
+ call wr.Create();
+ while (0<|q.contents|)
+ invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && !(q in wr.footprint);
+ decreases |q.contents|;
+ {
+ call ch:= q.Dequeue();
+ call wr.PutChar(ch);
+ }
+ call wr.Close();
+
+ }
+
+}
+
|