What is the case against a struct post-blit default constructor?

[Timon Gehr]

On 10/10/2012 01:59 PM, Don Clugston wrote:
> On 10/10/12 13:27, Timon Gehr wrote:
>> On 10/10/2012 12:45 PM, Don Clugston wrote:
>>> ...
>>> Really, there does not seem to me to be any point in having an invariant
>>> for a struct, without a default constructor.
>>>
>>
>> One can use a dented invariant.
>>
>> struct S{
>>      bool valid = false;
>>      // ...
>>      invariant(){ if(valid) assert(...); }
>>      void establishInvariant()out{assert(valid);}body{...}
>> }
>
> Yes, you have to do something like that. It's absolute garbage. When you
> have a hack like that, I don't see the point of having invariants in the
> language.
> ...

Well, all invariants in Spec# follow this pattern. Every object has an
implicit boolean 'valid' field.