JML(ID:3510/jml001)

Interface specification language for JAVA 

JAVA Modelling Language - Computer Science, Iowa State University

The Java Modeling Language (JML) is a behavioral interface specification language that can be used to specify the behavior of Java modules. It combines the approaches of Eiffel and Larch, with some elements of the refinement calculus.


Related languages
Java => JML   Formalising in
References:
  • Leavens, Gary T. ; Albert L. Baker, and Clyde Ruby. Preliminary Design of JML: A Behavioral Interface Specification Language for Java. Department of Computer Science, Iowa State University, TR #98-06q, June 1998, revised July, November 1998, January, April, June, July, August, December 1999, February, May, July, December 2000, February, April, May, August 2001, June 2002 view details Abstract: JML is a behavioral interface specification language tailored to Java.
    It also allows assertions to be intermixed with Java code, as an aid to verification and debugging.  JML is designed to be used by working
    software engineers; to do this it follows Eiffel in using Java
    expressions in assertions.  JML combines this idea from Eiffel with the model-based approach to specifications, typified by VDM and Larch,
    which results in greater expressiveness.  Other expressiveness
    advantages over Eiffel include quantifiers, specification-only
    variables, and frame conditions.

    This paper discusses the goals of JML, the overall approach, and
    describes the basic features of the language through examples. It is
    intended for readers who have some familiarity with both Java and
    behavioral specification using pre- and postconditions.
    pdf
  • Leavens, Gary T. ; Albert L. Baker, and Clyde Ruby. JML: A Notation for Detailed Design. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds (editors), Behavioral Specifications of Businesses and Systems, chapter 12, pages 175-188. Copyright Kluwer, 1999. view details pdf
  • Leavens, Gary T. ; K. Rustan M. Leino, Erik Poll, Clyde Ruby, and Bart Jacobs. JML: notations and tools supporting detailed design in Java view details pdf Abstract: JML is a notation for specifying the detailed design of Java classes
    and interfaces.  JML's assertions are stated using a slight extension
    of Java's expression syntax.  This should make it easy to use.  Tools
    for JML aid in static analysis, verification, and run-time debugging
    of Java code.

          in OOPSLA '00 Companion, Minneapolis, Minnesota, August 2000 view details
  • Arun D. Raghavan and Gary T. Leavens. Desugaring JML Method Specifications. Department of Computer Science, Iowa State University, TR #00-03c, March 2000, revised July, December 2000, August 2001 view details Abstract: JML, which stands for "Java Modeling Language,'' is a behavioral
    interface specification language (BISL) designed to specify Java
    modules.  JML features a great deal of syntactic sugar that is
    designed to make specifications more expressive.  This paper presents
    a desugaring process that boils down all of the syntactic sugars in
    JML into a much simpler form.  This desugaring will help one
    manipulate JML specifications in tools, understand the meaning of
    these sugars, and it also allows the use of JML specifications in
    program verification. pdf
          in OOPSLA '00 Companion, Minneapolis, Minnesota, August 2000 view details
    Resources