Spec#, nullables and more

[bearophile]

Andrei Alexandrescu:

> To find an array that always has initialized data, look no further than 
> std::vector. There is no way to grow an std::vector without filling it 
> with data under user's control. The only place where std::vector assumes 
> a default is the resize function:
> 
> void vector<T>::resize(size_type newSize, T filler = T());
> 
> If that default went away, the user would always be required to provide 
> a filler when growing the vector.

In D the array append is not an efficient operation, and in general it's not handy to limit to just that the ways to create an array of nonnullables. In another post I have shown how Spec# solves this problem (using a statement to divide the array building phase from the phase where you may read the array items).

Bye,
bearophile