As agreed in the jmlspecs-interest group, we have
added to the parser and type checker a new "code"
modifier. Specification cases with the "code"
modifier are not to be inherited by subtypes. This
is documented in the reference manual.
One problem that remains before we can make a real
release with this feature is that it's properly
impmented in the jmlc tool. (Another is implementing
it in the jmldoc tool.) It should be a matter of
checking that a specification case has the "code"
modifier before doing inheritance, and not doing
inheritance in that case.
Logged In: YES
user_id=633675
See also Feature Request 1307501.