JML. 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, an open source program analysis tool that statically checks the compliance of a Java program against its Java Modeling Language specification. References Gary T. Leavens and Yoonsik Cheon. Design by Contract with JML; Draft tutorial. Gary T. Leavens, 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, Kluwer, 1999, chapter 12, pages 175-188. Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, and Daniel M. Zimmerman. JML Reference Manual (DRAFT), September 2009. HTML Marieke Huisman, Wolfgang Ahrendt, Daniel Bruns, and Martin Hentschel. Formal specification with JML. 2014. download (CC-BY-NC-ND) External links JML website Java platform Formal specification languages Articles with example Java code