Lambda the Ultimate

inactiveTopic Getting started with JML
started 3/20/2003; 2:31:48 PM - last post 3/21/2003; 2:18:05 PM
Ehud Lamm - Getting started with JML  blueArrow
3/20/2003; 2:31:48 PM (reads: 1440, responses: 3)
Getting started with JML
JML introduces a number of constructs for declaratively describing behavior. These include model fields, quantifiers, visibility scoping for assertions, preconditions, postconditions, invariants, contract inheritance, and specifications of normal versus exceptional behavior.

JML (The Java Modeling Language) seems like an interesting notation, but I didn't manage to find detailed information on what tools are currently available (heck, I can invent notations myself, surely having a new notation is not the point).


Posted to Software-Eng by Ehud Lamm on 3/20/03; 2:33:41 PM

Some One - Re: Getting started with JML  blueArrow
3/20/2003; 4:10:23 PM (reads: 598, responses: 0)
The sourceforge project has the implementation available here

Vladimir Ivanovic - Re: Getting started with JML  blueArrow
3/20/2003; 4:25:57 PM (reads: 595, responses: 0)
Gauss once complained of another mathematician that he needed less notation and more notions.

Karl Zilles - Re: Getting started with JML  blueArrow
3/21/2003; 2:18:05 PM (reads: 480, responses: 0)
With regard to tools:

You can use the open source JML compiler to generate class files that automatically check your JML specifications at runtime. If a program doesn't do what its JML annotations say it should, JML will throw an unchecked exception indicating which part of the specification was violated. This is useful both for catching bugs and for helping to keep the documentation (in the form of JML annotations) in sync with the code.

The JML runtime assertion checking compiler is the first of a growing number of tools that work with JML. Others include jmldoc and jmlunit. jmldoc is similar to javadoc but it also includes JML specifications in the generated HTML documentation. jmlunit generates the skeleton of a test-case class that allows JML to be conveniently used in conjunction with JUnit. You'll find a reference for these and other tools in Resources.