Dafny: retired the "call" keyword

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;