Java PathFinder 的安装与简单使用,测试除零错误

软件测试, 使用 Java PathFinder 来找出一段代码中的除零错误并显示出来.

1. 要求

Find and report the division by zero in the folling prgram with Java Pathfinder.

使用Java Pathfinder 找出下边程序代码中的除零错误并展示.

1.1 程序代码

public class Racer implements Runnable {
    int d = 42;
    public void run () {
    doSomething(1001);
    d = 0; // (1)
    }

    public static void main (String[] args){
          Racer racer = new Racer();
          Thread t = new Thread(racer);
          t.start();
          doSomething(1000);
          int c = 420 / racer.d; // (2)
          System.out.println(c);
    }

    static void doSomething (int n) {
        try { Thread.sleep(n); } catch (InterruptedException ix) {}
    }
}

1.2 参考

2. 前期准备

在进行实验之前,首先肯定是要安装配置环境了.

2.1 Java JDK

此处更改, 一开始我使用的是Ubuntu源可以安装的openJDK. 后来发现, 在最新版的 Java PathFinder 上会出现类似IO的错误.

所以,建议使用oracle JDK :

下载oracle JDK, 官网地址, 也可以直接点此链接下载Linux x64版本Java1.8 .
解压到随便一个目录中, 建议不要使用临时目录, 可以新建一个专门用来放类似软件的目录.

修改全局环境变量
执行命令:

sudo vim /etc/profile

这是使用Vim编辑, 如果没有安装vim ,可以使用sudo apt install vim 安装, 也可以换用 Gedit编辑, 即: sudo gedit /etc/profile

在文件末尾添加如下语句:

export JAVA_HOME=/usr/lib/jdk/jdk1.8   //这里的/usr/lib/jdk/jdk1.8要换成你的jdk的路径
export JRE_HOME=${JAVA_HOME}/jre
export CLASSPATH=.:${JAVA_HOME}/lib:${JRE_HOME}/lib
export PATH=.:${JAVA_HOME}/bin:$PATH

2.2 Eclipse (或者其他JavaIDE)

同样在 Ubuntu 16.04 下,执行如下命令:

sudo apt install eclipse

即可安装Eclipse.

2.3 安装Java PathFinder

我使用的IDE是Eclipse 所以, 在这里我以安装配置Eclipse插件包的形式介绍.

此方法适用于 Eclipse 4.3.x 以及 Java 7 以上版本, 更老的版本是否可以不清楚.

更多的安装介绍, 参考官方WiKi

2.3.1 开始安装

在Eclipse中安装有三种方式, 分别是源码构建, 安装插件Jar包,从更新站点安装.

这里, 我使用的是比较简单的安装方法, 具体操作如下:

打开 Eclipse
点击Help => Install New Software
输入此链接: http://babelfish.arc.nasa.gov/trac/jpf/raw-attachment/wiki/projects/eclipse-jpf/update
重启Eclipse,即可

2.3.2 安装过程截图

点击 Help => Install New Software ,

输入网址.png
点击 ADD,填入Name和location,也就是网址, Name可以随便填

add.png
稍微等待之后, 就能在下方看到内容,然后我们选择要安装的包,其实在这里就是全选了.

选择安装的包.png
然后Next,可能会出现如下图的提示,点击OK就行了, 没有提示的话更好.

安装提示.png
接受协议

接受协议.png
然后就可以看大安装成功了, 成功之后重启Eclipse即可.

安装完成提示重启.png

2.3.3 clone JPF-core

由于JPF项目存放在Mercurial版本控制仓库中,而不是GIT中, 所以我们需要一个新的工具来进行 clone.

同样Ubuntu 16.04下, 执行以下命令:

sudo apt install mercurial

安装完成之后, 使用 hg 命令进行下载操作,也就是clone:

hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-core

我们只需要clone jpf-core 即可.

记住下载保存的文件夹.

3. 测试是否存在除零错误

3.1 引入JPF-core项目

在Eclipse中选择作为一个已存在的项目进行引入.
引入之后,会自动进行编译,如果编译成功,则会出现:

bianyichenggong.png

如果出现错误, 根据错误信息解决就好.

比如, 我一开始使用的是Ubuntu源上的openJDK, 结果一直编译不过去, 然后我下载配置了官方的JDK1.8, 则成功编译了.

新建一个带有主方法的类:

newclass-1.png
将需要测试的代码写入到刚刚新建的类中:

newclass-2.png

然后会自动重新编译:

newclass-3.png

当然你也可以另外新建一个java项目. 例如:

newproject.png
右键这个类文件,选择Run AS => Run Configuration...., 然后在左侧找到run-JPF,

左侧runjpf.png
填写参数

填写参数.png

注意:

+target=Racer # 指明类名
+classpath=/home/xiaofei/eclipseWorkspace/JPF/jpf-core/bin  # 是类文件的目录地址

然后点击 Run , 即可.

3.2 测试结果

result.png

完成!