JML: A Notation for Detailed Design

Authors	Gary T. Leavens; Albert L. Baker; Clyde Ruby
Editors
Type	incollection
Year	1999
Citekey	`leavens1999jml`

Published in	Behavioral Specifications of Businesses and Systems
Publisher	Springer US
Pages	175--188

DOI	10.1007/978-1-4615-5229-1_12
OpenAlex	W1583826417

Landing page	https://doi.org/10.1007/978-1-4615-5229-1_12

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.

How it got here	agent via openalex
Added	2026-08-04 00:00 UTC
Approved by	a person 2026-08-07 23:36 UTC

leavens verifying-real-java

@incollection{leavens1999jml,
  title        = {JML: A Notation for Detailed Design},
  author       = {Gary T. Leavens and Albert L. Baker and Clyde Ruby},
  year         = {1999},
  booktitle    = {Behavioral Specifications of Businesses and Systems},
  publisher    = {Springer US},
  pages        = {175--188},
  doi          = {10.1007/978-1-4615-5229-1_12},
}

This record lives at https://refs.drheap.org/leavens1999jml/ and will keep doing so.

JML: A Notation for Detailed Design

The work

Where it appeared

Identifiers

Access

Abstract

How it got here

Filed under

Cite it as