I feel like "unspecified" still sounds too lax. How about "implementation-defined"?
I'm thinking of scenarios like: "When this occurs, The Java Virtual Machine implementation may choose to either X or Y. If it does Y, then it shall throw a Z exception."
Can you add a source link? I would be interested in looking it up.
It is one of the few languages that has denotational semantics as part of the language definition.
It was also one of the first languages to fix the null reference problem (called Void-safety in Eiffel speak).
Had the compilers been a bit cheaper instead of targeted to the enterprise customers, maybe many more would be enjoying writing safe native compiled software on Eiffel.