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/vacid0/Composite.dfy   | 30 +++++++++++++++---------------
 Test/vacid0/SparseArray.dfy |  8 +++-----
 2 files changed, 18 insertions(+), 20 deletions(-)

(limited to 'Test/vacid0')

diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy
index 95ad12fa..ed376931 100644
--- a/Test/vacid0/Composite.dfy
+++ b/Test/vacid0/Composite.dfy
@@ -44,7 +44,7 @@ class Composite {
   {
     var delta := x - val;
     val := x;
-    call Adjust(delta, S, S);
+    Adjust(delta, S, S);
   }
 
   method Add(ghost S: set<Composite>, child: Composite, ghost U: set<Composite>)
@@ -73,7 +73,7 @@ class Composite {
       right := child;
     }
     child.parent := this;
-    call Adjust(child.sum, S, S+U);
+    Adjust(child.sum, S, S+U);
   }
 
   method Dislodge(ghost S: set<Composite>)
@@ -97,7 +97,7 @@ class Composite {
         p.right := null;
       }
       var delta := -sum;
-      call p.Adjust(delta, S - {this}, S);
+      p.Adjust(delta, S - {this}, S);
     }
   }
 
@@ -138,35 +138,35 @@ method Main()
   var c0 := new Composite.Init(57);
 
   var c1 := new Composite.Init(12);
-  call c0.Add({c0}, c1, {c1});
+  c0.Add({c0}, c1, {c1});
 
   var c2 := new Composite.Init(48);
 
   var c3 := new Composite.Init(48);
-  call c2.Add({c2}, c3, {c3});
-  call c0.Add({c0,c1}, c2, {c2,c3});
+  c2.Add({c2}, c3, {c3});
+  c0.Add({c0,c1}, c2, {c2,c3});
 
   ghost var S := {c0, c1, c2, c3};
-  call c1.Update(100, S);
-  call c2.Update(102, S);
+  c1.Update(100, S);
+  c2.Update(102, S);
 
-  call c2.Dislodge(S);
-  call c2.Update(496, S);
-  call c0.Update(0, S);
+  c2.Dislodge(S);
+  c2.Update(496, S);
+  c0.Update(0, S);
 }
 
 method Harness() {
   var a := new Composite.Init(5);
   var b := new Composite.Init(7);
-  call a.Add({a}, b, {b});
+  a.Add({a}, b, {b});
   assert a.sum == 12;
 
-  call b.Update(17, {a,b});
+  b.Update(17, {a,b});
   assert a.sum == 22;
 
   var c := new Composite.Init(10);
-  call b.Add({a,b}, c, {c});
-  call b.Dislodge({a,b,c});
+  b.Add({a,b}, c, {c});
+  b.Dislodge({a,b,c});
   assert b.sum == 27;
 }
 
diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy
index 2c217264..989ddfc6 100644
--- a/Test/vacid0/SparseArray.dfy
+++ b/Test/vacid0/SparseArray.dfy
@@ -37,11 +37,9 @@ class SparseArray<T> {
     ensures |Contents| == N && this.zero == zero;
     ensures (forall x :: x in Contents ==> x == zero);
   {
-    var aa;
-    var ii;
-    call aa := AllocateArray(N);  this.a := aa;
-    call ii := AllocateArray(N);  this.b := ii;
-    call ii := AllocateArray(N);  this.c := ii;
+    var aa := AllocateArray(N);  this.a := aa;
+    var bb := AllocateArray(N);  this.b := bb;
+    bb := AllocateArray(N);  this.c := bb;
     this.n := 0;
 
     // initialize ghost variable Contents to a sequence of length N containing only zero's,
-- 
cgit v1.2.3