diff options
Diffstat (limited to 'Test/VSI-Benchmarks/b7.dfy')
| -rw-r--r-- | Test/VSI-Benchmarks/b7.dfy | 167 |
1 files changed, 78 insertions, 89 deletions
diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy index ddad7599..e5af6357 100644 --- a/Test/VSI-Benchmarks/b7.dfy +++ b/Test/VSI-Benchmarks/b7.dfy @@ -29,84 +29,78 @@ class Queue<T> { }
class Stream {
- var footprint:set<object>;
+ ghost var footprint:set<object>;
var stream:seq<int>;
var isOpen:bool;
function Valid():bool
- reads this, footprint;
+ reads this, footprint;
{
- null !in footprint && this in footprint && isOpen
+ null !in footprint && this in footprint && isOpen
}
method GetCount() returns (c:int)
- requires Valid();
- ensures 0<=c;
+ requires Valid();
+ ensures 0 <= c;
{
- c:=|stream|;
+ c := |stream|;
}
method Create() //writing
- modifies this;
- ensures Valid() && fresh(footprint -{this});
- ensures stream == [];
+ modifies this;
+ ensures Valid() && fresh(footprint - {this});
+ ensures stream == [];
{
- stream := [];
- footprint := {this};
- isOpen:= true;
+ stream := [];
+ footprint := {this};
+ isOpen := true;
}
method Open() //reading
- modifies this;
- ensures Valid() && fresh(footprint -{this});
+ modifies this;
+ ensures Valid() && fresh(footprint - {this});
{
- footprint := {this};
- isOpen :=true;
+ footprint := {this};
+ isOpen := true;
}
method PutChar(x:int )
- requires Valid();
- modifies footprint;
- ensures Valid() && fresh(footprint - old(footprint));
- ensures stream == old(stream) + [x];
+ requires Valid();
+ modifies footprint;
+ ensures Valid() && fresh(footprint - old(footprint));
+ ensures stream == old(stream) + [x];
{
- stream:= 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..];
+ 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..];
-
+ 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;
-
- }
+ 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;
@@ -115,49 +109,44 @@ class Client { 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]]);
+ 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>;
- while (true)
- invariant rd.Valid() && fresh(rd.footprint) && fresh(q);
- decreases |rd.stream|;
- {
- call eos := rd.AtEndOfStream();
- if (eos)
- {
- break;
- }
-
- call ch := rd.GetChar();
- call q.Enqueue(ch);
- }
-
- call rd.Close();
- 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();
-
- }
-
+ method Main()
+ {
+ var rd := new Stream;
+ call rd.Open();
+
+ var q := new Queue<int>;
+ while (true)
+ invariant rd.Valid() && fresh(rd.footprint) && fresh(q);
+ decreases |rd.stream|;
+ {
+ call eos := rd.AtEndOfStream();
+ if (eos) {
+ break;
+ }
+
+ call ch := rd.GetChar();
+ call q.Enqueue(ch);
+ }
+
+ call rd.Close();
+ 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();
+ }
}
-
|