[Java Path Finder][JPF学习笔记][6]jpf-symbc的初步使用
2011-12-13 18:51
531 查看
这篇日志继续总结些简单的JPF使用经验:
在http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc/doc 对Symbolic PathFinder进行了最基本介绍,并给出了一个Example.java和Example.jpf的例子。
这里摘录一些设置,进行简单的中文解释:
另外,实际上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,争取在今天晚上再总结一篇博文。
在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,争取在今天晚上再总结一篇博文。
相关文章推荐
- [Java Path Finder][JPF学习笔记][6]jpf-symbc的初步使用
- [Java Path Finder][JPF学习笔记][5]编译jpf-symbc报错的解决方法
- [Java Path Finder][JPF学习笔记][3]使用jpf-shell
- [Java Path Finder][JPF学习笔记][5]编译jpf-symbc报错的解决方法
- [Java Path Finder][JPF学习笔记][8]几篇使用JPF的论文
- [Java Path Finder][JPF学习笔记][3]使用jpf-shell
- [Java Path Finder][JPF学习笔记][8]几篇使用JPF的论文
- Memcached学习笔记——windows上初步使用(与java结合)
- Memcached学习笔记——windows上初步使用(与java结合)
- [Java Path Finder][JPF学习笔记][1]在Windows Server上安装JPF
- [Java Path Finder][JPF学习笔记][7]JPF输出详细程度设置
- [Java Path Finder][JPF学习笔记][2]在Windows Server上安装JPF
- [Java Path Finder][JPF学习笔记][1]在Windows Server上安装JPF
- [Java Path Finder][JPF学习笔记][7]JPF输出详细程度设置
- [Java Path Finder][JPF学习笔记][4]将JPF源码导入Eclipse
- [Java Path Finder][JPF学习笔记][2]在Windows Server上安装JPF
- [Java Path Finder][JPF学习笔记][4]将JPF源码导入Eclipse
- [Java Path Finder][JPF学习笔记][4]将JPF源码导入Eclipse
- 第10课:底实战详解使用Java开发Spark程序学习笔记
- Java菜鸟学习笔记(3)--Java API 文档下载与文档注释的使用