Aggregate classes

Jan 13, 2011 at 11:17 AM


I have

  • a class A,
  • a class B that contains an object a of type A as member,
  • a method m of class B that modifies a.

The frame conditions I have for m are


which seem to have the desired effect. Is this the "write" way to do it? Is it necessary to specify ownership, as with [Rep] in Spec#?

On the other hand,


doesn't verify. It seems that wrapped(&This) doesn't imply wrapped(&This->B) and correspondingly for writes, which looks counterintuitive to me. I'd expected that the properties of This include the transitive closure of its members. Please explain.


Jan 13, 2011 at 2:45 PM

B can contain an A but still not own it. Ownership has to be made explicit in object invariants. So, if you add invariant(keeps(&a_field)) to B, then VCC can deduce wrapped(&this->a_field) from wrapped(this) .