SemanticsAndErrors

Semantics of Errors in JML

In the JML interest mailing list (June 19, 2013), Daniel Bruns raised the issue of the semantics of throwing an Error in JML. By this we mean an exception that is a subtype of java.lang.Error henceforth.

The current semantics (Sect. 9.6.2 of the Reference Manual) explicitly says that Errors are not considered in the semantics of JML. He points out that no JML compilers give warnings about when specifications mention Errors or explicitly throw Errors. Daniel suggested that Error be treated uniformly with all other types of exceptions.

Gary Leavens argued that "The reason JML treats Error specially is that these exceptions, besides the fact that they are not usually caught, can arise in very unexpected ways due to limits in the JVM. Thus they were deliberately ignored by the verification logic of Poetzsch-Heffter and Mueller. (JML's RACs also use subtypes of Error to signal detection of assertion violations.) if we made Error be treated the same as other exceptions, then every method would need to catch and handle Error in order to be provably correct. No library functions would correctly implement their specifications. This would make JML impractical."