#133 Jmlc doesn't execute model methods defined in refinements

[Gary T. Leavens]

This request is that an override of a model method in a
refinement file should allow that method to be executed.

See the example in
JML2/org/jmlspecs/jmlrac/testcase/bugs in the files
named ModelMethodRefinement.jml, which is refined by
ModelMethodRefinement.java.

This example shows a situation that is simplified from
that occuring in the digraph sample used in the
Preliminary Design Document for JML. In that example,
Digraph.jml is refined by Digraph.java. Digraph.jml had
a model method, unconnected(NodeType n) that was
used in preconditions of other methods. It could only be
implemented in the java file, because the
implementation needed to access the arcs
datastructure (or one would need to be able to access
model fields in model methods, which is also a current
request for enhancement). However, jmlc considers the
method to be not executable in this situation, as an
override in a refinement is apparently ignored, or not
used when compiling the .jml file.