
Reading through the 1column 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


Coordinator
Apr 6, 2011 at 9:19 PM

Yes, that's right, good catch. I've fixed this in the repository...
Best, Mark

