Support default (which, here, means nameless) class-instance constructors

5 files changed, 93 insertions, 48 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 63b4ffce..370e3c38 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -494,6 +494,7 @@ Execution trace:
 Dafny program verifier finished with 3 verified, 4 errors

 

 -------------------- ResolutionErrors.dfy --------------------

+ResolutionErrors.dfy(396,2): Error: More than one default constructor

 ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(110,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

@@ -511,6 +512,10 @@ ResolutionErrors.dfy(217,12): Error: ghost-context break statement is not allowe
 ResolutionErrors.dfy(229,12): Error: trying to break out of more loop levels than there are enclosing loops

 ResolutionErrors.dfy(233,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

 ResolutionErrors.dfy(238,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)

+ResolutionErrors.dfy(402,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called

+ResolutionErrors.dfy(407,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

+ResolutionErrors.dfy(408,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

+ResolutionErrors.dfy(410,9): Error: class Lamb does not have a default constructor

 ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops

 ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)

 ResolutionErrors.dfy(23,12): Error: sequence/array/map selection requires a sequence, array or map (got array3<T>)

@@ -542,16 +547,16 @@ ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specificat
 ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(343,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)

 ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)

-ResolutionErrors.dfy(363,4): Error: arguments to + must be int or a collection type (instead got bool)

-ResolutionErrors.dfy(368,4): Error: all lines in a calculation must have the same type (got int after bool)

-ResolutionErrors.dfy(371,4): Error: first argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(371,4): Error: second argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(372,8): Error: first argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(372,8): Error: second argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(377,8): Error: first argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(377,8): Error: second argument to ==> must be of type bool (instead got int)

-ResolutionErrors.dfy(382,4): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-57 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(363,6): Error: arguments to + must be int or a collection type (instead got bool)

+ResolutionErrors.dfy(368,6): Error: all lines in a calculation must have the same type (got int after bool)

+ResolutionErrors.dfy(371,6): Error: first argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(371,6): Error: second argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(372,10): Error: first argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(372,10): Error: second argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(377,10): Error: first argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(377,10): Error: second argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(382,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+62 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

diff --git a/Test/dafny0/IteratorResolution.dfy b/Test/dafny0/IteratorResolution.dfy
index 60b1bc7e..004bc85e 100644
--- a/Test/dafny0/IteratorResolution.dfy
+++ b/Test/dafny0/IteratorResolution.dfy
@@ -13,7 +13,7 @@ module Mx {
   }

 

   method IteratorUser() {

-    var iter := new ExampleIterator.ExampleIterator(15);

+    var iter := new ExampleIterator(15);

     iter.k := 12;  // error: not allowed to assign to iterator's in-parameters

     iter.x := 12;  // allowed (but this destroys the validity of 'iter'

     iter.xs := [];  // error: not allowed to assign to iterator's yield-history variables

@@ -41,7 +41,7 @@ module Mx {
   class Client {

     method M() {

       var m := StaticM(5);

-      var it := new ExampleIterator.ExampleIterator(100);

+      var it := new ExampleIterator(100);

       var a, b := Worker(it);

     }

     method Worker(xi: ExampleIterator) returns (k: int, m: int) {

@@ -58,17 +58,17 @@ module Mx {
     {

       g0.t := true;  // error: not allowed to assign to .t

       g0.u := true;  // allowed (but this destroys the validity of 'iter'

-      var g1 := new GenericIterator.GenericIterator(20);

+      var g1 := new GenericIterator(20);

       assert g1.u < 200;  // .u is an integer

 

       assert g2.u == 200;  // error: the type parameter of g2 is unknown

 

-      var h0 := new GenericIteratorResult.GenericIteratorResult();

+      var h0 := new GenericIteratorResult._ctor();

       // so far, the instantiated type of h0 is unknown

       var k := h0.t;

       assert k < 87;

 

-      var h1 := new GenericIteratorResult.GenericIteratorResult();

+      var h1 := new GenericIteratorResult();

       // so far, the instantiated type of h1 is unknown

       if (*) {

         var b: bool := h1.t;  // this determines h1 to be of type GenericIteratorResult<bool>

@@ -78,7 +78,7 @@ module Mx {
 

       var h2 := new GenericIteratorResult;  // error: constructor is not mentioned

 

-      var h3 := new GenericIterator.GenericIterator(30);

+      var h3 := new GenericIterator._ctor(30);

       if (h3.t == h3.u) {

         assert !h3.t;  // error: type mismatch

       }

diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy
index c6a0488b..43ef4e69 100644
--- a/Test/dafny0/Iterators.dfy
+++ b/Test/dafny0/Iterators.dfy
@@ -24,7 +24,7 @@ iterator Naturals(u: int) yields (n: nat)
 }

 

 method Main() {

-  var m := new MyIter.MyIter(12);

+  var m := new MyIter(12);

   assert m.ys == m.xs == [];

   var a := m.x;

   if (a <= 13) {

@@ -37,7 +37,7 @@ method Main() {
     mer := m.MoveNext();  // error

   }

 

-  var n := new MyIntIter.MyIntIter();

+  var n := new MyIntIter();

   var patience := 10;

   while (patience != 0)

     invariant n.Valid() && fresh(n._new);

@@ -48,7 +48,7 @@ method Main() {
     patience := patience - 1;

   }

 

-  var o := new Naturals.Naturals(18);

+  var o := new Naturals(18);

   var remaining := 100;

   while (remaining != 0)

     invariant o.Valid() && fresh(o._new);

@@ -80,7 +80,7 @@ iterator IterA(c: Cell)
 method TestIterA()

 {

   var c := new Cell;

-  var iter := new IterA.IterA(c);

+  var iter := new IterA(c);

   var tmp := c.data;

   var more := iter.MoveNext();

   assert tmp == c.data;  // error

@@ -107,7 +107,7 @@ iterator IterB(c: Cell)
 method TestIterB()

 {

   var c := new Cell;

-  var iter := new IterB.IterB(c);

+  var iter := new IterB(c);

   var tmp := c.data;

   var more := iter.MoveNext();

   if (more) {

@@ -138,7 +138,7 @@ iterator IterC(c: Cell)
 method TestIterC()

 {

   var c := new Cell;

-  var iter := new IterC.IterC(c);

+  var iter := new IterC(c);

   var tmp := c.data;

   var more := iter.MoveNext();

   if (more) {

@@ -147,7 +147,7 @@ method TestIterC()
     assert tmp == c.data;  // error: the postcondition says nothing about this

   }

 

-  iter := new IterC.IterC(c);

+  iter := new IterC(c);

   c.data := 17;

   more := iter.MoveNext();  // error: iter.Valid() may not hold

 }

@@ -217,7 +217,7 @@ iterator DoleOutReferences(u: Cell) yields (r: Cell, c: Cell)
 

 method ClientOfNewReferences()

 {

-  var m := new DoleOutReferences.DoleOutReferences(null);

+  var m := new DoleOutReferences(null);

   var i := 86;

   while (i != 0)

     invariant m.Valid() && fresh(m._new);

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index c615c5ec..7c919b2a 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -359,27 +359,67 @@ method MG1(l: GList, n: nat)
 

 method TestCalc(m: int, n: int, a: bool, b: bool)

 {

-	calc {

-		a + b; // error: invalid line

-		n + m;

-	}

-	calc {

-		a && b;

-		n + m; // error: all lines must have the same type

-	}

-	calc ==> {

-		n + m; // error: ==> operator requires boolean lines

-		n + m + 1;

-		n + m + 2;

-	}		

-	calc {

-		n + m;

-		n + m + 1;

-		==> n + m + 2; // error: ==> operator requires boolean lines

-	}

-	calc {

-		n + m;

-		{ print n + m; } // error: non-ghost statements are not allowed in hints

-		m + n;

-	}			

+  calc {

+    a + b; // error: invalid line

+    n + m;

+  }

+  calc {

+    a && b;

+    n + m; // error: all lines must have the same type

+  }

+  calc ==> {

+    n + m; // error: ==> operator requires boolean lines

+    n + m + 1;

+    n + m + 2;

+  }    

+  calc {

+    n + m;

+    n + m + 1;

+    ==> n + m + 2; // error: ==> operator requires boolean lines

+  }

+  calc {

+    n + m;

+    { print n + m; } // error: non-ghost statements are not allowed in hints

+    m + n;

+  }

+}

+

+// ------------------- nameless constructors ------------------------------

+

+class YHWH {

+  var data: int;

+  constructor (x: int)

+    modifies this;

+  {

+    data := x;

+  }

+  constructor (y: bool)  // error: duplicate constructor name

+  {

+  }

+  method Test() {

+    var IAmWhoIAm := new YHWH(5);

+    IAmWhoIAm := new YHWH._ctor(7);  // but, in fact, it is also possible to use the underlying name

+    IAmWhoIAm := new YHWH;  // error: the class has a constructor, so one must be used

+    var s := new Lucifer.Init(5);

+    s := new Lucifer.FromArray(null);

+    s := new Lucifer(false);

+    s := new Lucifer._ctor(false);

+    s := new Lucifer.M();  // error: there is a constructor, so one must be called

+    s := new Lucifer;  // error: there is a constructor, so one must be called

+    var l := new Lamb;

+    l := new Lamb();  // error: there is no default constructor

+    l := new Lamb.Gwen();

+  }

+}

+

+class Lucifer {

+  constructor Init(y: int) { }

+  constructor (nameless: bool) { }

+  constructor FromArray(a: array<int>) { }

+  method M() { }

+}

+

+class Lamb {

+  method Jesus() { }

+  method Gwen() { }

 }

diff --git a/Test/dafny3/Iter.dfy b/Test/dafny3/Iter.dfy
index 543a889a..3af868ca 100644
--- a/Test/dafny3/Iter.dfy
+++ b/Test/dafny3/Iter.dfy
@@ -73,7 +73,7 @@ method Client<T(==)>(l: List, stop: T) returns (s: seq<T>)
   requires l != null && l.Valid();

 {

   var c := new Cell;

-  var iter := new M.M(l, c);

+  var iter := new M(l, c);

   s := [];

   while (true)

     invariant iter.Valid() && fresh(iter._new);