PureMethodsCanBeHelperMethods

Pure Methods Can Be Helper Methods

In discussions on the jmlspecs-interest mailing list in May 2013, following the Shonan meeting, it was agreed that JML should allow pure methods to be helper methods. This has been recorded in the JML Reference Manual as only applying to methods (and not to constructors), but we may re-examine the issue of allowing pure constructors to be helpers if there are use-cases for that.

[Recorded in the JML Reference Manual]