4.1.2 Modifiers for Type Definitions

BML allows one to declare a class or interface as pure. The semantics of this annotation is the same as its semantics in JML, described in Section 6.1.2 of JML Reference Manual, i.e., a class or interface is annotated with pure as an abbreviation to specify that all its constructors and instance methods are pure.

[JMLObject-library does not use model types. It uses a few model methods. It uses pure types. Therefore, pure only class modifier in BML.]