ESC/Java2 Implementation Notes
David R. Cok, Joseph R. Kiniry, Dermot Cochran · 2008
Abstract: ESC/Java2 is a tool for statically checking program specifications. It expands significantly upon ESC/Java, on which it is built. It is consistent with the definition of JML and of Java 1.4. It adds additional static checking to that in ESC/Java; most significantly, it adds support for checking frame conditions and annotations containing method calls. This document describes the status of the final release of ESC/Java2, along with some notes regarding the details of that implementation.