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:
“The veto is a President’s Constitutional right, given to him by the drafters of the Constitution because they wanted it as a check against irresponsible Congressional action. The veto forces Congress to take another look at legislation that has been passed. I think this is a responsible tool for a president of the United States, and I have sought to use it responsibly.”
—Gerald R. Ford (b. 1913)
“Children learn to care by experiencing good care. They come to know the blessings of gentleness, or sympathy, of patience and kindness, of support and backing first through the way in which they themselves are treated.”
—James L. Hymes, Jr. (20th century)