dtrebbien Apr 6, 2011 at 9:35 PM Reading through the 1-column formatted tutorial (v0.1, July 21, 2010), I think that there is a typo in the description of the owns set. On page 26, the tutorial states: ... After such operation, the container should own whatever it used to own minus x plus y. To facilitate such transfers VCC introduces the owns set. It is essentially the inverse of the owner field. It is defined on every object p and referred to as p->\owns. VCC maintains that: \forall \object p, q; p->\consistent ==> (q \in p->\owns <==> p->\owner == q) The operator <==> reads "if and only if", and is simply boolean equality (or implication both ways), with a binding priority lower than implication. That is, for consistent p, the set p->\owns contains exactly the objects owned by p. Shouldn't it be: \forall \object p, q; p->\consistent ==> (q \in p->\owns <==> q->\owner == p) ? Daniel MarkHillebrand Apr 6, 2011 at 10:19 PM Yes, that's right, good catch. I've fixed this in the repository... Best, Mark