Dafny: retired the "call" keyword

5 files changed, 22 insertions, 22 deletions

diff --git a/Test/VSComp2010/Problem1-SumMax.dfy b/Test/VSComp2010/Problem1-SumMax.dfy
index 1b105ac1..3db9bf72 100644
--- a/Test/VSComp2010/Problem1-SumMax.dfy
+++ b/Test/VSComp2010/Problem1-SumMax.dfy
@@ -38,6 +38,6 @@ method Main()
   a[7] := 1;

   a[8] := 10;

   a[9] := 6;

-  call s, m := M(10, a);

+  var s, m := M(10, a);

   print "N = ", a.Length, "  sum = ", s, "  max = ", m, "\n";

 }

diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy
index bf6aca37..2a262d70 100644
--- a/Test/VSComp2010/Problem2-Invert.dfy
+++ b/Test/VSComp2010/Problem2-Invert.dfy
@@ -61,11 +61,11 @@ method Main()
   a[8] := 5;

   a[9] := 6;

   var b := new int[10];

-  call M(10, a, b);

+  M(10, a, b);

   print "a:\n";

-  call PrintArray(a);

+  PrintArray(a);

   print "b:\n";

-  call PrintArray(b);

+  PrintArray(b);

 }

 

 method PrintArray(a: array<int>)

diff --git a/Test/VSComp2010/Problem3-FindZero.dfy b/Test/VSComp2010/Problem3-FindZero.dfy
index 03e6bdfe..3d24255d 100644
--- a/Test/VSComp2010/Problem3-FindZero.dfy
+++ b/Test/VSComp2010/Problem3-FindZero.dfy
@@ -82,11 +82,11 @@ static method Search(ll: Node) returns (r: int)
 method Main()

 {

   var list: Node := null;

-  call list := list.Cons(0, list);

-  call list := list.Cons(5, list);

-  call list := list.Cons(0, list);

-  call list := list.Cons(8, list);

-  call r := Search(list);

+  list := list.Cons(0, list);

+  list := list.Cons(5, list);

+  list := list.Cons(0, list);

+  list := list.Cons(8, list);

+  var r := Search(list);

   print "Search returns ", r, "\n";

   assert r == 1;

 }

diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy
index ef084674..2f21b7a1 100644
--- a/Test/VSComp2010/Problem4-Queens.dfy
+++ b/Test/VSComp2010/Problem4-Queens.dfy
@@ -39,7 +39,7 @@ method Search(N: int) returns (success: bool, board: seq<int>)
                   ==>

                   (exists p :: 0 <= p && p < N && !IsConsistent(B, p)));

 {

-  call success, board := SearchAux(N, []);

+  success, board := SearchAux(N, []);

 }

 

 // Given a board, this function says whether or not the queen placed in column 'pos'

@@ -110,7 +110,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard:
 

         // Thus, we meet the precondition of 'SearchAux' on 'candidateBoard', so let's search

         // for a solution that extends 'candidateBoard'.

-        call s, b := SearchAux(N, candidateBoard);

+        var s, b := SearchAux(N, candidateBoard);

         if (s) {

           // The recursive call to 'SearchAux' found consistent positions for all remaining columns

           newBoard := b;

@@ -137,11 +137,11 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard:
 

 method Main()

 {

-  call s, b := Search(2);

+  var s, b := Search(2);

   print "N=2 returns ", s, "\n";

-  call s, b := Search(4);

+  s, b := Search(4);

   print "N=4 returns ", s, "\n";

-  call PrintSeq(b);

+  PrintSeq(b);

 }

 

 method PrintSeq(b: seq<int>)

diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
index df8cb1b7..0e141927 100644
--- a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
+++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
@@ -46,8 +46,8 @@ class AmortizedQueue<T> {
       front := f;

       rear := r;

     } else {

-      call rr := r.Reverse();

-      call ff := f.Concat(rr);

+      var rr := r.Reverse();

+      var ff := f.Concat(rr);

       front := ff;

 

       rear := new LinkedList<T>.Init();

@@ -75,7 +75,7 @@ class AmortizedQueue<T> {
     requires Valid();

     ensures r != null && r.Valid() && r.List == List + [item];

   {

-    call rr := rear.Cons(item);

+    var rr := rear.Cons(item);

     r := new AmortizedQueue<T>.InitFromPieces(front, rr);

   }

 }

@@ -133,8 +133,8 @@ class LinkedList<T> {
     if (length == 0) {

       r := end;

     } else {

-      call c := tail.Concat(end);

-      call r := c.Cons(head);

+      var c := tail.Concat(end);

+      r := c.Cons(head);

     }

   }

 

@@ -148,10 +148,10 @@ class LinkedList<T> {
     if (length == 0) {

       r := this;

     } else {

-      call r := tail.Reverse();

+      r := tail.Reverse();

       var e := new LinkedList<T>.Init();

-      call e := e.Cons(head);

-      call r := r.Concat(e);

+      e := e.Cons(head);

+      r := r.Concat(e);

     }

   }