Aggregate classes

Jan 13, 2011 at 11:17 AM

Hello,

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

maintains(wrapped(&This->B))
writes(&This->B)

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,

maintains(wrapped(&This))
writes(&This)

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.

Boris

Coordinator
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) .