Dafny: retired the "call" keyword

1 files changed, 11 insertions, 10 deletions

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 5d411eb3..155fbaef 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -28,8 +28,8 @@ class Termination {
   }

 

   method Lex() {

-    call x := Update();

-    call y := Update();

+    var x := Update();

+    var y := Update();

     while (!(x == 0 && y == 0))

       invariant 0 <= x && 0 <= y;

       decreases x, y;

@@ -38,7 +38,7 @@ class Termination {
         y := y - 1;

       } else {

         x := x - 1;

-        call y := Update();

+        y := Update();

       }

     }

   }

@@ -82,7 +82,8 @@ class Termination {
     while (l != List.Nil)

       decreases l;

     {

-      call x, l := Traverse(l);

+      var x;

+      x, l := Traverse(l);

     }

   }

 

@@ -204,7 +205,7 @@ method OuterOld(a: int)
   decreases a, true;

 {

   count := count + 1;

-  call InnerOld(a, count);

+  InnerOld(a, count);

 }

 

 method InnerOld(a: int, b: int)

@@ -213,9 +214,9 @@ method InnerOld(a: int, b: int)
 {

   count := count + 1;

   if (b == 0 && 1 <= a) {

-    call OuterOld(a - 1);

+    OuterOld(a - 1);

   } else if (1 <= b) {

-    call InnerOld(a, b - 1);

+    InnerOld(a, b - 1);

   }

 }

 

@@ -225,7 +226,7 @@ method Outer(a: int)
   modifies this;

 {

   count := count + 1;

-  call Inner(a, count);

+  Inner(a, count);

 }

 

 method Inner(a: int, b: int)

@@ -233,9 +234,9 @@ method Inner(a: int, b: int)
 {

   count := count + 1;

   if (b == 0 && 1 <= a) {

-    call Outer(a - 1);

+    Outer(a - 1);

   } else if (1 <= b) {

-    call Inner(a, b - 1);

+    Inner(a, b - 1);

   }

 }