ESC/Java2 License

The SRC "Java Programming Toolkit Source Release" was originally released under what we call a "pseudo-open source license." This license (from our reading) permitted us to modify the source any way we wanted, so long as we provided those changes back to the parent company and we did not commercialize the technology. (Note that this original SRC license cannot be seen at the SRC web pages unless you walk through the download process.)

Additionally, we originally understood that the license prohibited us from redistributing the original source of the toolkit, which meant we could only provide pre-built binary releases and patch-based releases. The latter would force interested parties to download the original toolkit from SRC, agreeing to the license in the process, then download and apply our patch release to have the full source code for ESC/Java2.

We also only permitted access to our CVS repository to parties who had accepted the original license and downloaded the toolkit source.

We and our users found this inconvenient, to say the least. After some discussions with knowledgeable parties at Hewlett-Packard, we came to realize that this inconvenience was not what was originally intended. Thus, a new "looser" version of the license was drafted and given to the H.P. lawyers sometime in Spring of 2004.

We have been given assurances from prior SRC ESC/Java team members that if we release a full source version of ESC/Java2 we will not be attacked by Hewlett-Packard's legal team. Thus, starting with version 2.0a9, we have done just this for the convenience of our users.

SRC ESC/Java license

Nearly all development over the past several years has been decoupled from the original SRC sources, thus we own the sources and we will be releasing it separately under the GPL. This new work was incorporated into the the Mobius Program Verification Environment, the development of which started in September 2005. The development work that falls under this umbrella includes all of the new back-ends to ESC/Java2 (SMT, PVS, Coq, etc.), the new VC generators, the new SMT and HOL logics, the specification consistency checker, the reachability analysis engine, pretty-printing of ASTs and VCs, VC complexity analysis, support for default non-null reference types, the universes type system, support for Java 5 and later VMs, specifications for Java 1.4 and later, all treatment of JML, loop invariant generation using SP/WP calculi, the ESC/Java2 Eclipse plugin, and assertion definedness checking.

All source for all versions of ESC/Java2 to date remain under the original SRC license, though we retain Copyright.

We do not expect any resolution on the original source license. If you are concerned about the ambiguous state of ESC/Java2, please email SRC and CC us.