summaryrefslogtreecommitdiff
path: root/Test/VSI-Benchmarks/b5.dfy
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2011-05-26 00:02:57 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2011-05-26 00:02:57 -0700
commitd9f2a82a417703f3669ba8399dcc8bcf34c3d742 (patch)
tree08b309fd809639a62c453c33dac86845dd4b9815 /Test/VSI-Benchmarks/b5.dfy
parente52270deab6d2fd5b885848211c2d9d1ab814b09 (diff)
Dafny: retired the "call" keyword
Diffstat (limited to 'Test/VSI-Benchmarks/b5.dfy')
-rw-r--r--Test/VSI-Benchmarks/b5.dfy36
1 files changed, 18 insertions, 18 deletions
diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy
index d9bd36f5..cd132ef3 100644
--- a/Test/VSI-Benchmarks/b5.dfy
+++ b/Test/VSI-Benchmarks/b5.dfy
@@ -98,9 +98,9 @@ class Queue<T> {
ensures Valid() && fresh(footprint - old(footprint));
ensures contents == old(contents)[1..] + old(contents)[..1];
{
- call t := Front();
- call Dequeue();
- call Enqueue(t);
+ var t := Front();
+ Dequeue();
+ Enqueue(t);
}
method RotateAny()
@@ -112,9 +112,9 @@ class Queue<T> {
ensures (exists i :: 0 <= i && i <= |contents| &&
contents == old(contents)[i..] + old(contents)[..i]);
{
- call t := Front();
- call Dequeue();
- call Enqueue(t);
+ var t := Front();
+ Dequeue();
+ Enqueue(t);
}
}
@@ -152,18 +152,18 @@ class Main<U> {
var q0 := new Queue<T>.Init();
var q1 := new Queue<T>.Init();
- call q0.Enqueue(t);
- call q0.Enqueue(u);
+ q0.Enqueue(t);
+ q0.Enqueue(u);
- call q1.Enqueue(v);
+ q1.Enqueue(v);
assert |q0.contents| == 2;
- call w := q0.Front();
+ var w := q0.Front();
assert w == t;
- call q0.Dequeue();
+ q0.Dequeue();
- call w := q0.Front();
+ w := q0.Front();
assert w == u;
assert |q0.contents| == 1;
@@ -179,18 +179,18 @@ class Main<U> {
ensures fresh(q0.footprint - old(q0.footprint));
ensures fresh(q1.footprint - old(q1.footprint));
{
- call q0.Enqueue(t);
- call q0.Enqueue(u);
+ q0.Enqueue(t);
+ q0.Enqueue(u);
- call q1.Enqueue(v);
+ q1.Enqueue(v);
assert |q0.contents| == 2;
- call w := q0.Front();
+ var w := q0.Front();
assert w == t;
- call q0.Dequeue();
+ q0.Dequeue();
- call w := q0.Front();
+ w := q0.Front();
assert w == u;
assert |q0.contents| == 1;