This project is read-only.

Typo in the tutorial?

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)



Apr 6, 2011 at 10:19 PM

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

Best, Mark