这篇日志继续总结些简单的JPF使用经验：
在http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc/doc 对Symbolic PathFinder进行了最基本介绍，并给出了一个Example.java和Example.jpf的例子。
这里摘录一些设置，进行简单的中文解释：
# The following JPF options are usually used for SPF as well:
# no state matching （设置不使用state matching）
vm.storage.class=nil
# instruct jpf to not stop at first error （设置运行过程中出错是否停止）
search.multiple_errors=true
# specify the search strategy (default is DFS) （设置搜索策略，默认为深度优先搜索）
search.class = .search.heuristic.BFSHeuristic
# limit the search depth (number of choices along the path)
# （设置搜索的深度）
search.depth_limit = 10
#You can specify multiple methods to be executed symbolically as follows:
#symbolic.method=<list of methods to be executed symbolically separated by ",">
#You can pick which decision procedure to choose (if unspecified, choco is used as #default):
# （symbolic pathfinder一共用了三种constraint solver，分别是choco，iasolver和CVC3）
symbolic.dp=choco
symbolic.dp=iasolver
symbolic.dp=cvc3
symbolic.dp=cvc3bitvec
symbolic.dp=no_solver
#(explores an over-approximation of program paths; similar to a CFG traversal)
#A new option was added to implement lazy initialization (see [TACAS'03] paper)
#（设置是否使用lazy initialization）
symbolic.lazy=on
#(default is off) -- for now it is incompatible with Strings
#New options have been added, to specify min/max values for symbolic variables #and also to give the default for don't care values.
symbolic.minint=-100
symbolic.maxint=100
symbolic.minreal=-1000.0
symbolic.maxreal=1000.0 symbolic.undefined=0
#An option to increase the time limit until which choco tries to solve a particular #constraint
choco.time_bound=30000
# default value is 30000
另外，实际上SPF提供了非常多的例子，来说明其用法，例子主要在：%JPF_HOME%\jpf\jpf-symbc\src\examples 目录下，以及%JPF_HOME%\jpf-symbc\src\tests\gov\nasa\jpf\symbc 目录下，譬如%JPF_HOME%\jpf\jpf-symbc\src\examples\strings 目录下，就介绍了怎么处理字符串数组变量（因为Java的main方法都是Strings[] args）。
我准备接下来看看什么是lazy initialization，争取在今天晚上再总结一篇博文。