Dafny: retired the "call" keyword

14 files changed, 99 insertions, 98 deletions

diff --git a/Test/dafny1/BinaryTree.dfy b/Test/dafny1/BinaryTree.dfy
index b4980d4b..88b06605 100644
--- a/Test/dafny1/BinaryTree.dfy
+++ b/Test/dafny1/BinaryTree.dfy
@@ -32,7 +32,7 @@ class IntSet {
     if (root == null) {

       present := false;

     } else {

-      call present := root.Find(x);

+      present := root.Find(x);

     }

   }

 

@@ -42,7 +42,7 @@ class IntSet {
     ensures Valid() && fresh(Repr - old(Repr));

     ensures Contents == old(Contents) + {x};

   { 

-    call t := InsertHelper(x, root);

+    var t := InsertHelper(x, root);

     root := t;

     Contents := root.Contents;

     Repr := root.Repr + {this};

@@ -64,12 +64,12 @@ class IntSet {
     } else {

       if (x < n.data) {

         assert n.right == null || n.right.Valid();

-        call t := InsertHelper(x, n.left);

+        var t := InsertHelper(x, n.left);

         n.left := t;

         n.Repr := n.Repr + n.left.Repr;

       } else {

         assert n.left == null || n.left.Valid();

-        call t := InsertHelper(x, n.right);

+        var t := InsertHelper(x, n.right);

         n.right := t;

         n.Repr := n.Repr + n.right.Repr;

       }

@@ -85,7 +85,7 @@ class IntSet {
     ensures Contents == old(Contents) - {x};

   {

     if (root != null) {

-      call newRoot := root.Remove(x);

+      var newRoot := root.Remove(x);

       root := newRoot;

       if (root == null) {

         Contents := {};

@@ -152,9 +152,9 @@ class Node {
     if (x == data) {

       present := true;

     } else if (left != null && x < data) {

-      call present := left.Find(x);

+      present := left.Find(x);

     } else if (right != null && data < x) {

-      call present := right.Find(x);

+      present := right.Find(x);

     } else {

       present := false;

     }

@@ -171,12 +171,12 @@ class Node {
   {

     node := this;

     if (left != null && x < data) {

-      call t := left.Remove(x);

+      var t := left.Remove(x);

       left := t;

       Contents := Contents - {x};

       if (left != null) { Repr := Repr + left.Repr; }

     } else if (right != null && data < x) {

-      call t := right.Remove(x);

+      var t := right.Remove(x);

       right := t;

       Contents := Contents - {x};

       if (right != null) { Repr := Repr + right.Repr; }

@@ -189,7 +189,7 @@ class Node {
         node := left;

       } else {

         // rotate

-        call min, r := right.RemoveMin();

+        var min, r := right.RemoveMin();

         data := min;  right := r;

         Contents := Contents - {x};

         if (right != null) { Repr := Repr + right.Repr; }

@@ -211,7 +211,8 @@ class Node {
       min := data;

       node := right;

     } else {

-      call min, t := left.RemoveMin();

+      var t;

+      min, t := left.RemoveMin();

       left := t;

       node := this;

       Contents := Contents - {min};

@@ -225,9 +226,9 @@ class Main {
   {

     var s := new IntSet.Init();

 

-    call s.Insert(12);

-    call s.Insert(24);

-    call present := s.Find(x);

+    s.Insert(12);

+    s.Insert(24);

+    var present := s.Find(x);

     assert present <==> x == 12 || x == 24;

   }

 

@@ -235,8 +236,8 @@ class Main {
     requires s != null && s.Valid();

     modifies s.Repr;

   {

-    call s.Insert(x);

-    call s.Insert(24);

+    s.Insert(x);

+    s.Insert(24);

     assert old(s.Contents) - {x,24} == s.Contents - {x,24};

   }

 }

diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy
index 089a72c4..2dc49cd9 100644
--- a/Test/dafny1/ExtensibleArray.dfy
+++ b/Test/dafny1/ExtensibleArray.dfy
@@ -57,7 +57,7 @@ class ExtensibleArray<T> {
     if (M <= i) {

       t := elements[i - M];

     } else {

-      call arr := more.Get(i / 256);

+      var arr := more.Get(i / 256);

       t := arr[i % 256];

     }

   }

@@ -72,7 +72,7 @@ class ExtensibleArray<T> {
     if (M <= i) {

       elements[i - M] := t;

     } else {

-      call arr := more.Get(i / 256);

+      var arr := more.Get(i / 256);

       arr[i % 256] := t;

     }

     Contents := Contents[i := t];

@@ -94,7 +94,7 @@ class ExtensibleArray<T> {
         Repr := Repr + {more} + more.Repr;

       }

       // "elements" is full, so move it into "more" and allocate a new array

-      call more.Append(elements);

+      more.Append(elements);

       Repr := Repr + more.Repr;

       M := M + 256;

       elements := new T[256];

@@ -113,14 +113,14 @@ method Main() {
     invariant a.Valid() && fresh(a.Repr);

     invariant |a.Contents| == n;

   {

-    call a.Append(n);

+    a.Append(n);

     n := n + 1;

   }

-  call k := a.Get(570); print k, "\n";

-  call k := a.Get(0); print k, "\n";

-  call k := a.Get(1000); print k, "\n";

-  call a.Set(1000, 23);

-  call k := a.Get(0); print k, "\n";

-  call k := a.Get(1000); print k, "\n";

-  call k := a.Get(66000); print k, "\n";

+  var k := a.Get(570); print k, "\n";

+  k := a.Get(0); print k, "\n";

+  k := a.Get(1000); print k, "\n";

+  a.Set(1000, 23);

+  k := a.Get(0); print k, "\n";

+  k := a.Get(1000); print k, "\n";

+  k := a.Get(66000); print k, "\n";

 }

diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy
index cff8b934..76e67205 100644
--- a/Test/dafny1/FindZero.dfy
+++ b/Test/dafny1/FindZero.dfy
@@ -9,7 +9,7 @@ method FindZero(a: array<int>) returns (r: int)
     invariant forall i :: 0 <= i && i < n && i < a.Length ==> a[i] != 0;

   {

     if (a[n] == 0) { r := n; return; }

-    call Lemma(a, n, a[n]);

+    Lemma(a, n, a[n]);

     n := n + a[n];

   }

   r := -1;

@@ -25,6 +25,6 @@ ghost method Lemma(a: array<int>, k: int, m: int)
 {

   if (0 < m && k < a.Length) {

     assert a[k] != 0;

-    call Lemma(a, k+1, m-1);

+    Lemma(a, k+1, m-1);

   }

 }

diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index 0e4c58e0..2c90769b 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -24,8 +24,8 @@ class IntegerInduction {
     ensures SumOfCubes(n) == Gauss(n) * Gauss(n);

   {

     if (n != 0) {

-      call Theorem0(n-1);

-      call Lemma(n-1);

+      Theorem0(n-1);

+      Lemma(n-1);

     }

   }

 

@@ -33,7 +33,7 @@ class IntegerInduction {
     requires 0 <= n;

     ensures 2 * Gauss(n) == n*(n+1);

   {

-    if (n != 0) { call Lemma(n-1); }

+    if (n != 0) { Lemma(n-1); }

   }

 

   // Here is another proof.  It states the lemma as part of the theorem, and

@@ -45,7 +45,7 @@ class IntegerInduction {
     ensures 2 * Gauss(n) == n*(n+1);

   {

     if (n != 0) {

-      call Theorem1(n-1);

+      Theorem1(n-1);

     }

   }

 

@@ -64,7 +64,7 @@ class IntegerInduction {
     ensures SumOfCubes(n) == Gauss(n) * Gauss(n);

   {

     if (n != 0) {

-      call Theorem2(n-1);

+      Theorem2(n-1);

 

       assert (forall m :: 0 <= m ==> 2 * Gauss(m) == m*(m+1));

     }

@@ -84,7 +84,7 @@ class IntegerInduction {
     ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n);

   {

     if (n != 0) {

-      call Theorem3(n-1);

+      Theorem3(n-1);

     }

   }

 

@@ -112,7 +112,7 @@ class IntegerInduction {
     if (*) {

       assert (forall m :: 0 <= m ==> SumOfCubes(m) == GaussWithPost(m) * GaussWithPost(m));

     } else {

-      call Theorem4();

+      Theorem4();

     }

   }

 

diff --git a/Test/dafny1/MatrixFun.dfy b/Test/dafny1/MatrixFun.dfy
index 86ad451d..81b3f4c9 100644
--- a/Test/dafny1/MatrixFun.dfy
+++ b/Test/dafny1/MatrixFun.dfy
@@ -64,20 +64,20 @@ method Main()
   B[0,0] := true;  B[0,1] := false;  B[0,2] := false;  B[0,3] := true;  B[0,4] := false;

   B[1,0] := true;  B[1,1] := true;   B[1,2] := true;   B[1,3] := true;  B[1,4] := false;

   print "Before:\n";

-  call PrintMatrix(B);

-  call MirrorImage(B);

+  PrintMatrix(B);

+  MirrorImage(B);

   print "Mirror image:\n";

-  call PrintMatrix(B);

+  PrintMatrix(B);

 

   var A := new int[3,3];

   A[0,0] := 5;  A[0,1] := 7;  A[0,2] := 9;

   A[1,0] := 6;  A[1,1] := 2;  A[1,2] := 3;

   A[2,0] := 7;  A[2,1] := 1;  A[2,2] := 0;

   print "Before:\n";

-  call PrintMatrix(A);

-  call Flip(A);

+  PrintMatrix(A);

+  Flip(A);

   print "Flip:\n";

-  call PrintMatrix(A);

+  PrintMatrix(A);

 }

 

 method PrintMatrix<T>(m: array2<T>)

diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy
index db1c60fa..6e19ab8f 100644
--- a/Test/dafny1/PriorityQueue.dfy
+++ b/Test/dafny1/PriorityQueue.dfy
@@ -41,7 +41,7 @@ class PriorityQueue {
   {

     n := n + 1;

     a[n] := x;

-    call SiftUp(n);

+    SiftUp(n);

   }

 

   method SiftUp(k: int)

@@ -76,7 +76,7 @@ class PriorityQueue {
     x := a[1];

     a[1] := a[n];

     n := n - 1;

-    call SiftDown(1);

+    SiftDown(1);

   }

 

   method SiftDown(k: int)

@@ -156,7 +156,7 @@ class PriorityQueue_Alternative {
   {

     n := n + 1;

     a[n] := x;

-    call SiftUp();

+    SiftUp();

   }

 

   method SiftUp()

@@ -189,7 +189,7 @@ class PriorityQueue_Alternative {
     x := a[1];

     a[1] := a[n];

     n := n - 1;

-    call SiftDown();

+    SiftDown();

   }

 

   method SiftDown()

diff --git a/Test/dafny1/Queue.dfy b/Test/dafny1/Queue.dfy
index 0ee953e1..bfb588be 100644
--- a/Test/dafny1/Queue.dfy
+++ b/Test/dafny1/Queue.dfy
@@ -48,9 +48,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()

@@ -62,9 +62,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);

   }

 

   method IsEmpty() returns (isEmpty: bool)

@@ -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/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index 33442219..95cdab89 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -26,7 +26,7 @@ class Main {
                 n.childrenVisited == old(n.childrenVisited) &&

                 n.children == old(n.children));

   {

-    call RecursiveMarkWorker(root, S, {});

+    RecursiveMarkWorker(root, S, {});

   }

 

   method RecursiveMarkWorker(root: Node, ghost S: set<Node>, ghost stackNodes: set<Node>)

@@ -67,7 +67,7 @@ class Main {
       {

         var c := root.children[i];

         if (c != null) {

-          call RecursiveMarkWorker(c, S, stackNodes + {root});

+          RecursiveMarkWorker(c, S, stackNodes + {root});

         }

         i := i + 1;

       }

diff --git a/Test/dafny1/SeparationLogicList.dfy b/Test/dafny1/SeparationLogicList.dfy
index 7828a54e..56a64bd6 100644
--- a/Test/dafny1/SeparationLogicList.dfy
+++ b/Test/dafny1/SeparationLogicList.dfy
@@ -28,7 +28,7 @@ class Node<T> {
       l.next := null;

       S := {l};

     } else {

-      call l, S := Cons(x, null, [], {});

+      l, S := Cons(x, null, [], {});

     }

   }

 

@@ -75,7 +75,7 @@ class ListNode<T> {
       l.Repr := {l};

       l.Contents := [x];

     } else {

-      call l := Cons(x, null);

+      l := Cons(x, null);

     }

   }

 

diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index 5cee5f6a..d3e0e82e 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -31,7 +31,7 @@ static ghost method Theorem(e: Expr, v: int, val: int)
     case Const(c) =>

     case Var(x) =>

     case Nary(op, args) =>

-      call Lemma(args, v, val);

+      Lemma(args, v, val);

   }

 }

 

@@ -41,8 +41,8 @@ static ghost method Lemma(l: List, v: int, val: int)
   match l {

     case Nil =>

     case Cons(e, tail) =>

-      call Theorem(e, v, val);

-      call Lemma(tail, v, val);

+      Theorem(e, v, val);

+      Lemma(tail, v, val);

   }

 }

 

@@ -80,11 +80,11 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int)
     case Var(x) =>

     case Nary(op, args) =>

       ghost var seArgs := SubstSeq(e, args, v, val);

-      call LemmaSeq(e, args, v, val);

+      LemmaSeq(e, args, v, val);

 

       ghost var se := Substitute(e, v, val);

       ghost var seArgs2 := SubstSeq(se, seArgs, v, val);

-      call LemmaSeq(se, seArgs, v, val);

+      LemmaSeq(se, seArgs, v, val);

 

       var N := |args|;

       var j := 0;

@@ -92,7 +92,7 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int)
         invariant j <= N;

         invariant (forall k :: 0 <= k && k < j ==> seArgs2[k] == seArgs[k]);

       {

-        call TheoremSeq(args[j], v, val);

+        TheoremSeq(args[j], v, val);

         j := j + 1;

       }

       assert seArgs == seArgs2;

@@ -107,6 +107,6 @@ static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>,
 {

   if (q == []) {

   } else {

-    call LemmaSeq(parent, q[..|q|-1], v, val);

+    LemmaSeq(parent, q[..|q|-1], v, val);

   }

 }

diff --git a/Test/dafny1/SumOfCubes.dfy b/Test/dafny1/SumOfCubes.dfy
index 2fecaee5..7ed7ce9b 100644
--- a/Test/dafny1/SumOfCubes.dfy
+++ b/Test/dafny1/SumOfCubes.dfy
@@ -10,19 +10,19 @@ class SumOfCubes {
     requires 0 <= n && n <= m;

     ensures r == SumEmUp(n, m);

   {

-    call a := SocuFromZero(m);

-    call b := SocuFromZero(n);

+    var a := SocuFromZero(m);

+    var b := SocuFromZero(n);

     r := a - b;

-    call Lemma0(n, m);

+    Lemma0(n, m);

   }

 

   static method SocuFromZero(k: int) returns (r: int)

     requires 0 <= k;

     ensures r == SumEmUp(0, k);

   {

-    call g := Gauss(k);

+    var g := Gauss(k);

     r := g * g;

-    call Lemma1(k);

+    Lemma1(k);

   }

 

   ghost static method Lemma0(n: int, m: int)

@@ -36,9 +36,9 @@ class SumOfCubes {
     {

       k := k + 1;

     }

-    call Lemma3(0, n);

-    call Lemma3(n, k);

-    call Lemma3(0, k);

+    Lemma3(0, n);

+    Lemma3(n, k);

+    Lemma3(0, k);

   }

 

   static function GSum(k: int): int

@@ -52,7 +52,7 @@ class SumOfCubes {
     ensures r == GSum(k);

   {

     r := k * (k - 1) / 2;

-    call Lemma2(k);

+    Lemma2(k);

   }

 

   ghost static method Lemma1(k: int)

@@ -64,10 +64,10 @@ class SumOfCubes {
       invariant i <= k;

       invariant SumEmDown(0, i) == GSum(i) * GSum(i);

     {

-      call Lemma2(i);

+      Lemma2(i);

       i := i + 1;

     }

-    call Lemma3(0, k);

+    Lemma3(0, k);

   }

 

   ghost static method Lemma2(k: int)

diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy
index 49f5a075..0aa36a10 100644
--- a/Test/dafny1/TerminationDemos.dfy
+++ b/Test/dafny1/TerminationDemos.dfy
@@ -58,10 +58,10 @@ class Ackermann {
     if (m == 0) {

       r := n + 1;

     } else if (n == 0) {

-      call r := ComputeAck(m - 1, 1);

+      r := ComputeAck(m - 1, 1);

     } else {

-      call s := ComputeAck(m, n - 1);

-      call r := ComputeAck(m - 1, s);

+      var s := ComputeAck(m, n - 1);

+      r := ComputeAck(m - 1, s);

     }

   }

 }

diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
index 61e86836..189ff2b5 100644
--- a/Test/dafny1/UltraFilter.dfy
+++ b/Test/dafny1/UltraFilter.dfy
@@ -22,9 +22,9 @@ class UltraFilter<G> {
   {

     if (M !in f) {

       // instantiate 'g' with the following 'h'

-      call h := H(f, S, M);

-      call Lemma_HIsFilter(h, f, S, M);

-      call Lemma_FHOrdering0(h, f, S, M);

+      var h := H(f, S, M);

+      Lemma_HIsFilter(h, f, S, M);

+      Lemma_FHOrdering0(h, f, S, M);

     }

   }

 

@@ -44,9 +44,9 @@ class UltraFilter<G> {
     // call Lemma_H1(h, f, S, M, *, *);

     assume (forall C, D :: C in h && D in h ==> C * D in h);

 

-    call Lemma_H2(h, f, S, M);

+    Lemma_H2(h, f, S, M);

 

-    call Lemma_H3(h, f, S, M);

+    Lemma_H3(h, f, S, M);

   }

 

   method Lemma_H0(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, A: set<G>, B: set<G>)

diff --git a/Test/dafny1/pow2.dfy b/Test/dafny1/pow2.dfy
index 52cddaac..c7e4bc63 100644
--- a/Test/dafny1/pow2.dfy
+++ b/Test/dafny1/pow2.dfy
@@ -36,7 +36,7 @@ ghost method Lemma(n: int)
   ensures pow2_slow(n) == Square(pow2_slow(n/2));

 {

   if (n != 0) {

-    call Lemma(n-2);

+    Lemma(n-2);

   }

 }

 

@@ -46,9 +46,9 @@ ghost method Theorem(n: int)
 {

   if (n == 0) {

   } else if (IsEven(n)) {

-    call Lemma(n);

-    call Theorem(n/2);

+    Lemma(n);

+    Theorem(n/2);

   } else {

-    call Theorem(n-1);

+    Theorem(n-1);

   }

 }