Re: JSONSerializer review, further study of reviewable coding techniques

On Mon, Aug 18, 2008 at 4:18 PM, Tyler Close <[email protected]> wrote:
> On Mon, Aug 18, 2008 at 2:41 PM, Tyler Close <[email protected]> wrote:
>> Let's assume the existence of a variable annotation: "@inert". For
>> variables with this annotation, the Joe-E verifier checks that:
>> 1. On access to a field of the referent, the field MUST be final and
>> the accessed value MUST be assigned to another variable that either:
>>    a. has the @inert annotation,
>>    b. or is of type Immutable.
>> 2. On invocation of a method of the referent, the referent MUST be Immutable.
>
> That last one should be tightened up to:
> 2. On invocation of a method of the referent, the invocation MUST be pure.

Oops, nevermind, that correction won't work, since the code could just
assign the referent to an Immutable variable and then invoke any of
its methods.

> For example, this constraint guarantees that JSONSerializer.write()
> can't pass the export argument to a referent obtained from the values
> argument, thus enabling that referent to stash a memory.

Knowing that the Exporter doesn't provide a memory to any of the
values will have to be dependent on knowing that the Exporter is
deterministic.

--Tyler