Changes

Version 4.0

This JPF version is a major rewrite - roughly the same size like JPF3, but with about 2/3 of the system changed, and substantial new functionality. Here are the rough numbers:

Table 1: JPF4 statistics
	src	ext	env	test	doc	Σ
files	335	85	41	53	57	571
loc	39600	9528	4183	10141	(3840)	63452
classes	317	72	41	75	-	505

The majority of the changes are in the core (gov.nasa.jpf.jvm.*) and extension (gov.nasa.jpf.abstraction) packages. While the regression test suite has been extended, the increase of loc is mainly due to an added test for large methods.

Table 2: Change Statistics for JPF4
	src	ext	env	test	doc	Σ
files added	47	51	9	16	3	126
files deleted	45	0	3	0	3	51
files modified	179	21	28	29	18	275

Here is a roadmap of what has and will be changed in JPF4. The majority of the implemented changes are related to the new execution engine. The focus of remaining changes in this version will be twofold: (a) the Eclipse plugin, and (b) state abstraction extensions.

JPF v4 changes

Major improvements from a users perspective include:

better support for Java 5.0, especially java.util.concurrent and java.lang.reflect
concurrent, backtrackable class initialization

Here is a more detailed list of JPF4 changes from the developers point of view:

(1) Distribution

Subversion Repository
build-tools now part of distribution
documentation (web-site) part of distribution

(2) Functional Extensions

unified ChoiceGenerator based execution scheme
java.util.concurrent support (sun.misc.Unsafe)
direct call infrastructure, enabling backtrackable JPF execution from listeners and/or NativePeers, but also better fidelity of static initialization (was atomic)
(some) Method and Field reflection
state abstraction extension
symbolic execution

(3) Refactoring

use of Java 5 language extensions
JUnit 4.1 based regression tests (caused Ant update)
toplevel package abstraction removed (gov.nasa.jpf interfaces)
gov.nasa.jpf.util.Debug replaced with java.util.logging based system
script-less build/launch