Re: Static Initializer in Joe-E

Mohsen Vakilian  wrote:
> I believe Joe-E should disallow calls to static methods in static
> initializers for the same reason that it forbids calls to instance methods
> in constructors.
> The following is an example of what can go wrong if you let static
> initializers invoke static methods. In this example, method m, which is
> verified  to be pure by Joe-E, returns two different results given the same
> input (m takes no inputs).  [... example elided ...]

Thanks, Mohsen.  I agree: this is a design defect in Joe-E, as Joe-E is
currently specified and implemented.

This is an instance of a known bug that's slightly more general in
nature: Joe-E does not prevent access to static final fields before
they are initialized.  This is one of a small number of known sources of
unsoundness in the purity/immutability checks of Joe-E.  There are a few
others of lesser importance, which you can find on the Joe-E bug tracker
(e.g., non-strictfp floating point, asserts).

The issue with static final fields is technically documented, although
admittedly in a fairly obscure way.  The Joe-E language spec says: "This
specification currently does not prevent the reading of an uninitialized
value for a static final field; this protection may be provided in the
future."  And a related issue is documented in Issue #10 on the Joe-E
bug tracker:
  http://code.google.com/p/joe-e/issues/detail?id=10
although the code example is a bit different.

I believe at one point Adrian worked out a set of checks that could
plausibly be applied to close the soundness hole with static final
(particularly with cyclic dependencies in class loading), but they were
fairly intricate and we deemed it a low priority, so they never got
implemented and we never paid much attention to this issue.  I don't
think they are written down anywhere, either.

Unfortunately there are currently no plans to fix this defect (we don't
have the resources to do it).  Sorry. :-(

Anyway, I don't want to downplay the severity of the issue.  It's clearly
a defect.  And I do appreciate that you took the time to report this
issue.  I've filed it in the Joe-E bug tracker so that we can track it.
  http://code.google.com/p/joe-e/issues/detail?id=17
Thanks again.