[e-lang] JSONSerializer review, further study of reviewable coding techniques
tyler.close at gmail.com
Mon Aug 18 18:30:09 CDT 2008
On Mon, Aug 18, 2008 at 4:18 PM, Tyler Close <tyler.close at gmail.com> wrote:
> 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.
Oops, nevermind, that correction won't work, since the code could just
assign the referent to an Immutable variable and then invoke any of
> 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
More information about the e-lang