Links to Related Web Pages
- The github OpenJML project.
- The AspectJML project, that is both an aspect-oriented extension to Java and a runtime assertion checking tool for JML.
- The Daikon invariant detector project from the University of Washington's Programming Languages and Software Engineering Group.
- The ChAsE tool for statically checking the modifiable/assignable clauses in the ESC/Java subset of JML specifications, by Néstor Cataño Collazos.
- Java Applet Correctness Kit which is an industrial use of JML.
- The KeY Project, project that aims to "integrate formal software specification and verification into the industrial software engineering processes". They also have a JML front end.
- Commands to use the syntax highlighting feature of VIM for JML specifications by Engelbert Hubbers from Nijmegen
- Jutil.org which is a "high-quality API for general utility code" specified using JML.
- The Bytecode Modeling Language (BML) a variant of JML at the bytecode level.
- Modern Jass (Java with assertions), which supports design by contract for Java. This supercedes the older version of Jass, and is more closely related to JML.
- jContractor, an open-source tool that supports design by contract for Java.
- J-LO (the Java Logical Observer), a tool for "runtime-checking temporal assertions in Java 5 applications."
- Jtest a tool for design by contract and unit testing from Parasoft Corporation.
- Perfect Developer for Java and C++ from Eschertech.
- Javadoc FAQ.
- JUnit 5 for Java test cases.
- Java PathFinder a model checker for Java programs.
- Findbugs, a tool for finding bugs in Java code.
- Bandera a model checker and model checking framework for Java programs, including a frontend for JML.
- Spec# a specification language similar to JML for C#.
- ANSI/ISO C Specification Language (ACSL), a specification language for C whose design was "inspired by JML". ACSL is part of Frama-C, "open-source extensible and collaborative platform dedicated to source-code analysis of C software".
- Eiffel.com, which features various Eiffel software tools and documentation about Eiffel.
- SmartEiffel the GNU Eiffel compiler from SmartEiffel.loria.fr, home of open source Eiffel tools.
- Sage, a language with an expressive type system that includes specifications that are run-time checked.
- Mocha model checker home page.
- Alloy Analyzer, an object modeling notation and lightweight formal method.
- MulSaw project web page.
- OCL, the Object Constraint Language of the UML.
- AspectJ, an aspect-oriented programming for Java.
- The Larch FAQ.
Last modified Friday, December 10, 2021.