DefaultSignalsOnlyClause

Default signals_only Clause

In the JML Reference Manual, the default for the signals_only clause was given as only consisting of the exceptions that a method declares in its header. On June 5, 2013, David Cok pointed out that this is pretty restrictive, and in particular would make many library functions incorrect (if they omit RuntimeExcpeption?, as premitted by the Java typing rules). He suggested that the default include java.lang.RuntimeException?, and argued that this would be consistent with the other defaults for JML specifications, which are as permissive as possible.

This was generally accepted, but still needs to be recorded in the JML Reference Manual.