⁵Currently this is mainly a feature to avoid repetition in method specifications; it is e.g. not yet checked whether a helper method is private as would be required for a true modular reasoning about objects.