Skip to content

Commit cfe0778

Browse files
authored
Remove use of _ctor (#1091)
Internally, the name of an anonymous class (or iterator) constructor is `_ctor`. Although this name can be used, it is not intended to be used in programs (not only is it uglier and more cryptic in the program text, but this internal name may also change to something else in the future). Thus, it also seems appropriate not to use this name in the test suite.
1 parent c4a0c3f commit cfe0778

File tree

3 files changed

+5
-5
lines changed

3 files changed

+5
-5
lines changed

Test/dafny0/IteratorResolution.dfy

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ module Mx {
6868

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

71-
var h0 := new GenericIteratorResult._ctor();
71+
var h0 := new GenericIteratorResult();
7272
// so far, the instantiated type of h0 is unknown
7373
var k := h0.t;
7474
assert k < 87;
@@ -83,7 +83,7 @@ module Mx {
8383

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

86-
var h3 := new GenericIterator._ctor(30); // see two lines down
86+
var h3 := new GenericIterator(30); // see two lines down
8787
if h3.t == h3.u {
8888
assert !h3.t; // error: type mismatch (here or two lines ago)
8989
}

Test/dafny0/IteratorResolution.dfy.expect

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
IteratorResolution.dfy(64,9): Error: LHS of assignment must denote a mutable field
22
IteratorResolution.dfy(84,13): Error: when allocating an object of type 'GenericIteratorResult', one of its constructor methods must be called
33
IteratorResolution.dfy(69,18): Error: arguments must have comparable types (got _T0 and int)
4-
IteratorResolution.dfy(86,36): Error: incorrect type of method in-parameter (expected bool, got int)
4+
IteratorResolution.dfy(86,16): Error: incorrect type of method in-parameter (expected bool, got int)
55
IteratorResolution.dfy(81,19): Error: RHS (of type bool) not assignable to LHS (of type int)
66
IteratorResolution.dfy(22,9): Error: LHS of assignment must denote a mutable field
77
IteratorResolution.dfy(24,9): Error: LHS of assignment must denote a mutable field

Test/dafny0/ResolutionErrors.dfy

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -481,12 +481,12 @@ module MiscAgain {
481481
}
482482
method Test() {
483483
var i := new Y(5);
484-
i := new Y._ctor(7); // but, in fact, it is also possible to use the underlying name
484+
i := new Y(7);
485485
i := new Y; // error: the class has a constructor, so one must be used
486486
var s := new Luci.Init(5);
487487
s := new Luci.FromArray(null);
488488
s := new Luci(false);
489-
s := new Luci._ctor(false);
489+
s := new Luci(true);
490490
s := new Luci.M(); // error: there is a constructor, so one must be called
491491
s := new Luci; // error: there is a constructor, so one must be called
492492
var l := new Lamb;

0 commit comments

Comments
 (0)