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);

5 files changed, 13 insertions, 22 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);

diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy
index 810931be..b790eea5 100644
--- a/Test/dafny1/ExtensibleArray.dfy
+++ b/Test/dafny1/ExtensibleArray.dfy
@@ -90,8 +90,8 @@ class ExtensibleArray<T> {
       elements[length - M] := t;

     } else {

       if (more == null) {

-        var mr := new ExtensibleArray<array<T>>;  more := mr;

-        call mr.Init();

+        var mr := new ExtensibleArray<array<T>>.Init();

+        more := mr;

         Repr := Repr + {mr} + mr.Repr;

       }

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

@@ -108,8 +108,7 @@ class ExtensibleArray<T> {
 }

 

 method Main() {

-  var a := new ExtensibleArray<int>;

-  call a.Init();

+  var a := new ExtensibleArray<int>.Init();

   var n := 0;

   while (n < 256*256+600)

     invariant a.Valid() && fresh(a.Repr);

diff --git a/Test/dafny1/ListCopy.dfy b/Test/dafny1/ListCopy.dfy
index 52f5cf76..d5febfe0 100644
--- a/Test/dafny1/ListCopy.dfy
+++ b/Test/dafny1/ListCopy.dfy
@@ -19,8 +19,7 @@ class Node {
     var newRegion: set<Node> := {};

 

     if (oldListPtr != null) {

-      newRoot := new Node;

-      call newRoot.Init();

+      newRoot := new Node.Init();

       newRegion := newRegion + {newRoot};

       var prev := newRoot;

 

@@ -33,8 +32,7 @@ class Node {
         invariant newRegion !! existingRegion;

         decreases *;  // omit loop termination check

       {

-        var tmp := new Node;

-        call tmp.Init();

+        var tmp := new Node.Init();

 

         newRegion := newRegion + {tmp};

         prev.nxt := tmp;

diff --git a/Test/dafny1/Queue.dfy b/Test/dafny1/Queue.dfy
index 42b7dd64..0ee953e1 100644
--- a/Test/dafny1/Queue.dfy
+++ b/Test/dafny1/Queue.dfy
@@ -33,8 +33,7 @@ class Queue<T> {
     ensures Valid() && fresh(footprint - {this});

     ensures |contents| == 0;

   {

-    var n := new Node<T>;

-    call n.Init();

+    var n := new Node<T>.Init();

     head := n;

     tail := n;

     contents := n.tailContents;

@@ -81,8 +80,8 @@ class Queue<T> {
     ensures Valid() && fresh(footprint - old(footprint));

     ensures contents == old(contents) + [t];

   {

-    var n := new Node<T>;

-    call n.Init();  n.data := t;

+    var n := new Node<T>.Init();

+    n.data := t;

     tail.next := n;

     tail := n;

 

@@ -150,10 +149,8 @@ class Node<T> {
 class Main<U> {

   method A<T>(t: T, u: T, v: T)

   {

-    var q0 := new Queue<T>;

-    call q0.Init();

-    var q1 := new Queue<T>;

-    call q1.Init();

+    var q0 := new Queue<T>.Init();

+    var q1 := new Queue<T>.Init();

 

     call q0.Enqueue(t);

     call q0.Enqueue(u);

diff --git a/Test/dafny1/UnboundedStack.dfy b/Test/dafny1/UnboundedStack.dfy
index 4c3b095a..940e1a0a 100644
--- a/Test/dafny1/UnboundedStack.dfy
+++ b/Test/dafny1/UnboundedStack.dfy
@@ -31,8 +31,7 @@ class UnboundedStack<T> {
     ensures IsUnboundedStack();

     ensures content == [val] + old(content);

   {

-    var tmp := new Node<T>;

-    call tmp.InitNode(val,top);

+    var tmp := new Node<T>.InitNode(val,top);

     top := tmp;

     representation := representation + top.footprint;

     content := [val] + content;