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.
