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

14 files changed, 94 insertions, 65 deletions

diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
index fdda243c..cf109c1a 100644
--- a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
+++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
@@ -30,12 +30,10 @@ class AmortizedQueue<T> {
     modifies this;

     ensures Valid() && List == [];

   {

-    var tmp := new LinkedList<T>;

+    var tmp := new LinkedList<T>.Init();

     front := tmp;

-    call front.Init();

-    tmp := new LinkedList<T>;

+    tmp := new LinkedList<T>.Init();

     rear := tmp;

-    call rear.Init();

     Repr := {this};

     Repr := Repr + front.Repr + rear.Repr;

     List := [];

@@ -54,8 +52,7 @@ class AmortizedQueue<T> {
       call ff := f.Concat(rr);

       front := ff;

 

-      var tmp := new LinkedList<T>;

-      call tmp.Init();

+      var tmp := new LinkedList<T>.Init();

       rear := tmp;

     }

     Repr := {this};

@@ -74,8 +71,7 @@ class AmortizedQueue<T> {
     requires Valid() && List != [];

     ensures r != null && r.Valid() && r.List == List[1..];

   {

-    r := new AmortizedQueue<T>;

-    call r.InitFromPieces(front.tail, rear);

+    r := new AmortizedQueue<T>.InitFromPieces(front.tail, rear);

   }

 

   method Enqueue(item: T) returns (r: AmortizedQueue<T>)

@@ -83,8 +79,7 @@ class AmortizedQueue<T> {
     ensures r != null && r.Valid() && r.List == List + [item];

   {

     call rr := rear.Cons(item);

-    var tmp := new AmortizedQueue<T>;

-    call tmp.InitFromPieces(front, rr);

+    var tmp := new AmortizedQueue<T>.InitFromPieces(front, rr);

     r := tmp;

   }

 }

@@ -158,8 +153,7 @@ class LinkedList<T> {
       r := this;

     } else {

       call r := tail.Reverse();

-      var e := new LinkedList<T>;

-      call e.Init();

+      var e := new LinkedList<T>.Init();

       call e := e.Cons(head);

       call r := r.Concat(e);

     }

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index bb88b265..3f30c4b5 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -54,8 +54,7 @@ class Benchmark3 {
     // the final Queue is a permutation of the input Queue

     ensures (forall i :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);

   {

-    r := new Queue<int>;

-    call r.Init();

+    r := new Queue<int>.Init();

     ghost var p := [];

     

     var n := 0;

diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy
index 94fe1eaa..d9bd36f5 100644
--- a/Test/VSI-Benchmarks/b5.dfy
+++ b/Test/VSI-Benchmarks/b5.dfy
@@ -31,8 +31,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;

@@ -53,8 +52,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/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy
index 9b244e69..13086f28 100644
--- a/Test/VSI-Benchmarks/b6.dfy
+++ b/Test/VSI-Benchmarks/b6.dfy
@@ -47,8 +47,7 @@ class Collection<T> {
     ensures fresh(iter.footprint) && iter.pos == -1;

     ensures iter.c == this;

   {

-      iter:= new Iterator<T>;

-      call iter.Init(this);

+      iter:= new Iterator<T>.Init(this);

   }

   

 }

@@ -107,8 +106,7 @@ class Client
 

   method Main()

   {

-    var c := new Collection<int>;

-    call c.Init();

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

     call c.Add(33);

     call c.Add(45);

     call c.Add(78);

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index a37f86e4..02c1a63a 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -47,10 +47,8 @@ class Glossary {
   {

     var rs:= new ReaderStream;

     call rs.Open();

-    var glossary := new Map<Word,seq<Word>>;

-    call glossary.Init();

-    var q:= new Queue<Word>;

-    call q.Init();

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

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

     

     while (true)

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

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 08570842..f57c6ead 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -79,7 +79,9 @@ TypeTests.dfy(64,6): Error: Duplicate local-variable name: z
 TypeTests.dfy(66,6): Error: Duplicate local-variable name: x

 TypeTests.dfy(69,8): Error: Duplicate local-variable name: x

 TypeTests.dfy(72,6): Error: Duplicate local-variable name: y

-14 resolution/type errors detected in TypeTests.dfy

+TypeTests.dfy(79,17): Error: member F in class C does not refer to a method

+TypeTests.dfy(80,17): Error: a method called as an initialization method must not have any result arguments

+16 resolution/type errors detected in TypeTests.dfy

 

 -------------------- SmallTests.dfy --------------------

 SmallTests.dfy(30,11): Error: index out of range

@@ -142,8 +144,14 @@ Execution trace:
     (0,0): anon6

     (0,0): anon14_Then

     (0,0): anon11

+SmallTests.dfy(272,24): Error BP5002: A precondition for this call might not hold.

+SmallTests.dfy(250,30): Related location: This is the precondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    SmallTests.dfy(267,19): anon3_Else

+    (0,0): anon2

 

-Dafny program verifier finished with 29 verified, 12 errors

+Dafny program verifier finished with 34 verified, 13 errors

 

 -------------------- Definedness.dfy --------------------

 Definedness.dfy(8,7): Error: possible division by zero

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 2eca82fd..a839d5a9 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -232,3 +232,43 @@ datatype Lindgren {
   Longstocking(seq<object>, Lindgren);

   HerrNilsson;

 }

+

+// --------------------------------------------------

+

+class InitCalls {

+  var z: int;

+  var p: InitCalls;

+

+  method Init(y: int)

+    modifies this;

+    ensures z == y;

+  {

+    z := y;

+  }

+

+  method InitFromReference(q: InitCalls)

+    requires q != null && 15 <= q.z;

+    modifies this;

+    ensures p == q;

+  {

+    p := q;

+  }

+

+  method TestDriver()

+  {

+    var c: InitCalls;

+    c := new InitCalls.Init(15);

+    var d := new InitCalls.Init(17);

+    var e: InitCalls := new InitCalls.Init(18);

+    var f: object := new InitCalls.Init(19);

+    assert c.z + d.z + e.z == 50;

+    // poor man's type cast:

+    ghost var g: InitCalls;

+    assert f == g ==> g.z == 19;

+

+    // test that the call is done before the assignment to the LHS

+    var r := c;

+    r := new InitCalls.InitFromReference(r);  // fine, since r.z==15

+    r := new InitCalls.InitFromReference(r);  // error, since r.z is unknown

+  }

+}

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 6e8e2b72..cbab53bf 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -72,3 +72,11 @@ method DuplicateVarName(x: int) returns (y: int)
   var y := y;  // error: redeclaration of an out-parameter is not allowed (it is

                // treated like an outermost-scoped local in this regard)

 }

+

+// ---------------------

+

+method InitCalls() {

+  var c := new C.F(null, null);  // error: F is not a method

+  var d := new C.M(8);  // error: M has out parameters

+  var e := new C.Caller();

+}

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;

diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy
index 87e63e2c..95ad12fa 100644
--- a/Test/vacid0/Composite.dfy
+++ b/Test/vacid0/Composite.dfy
@@ -135,18 +135,14 @@ class Composite {
 

 method Main()

 {

-  var c0 := new Composite;

-  call c0.Init(57);

+  var c0 := new Composite.Init(57);

 

-  var c1 := new Composite;

-  call c1.Init(12);

+  var c1 := new Composite.Init(12);

   call c0.Add({c0}, c1, {c1});

 

-  var c2 := new Composite;

-  call c2.Init(48);

+  var c2 := new Composite.Init(48);

 

-  var c3 := new Composite;

-  call c3.Init(48);

+  var c3 := new Composite.Init(48);

   call c2.Add({c2}, c3, {c3});

   call c0.Add({c0,c1}, c2, {c2,c3});

 

@@ -160,15 +156,15 @@ method Main()
 }

 

 method Harness() {

-  var a := new Composite;  call a.Init(5);

-  var b := new Composite;  call b.Init(7);

+  var a := new Composite.Init(5);

+  var b := new Composite.Init(7);

   call a.Add({a}, b, {b});

   assert a.sum == 12;

 

   call b.Update(17, {a,b});

   assert a.sum == 22;

 

-  var c := new Composite;  call c.Init(10);

+  var c := new Composite.Init(10);

   call b.Add({a,b}, c, {c});

   call b.Dislodge({a,b,c});

   assert b.sum == 27;