Dafny: retired the "call" keyword

8 files changed, 92 insertions, 89 deletions

diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy
index cd4a18c2..3bd2bf43 100644
--- a/Test/VSI-Benchmarks/b1.dfy
+++ b/Test/VSI-Benchmarks/b1.dfy
@@ -35,37 +35,37 @@ method Mul(x: int, y: int) returns (r: int)
   if (x == 0) {

     r := 0;

   } else if (x < 0) {

-    call r := Mul(-x, y);

+    r := Mul(-x, y);

     r := -r;

   } else {

-    call r := Mul(x-1, y);

-    call r := Add(r, y);

+    r := Mul(x-1, y);

+    r := Add(r, y);

   }

 }

 

 // ---------------------------

 

 method Main() {

-  call TestAdd(3, 180);

-  call TestAdd(3, -180);

-  call TestAdd(0, 1);

+  TestAdd(3, 180);

+  TestAdd(3, -180);

+  TestAdd(0, 1);

 

-  call TestMul(3, 180);

-  call TestMul(3, -180);

-  call TestMul(180, 3);

-  call TestMul(-180, 3);

-  call TestMul(0, 1);

-  call TestMul(1, 0);

+  TestMul(3, 180);

+  TestMul(3, -180);

+  TestMul(180, 3);

+  TestMul(-180, 3);

+  TestMul(0, 1);

+  TestMul(1, 0);

 }

 

 method TestAdd(x: int, y: int) {

   print x, " + ", y, " = ";

-  call z := Add(x, y);

+  var z := Add(x, y);

   print z, "\n";

 }

 

 method TestMul(x: int, y: int) {

   print x, " * ", y, " = ";

-  call z := Mul(x, y);

+  var z := Mul(x, y);

   print z, "\n";

 }

diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index 6c6f11b3..3046621b 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -38,13 +38,13 @@ method Main() {
   a[2] := -2;

   a[3] := 0;

   a[4] := 25;

-  call TestSearch(a, 4);

-  call TestSearch(a, -8);

-  call TestSearch(a, -2);

-  call TestSearch(a, 0);

-  call TestSearch(a, 23);

-  call TestSearch(a, 25);

-  call TestSearch(a, 27);

+  TestSearch(a, 4);

+  TestSearch(a, -8);

+  TestSearch(a, -2);

+  TestSearch(a, 0);

+  TestSearch(a, 23);

+  TestSearch(a, 25);

+  TestSearch(a, 27);

 }

 

 method TestSearch(a: array<int>, key: int)

@@ -52,6 +52,6 @@ method TestSearch(a: array<int>, key: int)
   requires (forall i, j :: 0 <= i && i < j && j < a.Length ==> a[i] <= a[j]);

 {

   var b := new Benchmark2;

-  call r := b.BinarySearch(a, key);

+  var r := b.BinarySearch(a, key);

   print "Looking for key=", key, ", result=", r, "\n";

 }

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index 3f30c4b5..3de94555 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -87,10 +87,10 @@ class Benchmark3 {
       invariant (forall i :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);

       invariant (forall i :: 0 <= i && i < |p| ==> q.contents[i] == old(q.contents)[p[i]]);

     {  

-      call m,k := RemoveMin(q);

+      var m,k := RemoveMin(q);

       perm := perm + [p[k]]; //adds index of min to perm

       p := p[k+1..] + p[..k]; //remove index of min from p  

-      call r.Enqueue(m);

+      r.Enqueue(m);

       pperm := pperm[k+1..|p|+1] + pperm[..k] + pperm[|p|+1..] + [pperm[k]];

     }

   }

@@ -116,8 +116,8 @@ class Benchmark3 {
       invariant 0 <= k && k < |old(q.contents)| && old(q.contents)[k] == m;

       invariant (forall i :: 0<= i && i < j ==> m <= old(q.contents)[i]); //m is min so far

     {

-      call x:= q.Dequeue();

-      call q.Enqueue(x);

+      var x := q.Dequeue();

+      q.Enqueue(x);

       if (x < m) { k := j; m := x; }

       j := j+1;

     }

@@ -127,11 +127,11 @@ class Benchmark3 {
       invariant j <= k;

       invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; 

     {

-      call x := q.Dequeue();

-      call q.Enqueue(x);

+      var x := q.Dequeue();

+      q.Enqueue(x);

       j := j+1;

     }

 

-    call m:= q.Dequeue();

+    m := q.Dequeue();

   }

 }

diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index 9f7e272e..b70ff4d0 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -54,7 +54,7 @@ class Map<Key,Value> {
     ensures !present ==> key !in Keys;

     ensures present ==> (exists i :: 0 <= i && i < |Keys| && Keys[i] == key && Values[i] == val);

   {

-    call p, n, prev := FindIndex(key);

+    var p, n, prev := FindIndex(key);

     if (p == null) {

       present := false;

     } else {

@@ -74,7 +74,7 @@ class Map<Key,Value> {
                     Keys[j] == old(Keys)[j] && Values[j] == old(Values)[j]));

     ensures key !in old(Keys) ==> Keys == [key] + old(Keys) && Values == [val] + old(Values);

   {

-    call p, n, prev := FindIndex(key);

+    var p, n, prev := FindIndex(key);

     if (p == null) {

       var h := new Node<Key,Value>;

       h.key := key;  h.val := val;  h.next := head;

@@ -107,7 +107,7 @@ class Map<Key,Value> {
               Keys[h..] == old(Keys)[h+1..] &&

               Values[h..] == old(Values)[h+1..]);

   {

-    call p, n, prev := FindIndex(key);

+    var p, n, prev := FindIndex(key);

     if (p != null) {

       Keys := Keys[..n] + Keys[n+1..];

       Values := Values[..n] + Values[n+1..];

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;

diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy
index 13086f28..fda9ca74 100644
--- a/Test/VSI-Benchmarks/b6.dfy
+++ b/Test/VSI-Benchmarks/b6.dfy
@@ -107,14 +107,14 @@ class Client
   method Main()

   {

     var c := new Collection<int>.Init();

-    call c.Add(33);

-    call c.Add(45);

-    call c.Add(78);

+    c.Add(33);

+    c.Add(45);

+    c.Add(78);

     

     var s := [];

     

-    call iter := c.GetIterator();

-    call b := iter.MoveNext();

+    var iter := c.GetIterator();

+    var b := iter.MoveNext();

     

     while (b)

       invariant iter.Valid() && b == iter.HasCurrent() && fresh(iter.footprint);

@@ -123,13 +123,13 @@ class Client
       invariant iter.c == c;

       decreases |c.elements| - iter.pos;

     {   

-      call x := iter.GetCurrent();

+      var x := iter.GetCurrent();

       s := s + [x];

-      call b := iter.MoveNext();

+      b := iter.MoveNext();

     }

     

     assert s == c.elements; //verifies that the iterator returns the correct things

-    call c.Add(100);

+    c.Add(100);

   }

   

 }

diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy
index 2304e602..f34f5c00 100644
--- a/Test/VSI-Benchmarks/b7.dfy
+++ b/Test/VSI-Benchmarks/b7.dfy
@@ -119,33 +119,34 @@ class Client {
   method Main()

   {

     var rd := new Stream;

-    call rd.Open();

+    rd.Open();

     

     var q := new Queue<int>;  

     while (true)

       invariant rd.Valid() && fresh(rd.footprint) && fresh(q);

       decreases |rd.stream|;

     {

-      call eos := rd.AtEndOfStream();

+      var eos := rd.AtEndOfStream();

       if (eos) {

         break;

       }

         

-      call ch := rd.GetChar();  

-      call q.Enqueue(ch);  

+      var ch := rd.GetChar();  

+      q.Enqueue(ch);  

     }

       

-    call rd.Close();

-    call q,perm := Sort(q);

+    rd.Close();

+    var perm;

+    q,perm := Sort(q);

       

-    var wr:= new Stream;

-    call wr.Create();

+    var wr := new Stream;

+    wr.Create();

     while (0 < |q.contents|)

       invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint;

     {

-      call ch := q.Dequeue();  

-      call wr.PutChar(ch);    

+      var ch := q.Dequeue();  

+      wr.PutChar(ch);    

     }

-    call wr.Close();

+    wr.Close();

   }

 }

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 3438d6e0..0c9d1186 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -46,7 +46,7 @@ class Glossary {
   method Main()

   {

     var rs:= new ReaderStream;

-    call rs.Open();

+    rs.Open();

     var glossary := new Map<Word,seq<Word>>.Init();

     var q := new Queue<Word>.Init();

     

@@ -60,21 +60,22 @@ class Glossary {
       invariant q.contents == glossary.keys;

       decreases *;  // we leave out the decreases clause - unbounded stream

     {

-      call term,definition := readDefinition(rs);

+      var term,definition := readDefinition(rs);

       if (term == null) {

         break;

       }

-      call present, d := glossary.Find(term);

+      var present, d := glossary.Find(term);

       if (!present) {

-        call glossary.Add(term,definition);

-        call q.Enqueue(term);

+        glossary.Add(term,definition);

+        q.Enqueue(term);

       }

     }    

     

-    call rs.Close();

-    call q,p := Sort(q);

+    rs.Close();

+    var p;

+    q,p := Sort(q);

     var wr := new WriterStream;

-    call wr.Create();

+    wr.Create();

     

     while (0 < |q.contents|)

       invariant wr.Valid() && fresh(wr.footprint);

@@ -84,12 +85,12 @@ class Glossary {
       invariant q !in wr.footprint;

       invariant (forall k :: k in q.contents ==> k in glossary.keys);

     {

-      call term := q.Dequeue();

-      call present,definition := glossary.Find(term);

+      var term := q.Dequeue();

+      var present,definition := glossary.Find(term);

       assert present;

       

       // write term with a html anchor

-      call wr.PutWordInsideTag(term, term);

+      wr.PutWordInsideTag(term, term);

       var i := 0;

 

       var qcon := q.contents;

@@ -103,19 +104,20 @@ class Glossary {
         invariant (forall k :: k in q.contents ==> k in glossary.keys);

       {

         var w := definition[i];

-        call present, d := glossary.Find(w);

+        var d;

+        present, d := glossary.Find(w);

         if (present)

         {

-          call wr. PutWordInsideHyperlink(w, w);

+          wr. PutWordInsideHyperlink(w, w);

         }

         else 

         {

-          call wr. PutWord(w);

+          wr. PutWord(w);

         }

         i:= i +1;

       }

     }

-    call wr.Close();          

+    wr.Close();          

   }

     

 

@@ -125,7 +127,7 @@ class Glossary {
     ensures rs.Valid() && fresh(rs.footprint - old(rs.footprint));

     ensures term != null ==> null !in definition;

   {

-    call term := rs.GetWord();

+    term := rs.GetWord();

     if (term != null)

     {

       definition := [];

@@ -134,7 +136,7 @@ class Glossary {
         invariant null !in definition;

         decreases *;  // we leave out the decreases clause - unbounded stream

       {

-        call w := rs.GetWord();

+        var w := rs.GetWord();

         if (w == null)

         {

           break;

@@ -273,7 +275,7 @@ class Map<Key,Value> {
     ensures present ==> (exists i :: 0 <= i && i < |keys| &&

                                      keys[i] == key && values[i] == val);

   {

-    call j := FindIndex(key);

+    var j := FindIndex(key);

     if (j == -1) {

       present := false;

     } else {

@@ -292,7 +294,7 @@ class Map<Key,Value> {
               (forall j :: 0 <= j && j < |values| && i != j ==> keys[j] == old(keys)[j] && values[j] == old(values)[j]));

     ensures key !in old(keys) ==> keys == old(keys) + [key] && values == old(values) + [val];

   {

-    call j := FindIndex(key);

+    var j := FindIndex(key);

     if (j == -1) {

       keys := keys + [key];

       values := values + [val];

@@ -321,7 +323,7 @@ class Map<Key,Value> {
               keys[h..] == old(keys)[h+1..] &&

               values[h..] == old(values)[h+1..]);

   {

-    call j := FindIndex(key);

+    var j := FindIndex(key);

     if (0 <= j) {

       keys := keys[..j] + keys[j+1..];

       values := values[..j] + values[j+1..];