ESC/Java, the Extended Static Checker for Java, is a tool designed to detect common run-time errors in Java programs at compile time using extended static checking, a form of static code analysis that extends traditional type checking. Originally developed at the Compaq Systems Research Center, ESC/Java2 added support for the Java Modeling Language specification language and multiple theorem provers, integrating with Eclipse. Though not sound or complete, it balances precision and usability. Its successor, OpenJML, supports Java 1.8, with source code hosted at GitHub.
See also
- Java Modeling Language (JML)
- Flanagan, C.; Kiniry, K. R. M. (2001). Houdini, an Annotation Assistant for ESC/Java. FME 2001: Formal Methods for Increasing Software Productivity. Lecture Notes in Computer Science. Vol. 2021. pp. 500–517. doi:10.1007/3-540-45251-6_29. ISBN 3-540-41791-5.
- Cataño, N.; Huisman, M. (2002). Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java. FME 2002:Formal Methods—Getting IT Right. Lecture Notes in Computer Science. Vol. 2391. pp. 272–289. doi:10.1007/3-540-45614-7_16. ISBN 3-540-43928-5.
- Cok, D. R.; Kiniry, J. R. (2005). ESC/Java2: uniting ESC/Java and JML. Proceedings of the 2004 international conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. Lecture Notes in Computer Science. Vol. 3362. pp. 108–128. doi:10.1007/978-3-540-30569-9_6. ISBN 3-540-24287-2.
- Chalin, P.; Kiniry, J. R.; Leavens, G. T.; Poll, E. (2006). Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. Formal Methods for Components and Objects. pp. 342–363. doi:10.1007/3-540-45614-7_16. ISBN 3-540-36749-7.
- Cok, D. R. (2006). Specifying java iterators with JML and Esc/Java2. Proceedings of the 2006 conference on Specification and verification of component-based systems. pp. 71–74. doi:10.1145/1181195.1181210. ISBN 1-59593-586-X.
- Chalin, P. (2006). Early detection of JML specification errors using ESC/Java2. Proceedings of the 2006 conference on Specification and verification of component-based systems. pp. 25–32. doi:10.1145/1181195.1181201. ISBN 1-59593-586-X.
- Ishikawa, H. (2009). An Approach for Refactoring using ESC/Java2: A Simple Case Study. Proceedings of the 2009 conference on New Trends in Software Methodologies, Tools and Techniques. pp. 61–72. ISBN 978-1-60750-049-0.
- Poll, E. (2009). Teaching Program Specification and Verification Using JML and ESC/Java2 (PDF). Proceedings of the 2nd International Conference on Teaching Formal Methods. Lecture Notes in Computer Science. Vol. 5846. pp. 92–104. doi:10.1007/978-3-642-04912-5_7. ISBN 978-3-642-04911-8.
- James, P. R.; Chalin, P. (2009). ESC4: a modern caching ESC for Java. Proceedings of the 8th international workshop on Specification and verification of component-based systems. pp. 19–26. doi:10.1145/1596486.1596491. ISBN 978-1-60558-680-9.
External links
- Java Programming Toolkit Source Release
- Extended Static Checking for Java at the Wayback Machine (archived December 8, 2005)
- ESC/Java2 at KindSoftware[usurped]
- SRC-RR-159 Extended Static Checking. - David L. Detlefs, K. Rustan M. Leino, Greg Nelson, James B. Saxe
- Extended Static Checking Modula-3 at the Wayback Machine (archived February 28, 2001)
- Extended Static Checking[usurped] Computer Science & Engineering Colloquia. University of Washington. 1999.
References
Flanagan, C.; Leino, K.R.M.; Lillibridge, M.; Nelson, G.; Saxe, J. B.; Stata, R. (2002). Extended static checking for Java. Proceedings of the Conference on Programming Language Design and Implementation. pp. 234–245. doi:10.1145/512529.512558. ISBN 1-58113-463-0. 1-58113-463-0 ↩
"OpenJML download site on sourceforge". http://jmlspecs.sourceforge.net/ ↩
"Java Modeling Language (JML) / Code / [r9606] /OpenJML/Trunk/OpenJML". https://sourceforge.net/p/jmlspecs/code/HEAD/tree/OpenJML/trunk/OpenJML/ ↩