ESC/Java2 FAQ

If you have any questions that you'd like added to this FAQ, please email your suggestions to either of the mailing lists. Thanks!

  1. What is ESC/Java2?

    The Extended Static Checker for Java version 2 (ESC/Java2) is a programming tool that attempts to find common run-time errors in Java programs by static analysis of Java programs and their JML annotations. Users can control the amount and kinds of checking that ESC/Java2 performs by annotating their program with specially formatted comments called pragmas. Pragmas are written in the Java Modeling Language (JML), a behavioral interface specification language for Java.

  2. Where did the name "ESC/Java2" come from?

    The original extended static checkers were called ESC/Modula-III (the extended static checker for the Modula-III programming language) and ESC/Java (the extended static checker for Java). The final version of ESC/Java to "ship" from Compaq SRC was version 1.2.4. Thus, when we began development on a new, updated, Open Source version of ESC/Java with tons of new features, it seemed fitting to bump a major version number. Thus, ESC/Java version 2, or ESC/Java2 for short, was born.

  3. What is the latest release of ESC/Java2? What is the development schedule for future releases?

    The latest release of ESC/Java2 is version 2.0.5. It is the 16th release of ESC/Java2 and its 1st stable release.

  4. I have looked at the ESC/Java2 source, and the design of the front-end (the lexer, parser, typechecker) confuse me because they do not seem to be really "object-oriented". Why is the front-end designed like this?

    ESC/Java2's frontend is inherited from SRC ESC/Java, which was written by several scientists and interns at Digital's Systems Research Lab in the late 1990s. While the original authors sometimes claim that the architecture has an "object-oriented" design, most would say that it is, instead, a "structured" design, given the heavy use of static variables to represent the state of the parser, for example.

    I (Joe K.) believe that this is (at least partially) due to several factors including: (a) the small size and close relationship of the original team, (b) the original team was very experienced with writing programs in modular programming languages but not object-oriented programming languages, and (c) the desire that the front-end be highly efficient both in time and space. As a result, while because of (a) and (b) the design is a bit difficult to initially understand and modify, due to (c) it is very efficient.

    We have attempted to remedy this situation in the ESC/Java2 project in two ways. First, we have been writing architecture documentation and supplimentary materials to introduce new developers to ESC/Java2. See, for example, the extensive "ESC/Java2 Implementation Notes" and the forthcoming "Extending ESC/Java2" booklet. Second, we have been writing formal specifiations of the architecture and running the JML tool suite and ESC/Java2 on itself.

  5. Can I run ESC/Java2 in a Java 1.5 VM or reason about Java 1.5 source code?

    ESC/Java2 is written with Java 1.4 and only runs in a Java 1.4 or 1.5 virtual machine. While ESC/Java2 should work in any Java 1.4 or 1.5 virtual machine, we strongly suggest using the latest stable release (1.4.2_09 at the time of this writing).

    ESC/Java2 does not parse Java 1.5 code, thus cannot reason about Java 1.5 programs. There are no plans at this time to support Java 1.5 source code within the ESC/Java2 framework. Work is ongoing to build a new extended static checker based upon the Eclipse JDT. Contact Joe Kiniry for more information about this project.

  6. What is the ESC/Java2 license like?

    See the license page on this site for more information. Essentially, we are still contrained by the original Compaq license, but we hope to make all of our changes available under a liberal Open Source BSD-like license in the near future. We also hope that Compaq will someday release the original source under a more mainstream, liberal license (e.g., GPL, BSD, or MIT license).

  7. Who has contributed to ESC/Java2?

    Contributors to ESC/Java2, direct and indirect, whether they know it or not, include: Michiel Alsters, Cees-Bart Breunesse, Mark Brown, Patrice Chalin, Rod Chapman, Michel Charpentier, Yoonsik Cheon, Curt Clifton, Dermot Cochran, David Cok, Jean-francois Dazy, Barry Denby, David Detlefs, Jean-Michel Douin, Fintan Fairmichael, Cormac Flanagan, Conor Gallagher, Radu Grigore, Martin Hoffmann, Engelbert Hubbers, Marieke Huisman, Clément Hurlin, Bart Jacobs (RUN), Mikoláš Janota, Joe Kiniry, Gary Leavens, Rustan Leino, Mark Lillibridge, Claude Marche, Todd Millstein, Alan Morkan, Peter Muller, David Naumann, Greg Nelson, Martijn Oostdijk, Wolter Pieters, Erik Poll, Frederic Rioux, Edwin Rodriguez, Clyde Ruby, Will Sargent, Jim Saxe, Aleksy Schubert, Silvija Seres, Raymie Stata. Cesare Tinelli, Martijn Warnier, and Daniel Zimmerman.

    Apologies if we have missed anyone, as I only update this list ever few months. Please email Joe if you think I need a nudge.

  8. What is the history of ESC/Java2?

    ESC/Java2 is the direct descendant of the Compaq Extended Static Checker for Java. The main group responsible for extended static checking research was at Digital Equipment Corporation's Systems Research Lab (SRC) in the mid-to-late 1990s. That group consisted of many excellent researchers including Cormac Flanagan, Mark Lillibridge, Greg Nelson, Jim Saxe, and Raymie Stata. The project was lead by K. Rustan M. Leino. Cormac and Raymie are now at UCSC. Rustan now leads a group at Microsoft Research working on Spec#, a kind of JML for C#. Greg is still at Hewlett-Packard (who bought Compaq in 2002) and works on digital printing technologies. Jim and Mark are perhaps also still at Hewlett-Packard. The main authors of ESC/Java2 are David Cok and Joe Kiniry. David is Chief Technologist for the Photographic Center within Kodak's R&D Laboratories in Rochester, New York. Joe is a Lecturer in Computer Science at University College Dublin.

  9. How do I get the source for ESC/Java2 or pre-built executables?

    You can download the latest ESC/Java2 source code and executables via the one of the ESCJava2 release home page mirrors:

  10. Are previous versions of ESC/Java available?

    You can download H.P./Compaq SRC ESC/Java (version 1.2.4) directly from HP's Java Programming Toolkit Source Release web page. Note that the SRC no longer actually exists and there is no guarantee that the SRC web page will remain online in the future (we have already chased it around a few times). We have previous versions of ESC/Java2 (version 2.0a0, 2.0a1, etc.) available as well, but given every version of ESC/Java2 is better in every way that its predecessor, we see no reason to keep old versions online. If you really need an older version, please email us and we'll get it to you.

  11. How can I contribute?

    You can contribute in many, many ways to ESC/Java2 and related projects.

    Most importantly, user feedback is extremely valuable to us. What are you doing with ESC/Java2? What problems are you having? What successes have you had? What kind of programs are you trying to check? What new features would you like to see? You can raise a bug report or feature request via our Trac.

    Only the very core classes of Java have JML specifications. So another very valuable way to contribute to not just ESC/Java2, but the entire JML community, is to write specs! Writing JML specifications for the classes you use is the best way to learn JML, the JML tools, and ESC/Java2. It is also an excellent way to learn the intimate details of the packages you use. We find that after having written the spec for a class you often understand it better than the original authors!

    There are many proposed research project descriptions available on the KindSoftware web site that involve program specification and verification in some fashion. Feel free to review these projects, take good ideas, and contact Joe with questions or comments.

    You can build a new tool that is based upon, or uses ESC/Java2 as a component. This approach has been followed by several contributors already. For example, see Engelbert Hubbers's work on integrating several JML-based tools into a single framework and Christoph Csallner's work called CnC which takes ESC/Java2-generated counterexamples and compiles them into JUnit test cases.

    Finally, we welcome new developers to contribute to ESC/Java2. For example, some independent submissions include: Will Sargent wrote the ESC/Java2 Ant task, Jean-Michel Douin and Jean-francois Dazy contributed a Windows batch file, and Aleksy Schubert added the -L switch.

    If you wish to contribute but do not quite know where to start or what needs doing, just email us and let us know your interests and background and we will try to point you in the right direction.

  12. What tools are used to develop ESC/Java2?

    Each developer uses his or her own set of tools. Since ESC/Java2 is written in Java and is completely platform independent, we do not force the use of any particular development environment. Joe uses a heavily enhanced Emacs and all of the tools mentioned in the KindSoftware code standard, David used vim and a shell until recently moving to Eclipse.

  13. What is the primary documentation on ESC/Java2?

    We have not written an updated User's Guide for ESC/Java2. The User's Guide of ESC/Java is still highly relevant.

    The subversion repository of ESC/Java2 contains all of the original ESC/Java design documents from SRC. These documents provide background information on the design, purpose, and history of SRC ESC/Java.

    We are also writing several documents about various aspects of ESC/Java2. These are not exhaustive, but contain large amounts of useful information.

  14. What university classes use ESC/Java2?

    A partial list of instructors using ESC/Java2 to teach (currently or in the past, in no particular order) includes:

    ESC/Java2 has been used to teach programming in Java, software engineering, (applied) formal methods, programming language semantics, program specification and verification, and security. It has also been used to help grade Java programs.

  15. What research groups or individuals are using ESC/Java2?

    A partial list of groups and researchers using or extending ESC/Java2 or Simplify (currently or in the past, in no particular order) includes:

    • Alastair Donaldson at Imperial College London
    • Don Sannella's group at the University of Edinburgh
    • Gary Leavens's group at Iowa State University
    • Patrice Chalin's group at Concordia University
    • Steve Edwards's group at the University of Vermont
    • Peter Schmidt at an undisclosed university in Austria
    • Richard Knight at the University of North Carolina (Charlotte)
    • Steffen Schlager's group at the University of Karlsruhe
    • Jean-Michel Douin and Jean-francois Dazy at the Conservatoire National des Arts et Metiers Paris
    • the SAnToS lab at Kansas State University
    • Timothy Halloran at Carnegie Mellon University
    • Ozan Yigit at York University in Canada
    • Leonardo Freitas at University of York (previously at the University of Kent)
    • Nick Rutar at the University of Maryland
    • Nichole Rauch at informatik.uni-kl.de
    • Adnan Agbaria at UIUC
    • Hiroshi Wanatabe's group at the Center for Verification and Semantics, National Institute of Advanced Industrial Science and Technology (AIST) in Amagasaki, Japan
    • David Notkin's group at the University of Washington
    • Christoph Csallner's group at Georgia Tech
    • Marieke Huisman's students (Julien Groslambert) at the Franche-Comte University
    • Jun Yuan
    • Carl Pulley at ACME Labs in the UK
    • Rosemary Monahan's group at the National University of Ireland, Maynooth
    • Daniel Moisset at ?
    • Ke Sun, an MSc student at Eindhoven
  16. What companies have used ESC/Java2 in some manner (currently or in the past, in no particular order)?

    A partial list of companies includes:

    • the Formal Methods and Security group, Smart Cards Research, Axalto (a Schlumberger Company), France
    • DoCoMo Labs in San Jose, California
    • the Center for Verification and Semantics, National Institute of Advanced Industrial Science and Technology (AIST) in Amagasaki, Japan
    • tma.com.vn in Vietnam
    • T.J. Watson Research Labs at IBM
    • RapidMoney Corporation
    • ACME Labs
    • Sun Microsystems
  17. What research tools incorporate ESC/Java2 or Simplify in some way?

    We are aware of the following tools. If you have developed a new tool, please let us know.

    • Engelbert Hubbers integrated several JML-based tools into a single framework
    • Christoph Csallner's developed CnC which takes ESC/Java2-generated counterexamples and compiles them into JUnit test cases
    • The Spec# system at Microsoft Research

    Also, comparisons of ESC/Java2 with other tools have been written. For example, see this recent ISSRE paper by Rutar, Almazan, and Foster which describes a "meta-tool" to combine many approaches, including extended static checking.

  18. If I want to learn about extended static checking or related topics (source code-based verification, formal annotations, object logics, etc.), where should I look?

    Jonathan Bowen's Formal Methods web pages are an excellent starting point for this kind of work. The JML web site is the key website for all things JML-related. The Spec# project at Microsoft Research is one of the other most active research groups in this domain.

  19. What is the future of Simplify?

    Simplify was written by Greg Nelson and others at SRC. It is implemented in Modula-III. The only recent development on Simplify that has taken place is our port of it to Mac OS X. We do not plan on doing any development on Simplify, as the world of first-order theorem provers has changed quite a bit over the past decade or so. Instead, we are working on integrating ESC/Java2 with new-generation SMT-LIB provers. As of mid-2011 there was a rumor that H.P. has decided to release Simplify under an Open Source license, but we have yet to see an official announcement.

  20. How can I integrate ESC/Java2 into my development process?

    ESC/Java2 generates warnings and error messages in the standard output format of various GNU tools like gcc. Thus, if your development environment understands the output of any such tools, it will work with ESC/Java2.

    For example, by using a Makefile and compile-mode in Emacs, one can execute the tool and directly jump to the indicated lines in warnings and errors with a push of a button.

    We are writing a booklet at the moment, entitled "The Mobius Software Development Process," that discusses these issues in detail using a series of case studies.

  21. Does ESC/Java2 support any modern Java IDEs such as Eclipse?

    David Cok has implemented a minimal GUI for ESC/Java2. By running the ESC/Java2 jar file directly, you will see the GUI.

    David also initiated the implementation of an excellent Eclipse plug-in for ESC/Java2. This work is now continued by various Mobius partners. Please see the KSU homepage for more details.

    An ESC/Java plug-in for Eclipse has also been written by researchers at the University of Virginia. Please see their Engineering Software webpage for more information.

  22. Where do discussions about ESC/Java2 take place?

    There are two mailing lists that focus on ESC/Java2:

    1. The JMLSpecs-ESCJava mailing list is the "users" mailing list where one can ask questions of experienced users and the developers of ESC/Java2. Subscribe to this list by registering at SourceForge.
  23. What is the future of ESC/Java2?

    ESC/Java2 is no longer under development. It has been replaced by the ESC component of JMLEclipse from Patrice Chalin, Jooyong Lee, and Robby and the ESC component of OpenJML by David Cok. Contact those respective authors for more information about these new generations of extended static checkers for Java.