From d9f2a82a417703f3669ba8399dcc8bcf34c3d742 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Thu, 26 May 2011 00:02:57 -0700
Subject: Dafny: retired the "call" keyword

---
 Test/VSComp2010/Problem1-SumMax.dfy           |  2 +-
 Test/VSComp2010/Problem2-Invert.dfy           |  6 +++---
 Test/VSComp2010/Problem3-FindZero.dfy         | 10 +++++-----
 Test/VSComp2010/Problem4-Queens.dfy           | 10 +++++-----
 Test/VSComp2010/Problem5-DoubleEndedQueue.dfy | 16 ++++++++--------
 5 files changed, 22 insertions(+), 22 deletions(-)

(limited to 'Test/VSComp2010')

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);
     }
   }
 
-- 
cgit v1.2.3