下载完成相应组件后,从控制台进入jpf-core安装目录(以jpf-core的安装为例,毕竟这个是必须的),如C:\Documents and Settings\Administrator\jpf\jpf-core中,运行

bin\ant test

然后ant会出现很多信息,如果顺利的话,会在最后出现

BUILD SUCCESSFUL
Total time: 2 minutes 31 seconds

类似这样的信息。但是我在自己服务器上build的结果是会有一个报错:

BUILD FAILED
C:\Documents and Settings\Administrator\jpf\jpf-core\build.xml:350: Test gov.nasa.jpf.test.mc.data.PerturbatorTest failed

但是经过上述Build运行之后,已经能够成功生成“build”文件夹了。当然,如果不通过repositories进行安装,则更为简单和便捷,在JPF的每个组件的介绍页面的最下部,都有相应ZIP文件夹包含了已经编译好的对应项目,例如jpf-core的zip文件可以通过链接:http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-core#no1 直接看到。

接下来我们简单通过Eclipse来看看JPF的功能,参考页面http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/eclipse-plugin 中提示的最简单步骤(Using the Update Site (Simplest Method))可以很简单地安装JPF的Eclipse Plugin。但是如果仅仅安装该Plugin,还是不能正常在Eclipse中运行JPF。需要进行下述检查及设置:

1. 创建site.properties文件并进行设置。

在安装好Eclipse插件后,在Eclipse主界面Window--Preferences--JPF Preferences中的Path to site properties可以看到,该插件对site.properties的默认位置是:C:\Documents and Settings\Administrator\.jpf\site.properties (这个每个系统会有微小差异),方便起见,我们可以将site.properties文件创建在该位置。在JPF主页上有对site.properties在window下创建的示例:http://babelfish.arc.nasa.gov/trac/jpf/attachment/wiki/install/site-properties/site.properties-windows

2. 在Eclipse中运行JPF插件。

正如这个页面中http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/build 中讲到的,Specify classpath=PATH_TO_BIN_DIRECTORY to add the class files for the program under test to JPF's class path. Windows users will need to use the double-backslash notation in specifying paths in the .jpf file. 和命令行相比,在Eclipse中运行稍微麻烦一些,需要在.jpf文件中指定classpath,classpath的值就是需要进行检验的java文件对应的bin目录,例如,如果要对HelloWorld这个类进行检验,那么classpath应设置成类似:

classpath=C:\\Documents and Settings\\Administrator\\workspace\\HelloWorld\\bin

的值。上面的页面还很细心地提到注意将单斜杠换成双斜杠。

更改好之后,在Eclipse IDE下右键单击对应的.jpf文件,选择“Verify”,就可以用JPF分析目标文件并产生结果了。这次就记这么多。

【连载,未完待续】

[Java Path Finder][JPF学习笔记][2]在Windows Server上安装JPF相关推荐

  1. [Java Path Finder][JPF学习笔记][1]在Windows Server上安装JPF

    从这篇blog开始,准备记录下自己学习和使用JPF的经验,很多都只是官网Manual的翻译. 在这里:http://babelfish.arc.nasa.gov/trac/jpf/wiki/insta ...

  2. Solr学习笔记001---solr在windows下的安装及配置

    JAVA技术交流QQ群:170933152 首先,solr是基于java开发的,所以使用的话需要先进行java环境的配置,在Java环境配置好之后就可以去http://www.apache.org/d ...

  3. kali linux重启网络服务报错,Web安全学习笔记之在Kali Linux上安装Openvas以及启动失败修复...

    现在用的kali linux是2018.1的版本,在安装openvas的时候报错,无法通过网络下载和安装openvas. 主要错误是源配置错误,可能现在用的kali很久没更新了. 一.解决和配置更新源 ...

  4. PCL学习笔记01:在Ubuntu上安装PCL

    文章目录 一.PCL官网 二.在Ubuntu上安装PCL 三.PCL官网教程 四.溜达一圈PCL 五.PCL基本结构 (一)有组织的点云 (二)无组织的点云 六.测试PCL是否安装成功 (一)编写程序 ...

  5. WPF学习笔记——在“System.Windows.StaticResourceExtension”上提供值时引发了异常

    在"System.Windows.StaticResourceExtension"上提供值时引发了异常 因应需要,写了一个转换器,然后窗体上引用,结果就出来这个错.编译的时候没事, ...

  6. Mysql学习笔记——mysql服务在win上安装与启动

    1.先去下载服务包 https://dev.mysql.com/downloads/mysql/ 2.下载完成后,解压在D盘 3.添加一个配置文件,先创建文本,填写内容后改名:my.ini 内容为: ...

  7. JAVA基础与高级学习笔记

    JAVA基础与高级学习笔记 /记录java基础与高级,除了较简单的内容,没有必要记录的没有记录外,其余的都记录了/ java初学者看这一篇就够了,全文 6万+ 字. JAVA基础 java会出现内存溢 ...

  8. 第10课:底实战详解使用Java开发Spark程序学习笔记

    第10课:底实战详解使用Java开发Spark程序学习笔记 本期内容: 1. 为什么要使用Java? 2. 使用Java开发Spark实战 3. 使用Java开发Spark的Local和Cluster ...

  9. 零基础学习Java开发,这些学习笔记送给你

    因为Java具备很多特点,并且在企业中被广泛应用为此很多小伙伴选择学习Java基础开发,但是零基础学习Java技术开发需要我们制定Java学习路线图对于我们之后的学习会非常有帮助. 零基础学习Java ...

最新文章

  1. iOS开发之--TableViewCell重用机制避免重复显示问题
  2. 在细分场景的时代,如何反欺诈和防止内外勾结?
  3. Nginx-Nginx配置文件详细说明
  4. Windows基础题目
  5. mysql 字符串索引 优化_MySQL性能优化之索引调优实战
  6. 姓名和学号 c语言,急啊!!!求救了 C语言编一个链表,输出姓名和学号就好
  7. 关于解决jdbc版本错误问题
  8. linux apktool使用教程,简单介绍ubuntu下apktool的使用与配置
  9. Alex 的 Hadoop 菜鸟教程: 第21课 不只是在HBase中用SQL:Phoenix
  10. 结合spring IOC AOP Mybatis写一个简易的银行转账案例
  11. 2015阿里巴巴实习生招聘客户端开发试题
  12. 红外触发蓝牙遥控器自动匹配
  13. kali 插上耳机没声音
  14. 博客篇-如何使用阿里云搭建网站
  15. Java通过freemaker实现健康报告生成(包含列表、列表合并列)
  16. [CTF] SQL注入的一些经验总结(未完待续)【更新:2022.11.25】
  17. form表单用butten提交后无反应表单提交三种方式
  18. Xbox One的Unity在这里!
  19. linux 多线程环形缓冲区,[多线程]环形缓冲区以及多线程条件同步
  20. 项目经理,你要考的证书都在这

热门文章

  1. 随机突然黑屏重启解决经验分享(华硕主板)
  2. 牛客网 MIKU酱的氪金宝典(BFS)
  3. 几个测试阶段英文简写的解释说明
  4. 该选自动对焦还是定焦的OAK相机?
  5. 加密软件的加密技术发展分析
  6. 【Tools-Mujoco】创建自定义的Mujoco模型
  7. 【ABAP】VL01N、VL02N、VL03N和VL06G过账发货功能码的区别
  8. 频率响应范围测试软件,关于示波器频率响应分析仪选件和伯德图测试的区别和发展分析...
  9. 数据填报有什么用?数据填报系统具有哪些优势?_光点科技
  10. 服务器编码问题ascii’ codec can’t encode character