Dafny: Added support for an initializing call as part of the new-allocation syntax. What you previously would have written like:

  c := new C;
  call c.Init(x, y);

you can now write as:

  c := new C.Init(x, y);

1 files changed, 2 insertions, 4 deletions

diff --git a/Test/dafny1/BinaryTree.dfy b/Test/dafny1/BinaryTree.dfy
index fbda3ecb..b4980d4b 100644
--- a/Test/dafny1/BinaryTree.dfy
+++ b/Test/dafny1/BinaryTree.dfy
@@ -58,8 +58,7 @@ class IntSet {
     decreases if n == null then {} else n.Repr;

   {

     if (n == null) {

-      m := new Node;

-      call m.Init(x);

+      m := new Node.Init(x);

     } else if (x == n.data) {

       m := n;

     } else {

@@ -224,8 +223,7 @@ class Node {
 class Main {

   method Client0(x: int)

   {

-    var s := new IntSet;

-    call s.Init();

+    var s := new IntSet.Init();

 

     call s.Insert(12);

     call s.Insert(24);