Groups allow to control ownership and invariants in structured types without changing the type definitions. Consider the following example:

struct S {
  int a;
  int b;
  int c;
};


Now assume that we want to control a and c independently from the other fields of struct S, attach an invariant to it etc.

For this, we can declare a group G in struct S and assign some fields of struct S to this group:

struct S {
  def_group(G)

  in_group(G) int a;
              int b;
  in_group(G) int c;

  inv_group(G, this->a == this->c)
};


Note how inv_group is used to attach an invariant to the group G.

To refer to the type of the group G, the scoped group operator (::) is available. So, for example, to express that a struct S owns its group G, we could add the following invariant to struct S:

invariant(set_in((struct S::G *)this, owns(this))


This group cast can be abbreviated by

invariant(set_in(this::G, owns(this))


With this invariant, the following code will verify as correct:

void foo(struct S *s)
  maintains(wrapped(s))
  maintains(wrapped(s::G))
  writes(s)
  writes(s::G)
{
  unwrap(s);
  s->b = 10; // legal without unwrapping G because b is not in the group
  unwrap(s::G);
  s->a = 5;
  s->c = 5;
  wrap(s::G);
  wrap(s);
}


Sometimes it might also be required to specify additional VCC attributes for a group. This additional arguments can directly be passed to the def_group() macro as a second argument. The following code generates a group G in the struct S with the vcc(claimable) attribute (cf. Claims).
struct S {
  def_group(G, vcc(claimable))

  in_group(G) int a;
              int b;
  in_group(G) int c;

  inv_group(G, this->a == this->c)
};

Last edited Nov 13, 2009 at 1:03 PM by stobies, version 3

Comments

georgefernendis Jun 28, 2010 at 3:46 PM 
I suppose as the latest VCC set up, one should use keeps(this::G) rather than set_in(this::G,owns(G)) which gives an error

holgerblasum Apr 15, 2010 at 12:04 PM 
When you simply paste together the first definition "struct S" that contains "def_group" and the definition "void foo" (and, of course, precede it by #include "vcc.h") you get a standalone working example.

Furthermore, note that "this invariant" in "With this invariant, the following code will verify as correct" refers to the *first* invariant in this text "inv_group(G, this->a == this->c)" and *not* to the second "invariant(set_in((struct S::G *)this, owns(this))". . (You'll get /smoke warnings when using the second invariant.)