From 4f0a7156a61ae3d16b8f716a23ac3f3dd596ab86 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Sun, 27 Mar 2011 18:00:28 +0000
Subject: 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);
---
 Test/VSComp2010/Problem5-DoubleEndedQueue.dfy | 18 ++++++------------
 1 file changed, 6 insertions(+), 12 deletions(-)

(limited to 'Test/VSComp2010')

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);
     }
-- 
cgit v1.2.3