[null, {"document_url": "https://link.springer.com/chapter/10.1007%2F978-3-642-20398-5_35", "unformatted_src": "https://media.springernature.com/w306/springer-static/cover/book/978-3-642-20398-5.jpg", "src": "https://media.springernature.com/w306/springer-static/cover/book/978-3-642-20398-5.jpg"}, null]


NASA Formal Methods NASA Formal Methods Symposium

NFM 2011: NASA Formal Methods pp 472-479 | Cite as

OpenJML: JML for Java 7 by Extending OpenJDK


The Java Modeling Language is a widely used specification language for Java. However, the tool support has not kept pace with advances in the Java language. This paper describes OpenJML, an implementation of JML tools built by extending the OpenJDK Java tool set. OpenJDK has a readily extendible architecture, though its details could be revised to further facilitate extension. The result is a suite of JML tools for Java 7 that provides static analysis, specification documentation, and runtime checking, an API that is used for other tools, uses Eclipse as an IDE, and can be extended for further research. In addition, OpenJML can leverage the community effort devoted to OpenJDK.


OpenJML JML specification verification OpenJDK ESC/Java2








Cok D.R. (2011) OpenJML: JML for Java 7 by Extending OpenJDK. In: Bobaru M., Havelund K., Holzmann G.J., Joshi R. (eds) NASA Formal Methods. NFM 2011. Lecture Notes in Computer Science, vol 6617. Springer, Berlin, Heidelberg



