[e-lang] Prize and Milestone as mutable state idioms

[Tyler Close]

Wow, thanks for all the feedback!

I'm just going to cherry pick at it to start with...

On Wed, Jul 2, 2008 at 12:13 PM, David Wagner <daw at cs.berkeley.edu> wrote:
>  * I found it challenging to reconstruct how this class was supposed
>    to be used.  Perhaps an example calling sequence?

Monty reported this as well. I'm kind of stuck a bit here. Normally, I
try to provide such documentation for the public APIs intended to be
called by users of the library and don't for other classes. It's just
a workload issue. Problem is, in a security review, it's almost like
every class is public and needs to be well understood by the user
(security reviewer).

With the Prize and Milestone classes, I was working on a hypothesis
that it might be possible to standardize different coding idioms that
make it possible for a reviewer to understand code with much less
documentation. Like pushing the ideas embodied in the Joe-E verifier
further up the semantic stack. The Prize and Milestone classes are an
admittedly modest start in that direction, but that was the idea. Seem
plausible?

For the particular case of ValueWriter, it is, as you noted, a package
scope class, that is not directly available to user code. ValueWriter
is only used by the JSONSerializer, which itself is infrastructure
code that a user of the Waterken server never sees. I picked the
ValueWriter to try out this review concept since it has very few
dependencies and is implementing well-known functionality.

>    There is an alternative that may be easier to reason about but
>    may not meet your requirements.

To better understand the rationale for the ValueWriter API, take a
look at its only client, JSONSerializer. There are a lot more
dependencies here, so reviewing it is harder, but you might be able to
get a sense of why the ValueWriter API is the way it is. See:

http://waterken.svn.sourceforge.net/viewvc/waterken/server/trunk/waterken/remote/src/org/waterken/syntax/json/JSONSerializer.java?view=markup

The idea with ValueWriter, is that someone looking at JSONSerializer
can at least say that no matter what JSONSerializer does, at least it
is known that valid JSON comes out.

--Tyler