Re: A broken brand?

Toby,

    Trying to have more testable and unambiguous statements of 
requirement...

> Actually, more simply, that should be:
> 
> "An object that does not possess both u and a proxy to b, or b 
> itself, cannot have c returned to it by u."

    This is a constraint on u and should be stated that way...

    "u shall return the c iff an invoking object o satisfies the 
    following preconditions:
    a) o invokes u using a valid capability, and
    b) the message from o invoking u provides a valid capability 
       to either b or a proxy to b"
> 
> This is nicer because it requires fewer assumptions about the other
> objects in the system in order to test (e.g. that they won't pass an
> object c etc.).
> 
> > We define an object p to be a "proxy to object o", if: p is 
> > not an unsealer and p can call o in response to an invocation, 
> > or p can call a proxy to o in response to an invocation.
> 
> Boxes are also not proxies by definition.

    I think that the "if:" in the definition for "proxy" should be
an "iff:", since in all cases that I can think of both conditions 
must be satisfied.

    Happy modeling,

-DMC