Re: JSONSerializer review, further study of reviewable coding techniques

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.

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.

--Tyler