Tool Support
A variety of tools provide functionality based on JML annotations. The Iowa State JML tools provide an assertion checking compiler jmlc which converts JML annotations into runtime assertions, a documentation generator jmldoc which produces Javadoc documentation augmented with extra information from JML annotations, and a unit test generator jmlunit which generates JUnit test code from JML annotations.
Independent groups are working on tools that make use of JML annotations. These include:
- ESC/Java2, an extended static checker which uses JML annotations to perform more rigorous static checking than is otherwise possible;
- Daikon, a dynamic invariant generator;
- KeY, which provides a theorem prover with a JML front-end;
- Krakatoa, a static verification tool based on the Why verification platform and using the Coq proof assistant;
- JMLeclipse, a plugin for the Eclipse integrated development environment with support for JML syntax and interfaces to various tools that make use of JML annotations.
- Sireum/Kiasan, a symbolic execution based static analyzer which supports JML as a contract language.
- JMLUnit, a tool to generate files for running JUnit tests on JML annotated Java files.
- TACO, open source program analysis tool that statically checks the compliance of a Java program against its Java Modeling Language specification.
Read more about this topic: Java Modeling Language
Famous quotes containing the words tool and/or support:
“Is it not possible that an individual may be right and a government wrong? Are laws to be enforced simply because they were made? or declared by any number of men to be good, if they are not good? Is there any necessity for a man’s being a tool to perform a deed of which his better nature disapproves?”
—Henry David Thoreau (1817–1862)
“Well of all things in the world, I don’t suppose anything can be so dreadful as a public wedding—my stars!—I should never be able to support it!”
—Frances Burney (1752–1840)