ESC/Java
 | This article includes a list of general references, but it lacks sufficient corresponding inline citations. (March 2010) |
ESC/Java (and more recently ESC/Java2), the "Extended Static Checker for Java," is a
type checking. Extended static checking usually involves the use of an automated theorem prover
and, in ESC/Java, the Simplify theorem prover was used.
ESC/Java is neither
multithreading
.
ESC/Java was originally developed at the Compaq Systems Research Center (SRC). SRC launched the project in 1997, after work on their original extended static checker, ESC/Modula-3, ended in 1996. In 2002, SRC released the source code for ESC/Java and related tools. Recent versions of ESC/Java are based around the Java Modeling Language (JML). Users can control the amount and kinds of checking by annotating their programs with specially formatted comments or pragmas.
The
theorem provers and integration with Eclipse
.
OpenJML, the successor of ESC/Java2, is available for Java 1.8.[2] The source is available at https://github.com/OpenJML
See also
- Java Modeling Language (JML)
References
- Notes
- Flanagan, C.; Kiniry, K. R. M. (2001). Houdini, an Annotation Assistant for ESC/Java. FME 2001: Formal Methods for Increasing Software Productivity. pp. 500–517. 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. pp. 272–289. 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. pp. 108–128. 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. 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. 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. 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. pp. 92–104. 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. 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
- 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 Computer Science & Engineering Colloquia. University of Washington. 1999.