[e-lang] JSONSerializer review, further study of reviewable coding techniques
tyler.close at gmail.com
Mon Aug 18 18:18:07 CDT 2008
On Mon, Aug 18, 2008 at 2:41 PM, Tyler Close <tyler.close at gmail.com> 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.
More information about the e-lang