Initialize the length of an array whose element is class

[dreamqin68]

Hi All,

I have a question and hope to get help. Thanks.

class TestType
{
   var id: int
}

method test(element:TestType) returns(r: array<TestType>)
{
   r := new TestType[5];
}

In the above code, after verification shows Error: unless an initializer is provided for the array elements, a new array of 'TestType' must have empty size.

I don't know how to provide an initializer to the TestType.

[cpitclaudel]

You can initialize a fixed-length array with a sequence expression, like this:

  r := new TestType[5] [element, element, element, element, element];

For lengths not statically known, you can use a lambda (the parameter is the index:

r := new TestType[5](_ => element);

[dreamqin68]

Gotta, thank you!

[RustanLeino]

Section 20.16 of the reference manual gives the answer to this question.

The type TestType denotes non-null references to instances of class TestType. When you allocate a nonempty array of TestTypes, then these array elements need to be filled in somehow. In your case, since method test already takes a TestType argument, the easiest thing to do is to use this value to initial every element of the array. You can do that as follows:

r := new TestType[5](_ => element);

Alternatively, you can give the 5 elements explicitly, like this:

r := new TestType[5] [element, element, element, element, element];

(in which case you can change new TestType[5] to new TestType[], since Dafny will easily infer the 5 for you).

[dreamqin68]

Gotta, thank you!