这篇日志继续总结些简单的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=

#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方法都是String[] args)。

我准备接下来看看什么是lazy initialization，争取在今天晚上再总结一篇博文。