diff options
Diffstat (limited to 'Test/VSI-Benchmarks/b7.dfy')
| -rw-r--r-- | Test/VSI-Benchmarks/b7.dfy | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy index 2304e602..f34f5c00 100644 --- a/Test/VSI-Benchmarks/b7.dfy +++ b/Test/VSI-Benchmarks/b7.dfy @@ -119,33 +119,34 @@ class Client { method Main()
{
var rd := new Stream;
- call rd.Open();
+ rd.Open();
var q := new Queue<int>;
while (true)
invariant rd.Valid() && fresh(rd.footprint) && fresh(q);
decreases |rd.stream|;
{
- call eos := rd.AtEndOfStream();
+ var eos := rd.AtEndOfStream();
if (eos) {
break;
}
- call ch := rd.GetChar();
- call q.Enqueue(ch);
+ var ch := rd.GetChar();
+ q.Enqueue(ch);
}
- call rd.Close();
- call q,perm := Sort(q);
+ rd.Close();
+ var perm;
+ q,perm := Sort(q);
- var wr:= new Stream;
- call wr.Create();
+ var wr := new Stream;
+ wr.Create();
while (0 < |q.contents|)
invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint;
{
- call ch := q.Dequeue();
- call wr.PutChar(ch);
+ var ch := q.Dequeue();
+ wr.PutChar(ch);
}
- call wr.Close();
+ wr.Close();
}
}
|