JML: A notation for detailed design

JML is a behavioral interface specification language tailored to Java. It is designed to be written and read by working software engineers, and should require only modest mathematical training. It uses Eiffel-style syntax combined with model-based semantics, as in VDM and Larch. JML supports quantifiers, specification-only variables, and other enhancements that make it more expressive for specification than Eiffel and easier to use than VDM and Larch. JML [Leavens-Baker-Ruby01], which stands for “Java Modeling Language, ” is a behavioral interface specification language (BISL) [Wing87] designed to specify Java [Arnold-Gosling98] [Gosling-Joy-Steele96] modules. Java modules are classes and interfaces. A behavioral interface specification describes both the details of a module’s interface with clients, and its behavior from the client’s point of view. Such specifications are not good for the specification of whole programs, but are good for recording detailed design decisions or documentation of intended behavior, for a software module. The goal of this chapter is to explain JML and the concepts behind its approach t