UnitThreeSummary

目录

• 一、JML的梳理与总结
• 二、SMT Solver的部署与验证
• 三、JMLUnitNG的部署与测试
• 四、作业的设计与总结
  • 第一次作业
  • 第二次作业
  • 第三次作业
• 五、BUG
• 六、总结与反思

一、JML的梳理与总结

(一)理论基础

1.定义(What)

The Java Modeling Language (JML) is a specification language for Java programs, using Hoare style pre and postconditions and invariants, that follows the design by contract paradigm. Specifications are written as Java annotation comments to the source files, which hence can be compiled with any Java compiler. --wiki

通俗而言，JML即是在Java代码中添加注释，这些注释使我们可以指定要执行的方法而不必说出它们如何执行。使用JML，我们可以在不考虑实现的情况下描述方法的预期功能。

2.好处(Why)

使用JML描述类和方法的期望行为可以带来如下好处：

• 可以对代码功能进行更精确的描述
• 按照规格描述可以更直接高效地发现和纠正错误
• 在程序的不断迭代开发过程中，可以减少引入错误的机会
• 可以同时获取与代码精确同步的文档
• ......

3.使用(How)

基本语法梳理如下：

关键字	含义
normal_behavior	正常行为
exceptional_behavior	异常行为
requires	前置条件
ensures	后置条件
\result	方法执行后的返回值
signals(e)	抛出异常e
\old(expr)	expr在方法执行前的取值
\forall	全称量词
\exists	存在量词
\sum	求和
\max	求最大值
\min	求最小值
\product	求得连乘结果
assignable	约束可以更改的数据
\type(type)	得到type对应的类型
\typeof(expr)	得到expr对应的准确类型
\not_assigned(variables)	限制对variables的赋值
\not_modified(variables)	varibles在方法执行过程中没有改变
\nonnullelements(container)	约束container中的对象不含有null
&&	与逻辑
||	或逻辑
==	相等
==>	蕴含
<==>	互相蕴含
invariant	不变式:在所有可见状态下都必须要满足的性质
constraint	状态变化约束
pure	常用来描述不会对对象的状态进行任何改变，也不需要提供输入参数的访问性的方法，可以在其他方法规格中引用

4.具体使用实例

通过ensures约束结果

//@ ensures \result == id;
public /*@pure@*/ int getId();

通过\exists存在量词描述容器内是否包含person

//@ ensures \result == (\exists int i; 0 <= i && i < people.length; people[i].equals(person));
public /*@pure@*/ boolean hasPerson(Person person);

通过\sum描述求和，最后求得平均值

/*@ ensures \result == (people.length == 0? 0 : 
  @          ((\sum int i; 0 <= i && i < people.length; people[i].getAge()) / people.length));
  @*/
public /*@pure@*/ int getAgeMean();

通过signals表示不满足条件时抛出异常,normal_behavior和exceptional_behavior分别表示正常情况和异常情况

/*@ public normal_behavior
  @ requires contains(id);
  @ ensures (\exists int i; 0 <= i && i < people.length && people[i].getId() == id;
  @          money[i] == \result);
  @ also
  @ public exceptional_behavior
  @ signals (PersonIdNotFoundException e) !contains(id);
  @*/
public /*@pure@*/ int queryMoney(int id) throws  PersonIdNotFoundException;

(二)应用工具链

JML工具链完整清单：http://www.eecs.ucf.edu/~leavens/JML//download.shtml

以下主要介绍几个可以使用的工具

1.OpenJML

使用SMT Solver来对检查程序实现是否满足所设计的规格。

下载地址：http://www.openjml.org/

2.JMLUnitNG

根据规格自动化生成测试样例，进行单元测试。

官网地址：http://insttech.secretninjaformalmethods.org/software/jmlunitng/

3.Eclipse_OpenJML插件

安装地址：http://jmlspecs.sourceforge.net/openjml-updatesite/

二、SMT Solver的部署与验证

部署方法

在Eclipse上安装OpenJML插件，具体步骤如下:

1.Help -> Install New Software -> add

Location为http://jmlspecs.sourceforge.net/openjml-updatesite/

2.Window -> Preferences -> OpenJML -> OpenJML Solvers->设置配置

如图：

路径自定义，本次使用的SMT Solver为z3

测试方法为：

public class Test {
	public static void main(String[] args) {
		System.out.println(Test.add(1, 2));
		System.out.println(Test.sub(2,1));
		System.out.println(Test.div(6, 3));
	}
	
	//@ensures \result == a + b;
	public static int add(int a, int b) {
		return a + b;
	}
	
	//@ensures \result == a - b;
	public static int sub(int a, int b) {
		return a - b;
	}
	
	//@ensures \result == a / b;
	public static int div(int a, int b) {
		return a / b;
	}
}

因为z3不能较好的支持复杂的JML逻辑，所以写了三个简单的方法进行测试

测试结果如下图：

INVALID说明存在溢出的情况,div还可能出现除0的情况

三、JMLUnitNG的部署与测试

JMLUnitNG部署步骤如下：

注：所有步骤都在同一目录下执行

1.下载OpenJML，并执行java -jar openjml.jar "$@"

2.下载JMLUnitNG，保存到OpenJML所在的目录下，并执行java -jar jmlunitng.jar "$@"

3.在OpenJML所在目录下新建文件夹demo,并创建./demo/Demo.java，如下 ：

package demo;
import java.util.ArrayList;
public class Demo {
    public ArrayList<Integer> peopleId = new ArrayList<Integer>();
    // @ public normal_behaviour
    // @ ensures \result = peopleId.size();
    public /*@pure@*/ int getSize(){
        return peopleId.size();
    }
    // @ public normal_behaviour
    // @ requires index >= 0 && index < size();
    // @ assignable \nothing;
    // @ ensures \result == peopleId.get(index);
    public   /*@pure@*/ int getPersonId(int index) {

        if (index < 0 || index >= getSize()) {
            return -1;
        }
        return peopleId.get(index);
    }
    public static void main(String[] args) {
        Demo example = new Demo();
        example.peopleId.add(1);
        example.peopleId.add(2);
        int x = example.getSize();
        System.out.println(x);
        int y = example.getPersonId(1);
        System.out.println(y);
    }
}

因为JMLUnitNG不支持\forall,\exists等较为复杂的关键词，所以选取了作业中两个较为简单的方法组成新的Demo

4.执行命令java -jar jmlunitng.jar demo/Demo.java

自动生成如下文件：

demo
├── Demo_InstanceStrategy.java
├── Demo.java                                      
├── Demo_JML_Data
│   ├── ClassStrategy_int.java
│   ├── ClassStrategy_java_lang_String1DArray.java
│   ├── ClassStrategy_java_lang_String.java
│   ├── compare__int_lhs__int_rhs__0__lhs.java
│   ├── compare__int_lhs__int_rhs__0__rhs.java
│   └── main__String1DArray_args__10__args.java
├── Demo_JML_Test.java
├── PackageStrategy_int.java
├── PackageStrategy_java_lang_String1DArray.java
└── PackageStrategy_java_lang_String.java

5.编译所有文件，分别执行javac -cp jmlunitng.jar demo/**/**.java，javac -cp jmlunitng.jar demo/**.java

6.执行命令java -jar openjml.jar -rac demo/Demo.java，得到rac文件

7.执行命令java -cp jmlunitng.jar demo/Demo_JML_Test，运行得到如下结果

至此，有关JMLUnitNG的部署与自动测试已经完成。

四、设计策略与程序分析

第一次作业

设计思路：

实现接口中的方法

其中isCircle采用bfs实现

并通过Junit构造测试数据测试异常情况：

import com.oocourse.spec1.exceptions.EqualPersonIdException;
import com.oocourse.spec1.exceptions.EqualRelationException;
import com.oocourse.spec1.exceptions.PersonIdNotFoundException;
import com.oocourse.spec1.exceptions.RelationNotFoundException;
import org.hamcrest.Matchers;
import org.junit.Assert;
import org.junit.BeforeClass;
import org.junit.Test;

import static org.hamcrest.MatcherAssert.*;

import java.math.BigInteger;

public class TaskOneTest {
    private static MyNetwork network = new MyNetwork();
    private static MyPerson myPerson = new MyPerson(1, "test", BigInteger.TWO, 100);

    @BeforeClass
    public static void before() throws EqualPersonIdException {
        //normal
        network.addPerson(new MyPerson(1, "a", BigInteger.ONE, 1));
        network.addPerson(new MyPerson(2, "b", BigInteger.ZERO, 2));
        network.addPerson(new MyPerson(6, "c", BigInteger.ZERO, 3));
        network.addPerson(new MyPerson(7, "d", BigInteger.ZERO, 4));
        network.addPerson(new MyPerson(8, "e", BigInteger.ZERO, 5));
        network.addPerson(new MyPerson(9, "f", BigInteger.ZERO, 6));
    }

    @Test
    public void getId() {
        Assert.assertEquals(myPerson.getId(), 1);
    }

    @Test
    public void getName() {
        Assert.assertEquals(myPerson.getName(), "test");
    }

    @Test
    public void getCharacter() {
        Assert.assertEquals(myPerson.getCharacter(), BigInteger.TWO);
    }

    @Test
    public void getAge() {
        Assert.assertEquals(myPerson.getAge(), 100);
    }

    @Test
    public void isLinked() {
        Assert.assertTrue(myPerson.isLinked(myPerson));
    }

    @Test
    public void getAcquaintanceSum() {
        Assert.assertEquals(myPerson.getAcquaintanceSum(), 0);
    }

    @Test
    public void queryValueInMyPerson() {
        Assert.assertEquals(myPerson.queryValue(myPerson), 0);
    }

    @Test(expected = EqualPersonIdException.class)
    public void addPerson() throws EqualPersonIdException {
        //exception
        network.addPerson(new MyPerson(1, "a", BigInteger.ONE, 1));
    }

    @Test(expected = PersonIdNotFoundException.class)
    public void addRelationNoId() throws PersonIdNotFoundException, EqualRelationException {
        network.addRelation(3, 2, 3);
    }

    @Test(expected = EqualRelationException.class)
    public void addRelationEqualRelation() throws PersonIdNotFoundException, EqualRelationException {
        network.addRelation(1, 2, 100);
        network.addRelation(2, 1, 10);
    }

    @Test(expected = PersonIdNotFoundException.class)
    public void queryValue() throws PersonIdNotFoundException, RelationNotFoundException, EqualRelationException {
        //normal
        network.addRelation(6, 7, 100);
        int ans = network.queryValue(6, 7);
        Assert.assertEquals(ans, 100);
        int sameId = network.queryValue(1, 1);
        Assert.assertEquals(sameId, 0);
        //exception
        network.queryValue(2, 3);
    }

    @Test(expected = PersonIdNotFoundException.class)
    public void queryConflict() throws PersonIdNotFoundException {
        //normal
        BigInteger ans = network.queryConflict(1, 2);
        Assert.assertEquals(ans, BigInteger.ONE);
        //exception
        network.queryConflict(2, 3);
    }

    @Test(expected = PersonIdNotFoundException.class)
    public void queryAcquaintanceSum() throws PersonIdNotFoundException, EqualRelationException {
        //normal
        network.addRelation(8, 9, 1);
        int ansA = network.queryAcquaintanceSum(8);
        int ansB = network.queryAcquaintanceSum(9);
        Assert.assertEquals(ansA, 1);
        Assert.assertEquals(ansB, 1);
        //exception
        network.queryAcquaintanceSum(3);
    }

    @Test(expected = PersonIdNotFoundException.class)
    public void compareAge() throws PersonIdNotFoundException {
        //normal
        int ans = network.compareAge(1, 2);
        Assert.assertEquals(ans, -1);
        int sameId = network.compareAge(1, 1);
        Assert.assertEquals(sameId, 0);
        //exception
        network.compareAge(1, 3);
    }

    @Test(expected = PersonIdNotFoundException.class)
    public void compareName() throws PersonIdNotFoundException {
        //normal
        int ans = network.compareName(1, 2);
        Assert.assertEquals(ans, -1);
        int sameId = network.compareName(1, 1);
        Assert.assertEquals(sameId, 0);
        //exception
        network.compareName(1, 3);
    }

    @Test
    public void compareNameTestWithAssertThat() throws PersonIdNotFoundException {
        //normal
        assertThat(network.compareName(1, 9), Matchers.lessThan(0));
        assertThat(network.compareName(7, 1), Matchers.greaterThan(0));
    }


    @Test
    public void queryPeopleSum() {
        int ans = network.queryPeopleSum();
        Assert.assertEquals(ans, 6);
    }

    @Test(expected = PersonIdNotFoundException.class)
    public void queryNameRank() throws PersonIdNotFoundException {
        //normal
        int ans = network.queryNameRank(2);
        Assert.assertEquals(ans, 2);
        //exception
        network.queryNameRank(3);
    }

    @Test(expected = PersonIdNotFoundException.class)
    public void isCircle() throws PersonIdNotFoundException, EqualRelationException {
        //normal
        network.addRelation(1, 2, 100);
        boolean ans = network.isCircle(1, 2);
        Assert.assertTrue(ans);
        //exception
        network.isCircle(3, 2);
    }
}

第二次作业

设计思路：

isCircle转变为并查集实现

同时利用Hashmap建立对应映射关系提升查询效率

MyGroup的方法中普遍采用缓存机制O(1)实现方法提升效率

比如getRelationSum方法，只需要在MyGroup中维护一个变量即可，当向组内添加人和添加组内人的关系时，更新此变量，查询时直接返回此变量的值即可。

再比如getAgeVar方法，只需要在每次向组内加人的时候，同时对年龄的平方求和，在查询时，按照未化简的方差公式计算并返回值即可。

同时增加Junit测试方法对新增方法进行测试，新增测试方法如下：

@Test(expected = EqualGroupIdException.class)
    public void addGroup() throws EqualGroupIdException {
        //normal
        network.addGroup(new MyGroup(1));
        network.addGroup(new MyGroup(2));
        //exception
        network.addGroup(new MyGroup(1));
    }

    @Test(expected = GroupIdNotFoundException.class)
    public void addToGroupGroupIdNotFound() throws EqualGroupIdException, PersonIdNotFoundException, EqualPersonIdException, GroupIdNotFoundException {
        //normal
        network.addGroup(new MyGroup(3));
        network.addtoGroup(1, 3);
        //exception
        network.addtoGroup(2, 4);
    }

    @Test(expected = PersonIdNotFoundException.class)
    public void addToGroupPersonIdNotFound() throws EqualGroupIdException, PersonIdNotFoundException, EqualPersonIdException, GroupIdNotFoundException {
        //exception
        network.addGroup(new MyGroup(4));
        network.addtoGroup(12, 4);
    }

    @Test(expected = EqualPersonIdException.class)
    public void addToGroupEqualPersonIdFound() throws EqualGroupIdException, PersonIdNotFoundException, EqualPersonIdException, GroupIdNotFoundException {
        //normal
        network.addGroup(new MyGroup(5));
        network.addtoGroup(6, 5);
        //exception
        network.addtoGroup(6, 5);
    }

    @Test(expected = GroupIdNotFoundException.class)
    public void QueryGroup() throws EqualGroupIdException, PersonIdNotFoundException, EqualPersonIdException, GroupIdNotFoundException, EqualRelationException {
        //normal
        network.addGroup(new MyGroup(6));
        network.addtoGroup(9, 6);
        Assert.assertEquals(network.queryGroupConflictSum(6), BigInteger.ZERO);
        //Assert.assertEquals(network.queryGroupPeopleSum(6),1);
        Assert.assertEquals(network.queryGroupRelationSum(6), 1);
        network.addRelation(7, 9, 12);
        network.addtoGroup(7, 6);
        Assert.assertEquals(network.queryGroupRelationSum(6), 4);
        Assert.assertEquals(network.queryGroupValueSum(6), 24);
        network.addtoGroup(10, 6);
        Assert.assertEquals(network.queryGroupConflictSum(6), BigInteger.TWO);
        Assert.assertEquals(network.queryGroupAgeMean(6), 5);
        Assert.assertEquals(network.queryGroupAgeVar(6), 0);
        //exception
        network.queryGroupPeopleSum(10);
    }

    @Test(expected = GroupIdNotFoundException.class)
    public void GroupNotFoundTest1() throws GroupIdNotFoundException {
        network.queryGroupRelationSum(10);
    }

    @Test(expected = GroupIdNotFoundException.class)
    public void GroupNotFoundTest2() throws GroupIdNotFoundException {
        network.queryGroupValueSum(10);
    }

    @Test(expected = GroupIdNotFoundException.class)
    public void GroupNotFoundTest3() throws GroupIdNotFoundException {
        network.queryGroupConflictSum(10);
    }

    @Test(expected = GroupIdNotFoundException.class)
    public void GroupNotFoundTest4() throws GroupIdNotFoundException {
        network.queryGroupAgeMean(10);
    }

    @Test(expected = GroupIdNotFoundException.class)
    public void GroupNotFoundTest5() throws GroupIdNotFoundException {
        network.queryGroupAgeVar(10);
    }

第三次作业

设计思路：

为了使各个算法的实现不增加MyNetwork的复杂度，将各个图相关的算法实现单独建类并统一管理，具体UML如下图：

同时利用getPersonById和getGroupById方法将重复的异常判断抽离出来

private Person getPersonById(int id) throws PersonIdNotFoundException {
    if (!contains(id)) {
        throw new PersonIdNotFoundException();
    }
    return people.get(id);
}

private Group getGroupById(int id) throws GroupIdNotFoundException {
    if (!groups.containsKey(id)) {
        throw new GroupIdNotFoundException();
    }
    return groups.get(id);
}

最终MyNetwork的实现只有307行

较为复杂的方法具体实现算法：

方法	算法
isCircle	并查集
queryMinPath	堆优化的Dijkstra
queryStrongLinked	tarjan
queryBlockSum	直接利用isCircle的并查集统计连通块的个数

复杂度分析：

五、BUG

三次作业强测互测均未出现bug

互测中hack别人的bug主要是：

1.对JML的规格实现不完全(比如缺少判断相等的情况)

2.方法的实现复杂度过高而超时(比如qsl用dfs实现)

除了使用Junit构造测试数据测试以外，三次作业还通过自动生成数据进行对拍测试程序的正确性

测试数据生成python脚本：

import random

instructions = ['ar',
                'ap',
                'qci',
                'qv',
                'qc',
                'qas',
                'ca',
                'cn',
                'qnr',
                'qps',
                'ag',
                'atg',
                'qgs',
                'qgps',
                'qgrs',
                'qgvs',
                'qgcs',
                'qgam',
                'qgav',
                'qasu',
                'qmp',
                'qsl',
                'dfg',
                'qbs',
                'bf',
                'qm']

maxPersonNumber = 800
maxGroupNumber = 10
maxInstructionNumber = 10000
maxValue = 1000
maxName = 100000
maxCharacter = 100000
maxAge = 2000

f = open('total_test.txt', 'w')

for time in range(maxInstructionNumber):
    i = random.randint(0, 25)
    f.write(instructions[i] + ' ')
    if i == 0 or i == 24:
        f.write(str(random.randint(0, maxPersonNumber)) + ' ' + str(random.randint(0, maxPersonNumber)) + ' ' + str(
            random.randint(0, maxValue)))
    elif i == 1:
        f.write(str(random.randint(0, maxPersonNumber)) + ' ' + str(random.randint(0, maxName)) + ' ' + str(
            random.randint(0, maxCharacter)) + ' ' + str(random.randint(0, maxAge)))
    elif i == 2:
        f.write(str(random.randint(0, maxPersonNumber)) + ' ' + str(random.randint(0, maxPersonNumber)))
    elif i == 3 or i == 4 or i == 6 or i == 7 or i == 20 or i == 21 or i == 22:
        f.write(str(random.randint(0, maxPersonNumber)) + ' ' + str(random.randint(0, maxPersonNumber)))
    elif i == 5 or i == 8 or i == 25:
        f.write(str(random.randint(0, maxPersonNumber)))
    elif i == 10 or i == 13 or i == 14 or i == 15 or i == 16 or i == 17 or i == 18:
        f.write(str(random.randint(0, maxGroupNumber)))
    elif i == 11:
        f.write(str(random.randint(0, maxPersonNumber)) + ' ' + str(random.randint(0, maxGroupNumber)))
    elif i == 19:
        f.write(str(random.randint(0, maxAge)) + ' ' + str(random.randint(0, maxAge)))
    else:
        pass
    f.write('\n')

六、总结与反思

第三单元主要是对JML描述的方法的具体实现，特别需要注意JML描述中的细节之处的实现，同时要结合课程组给出的数据范围从全局出发考量方法实现的复杂度。

与前两个单元相比，第三单元强调的更多是规格二字，从规格出发，同时又不拘泥于规格，才能正确高效的完成每一次的迭代开发。

在迭代开发的过程中，要考虑一个类的复杂度，比如MyNetwork，要不断地将复杂的算法抽象分离，同时可以将重复的异常判断单独提出，减少重复代码。

最后要综合考量实现算法的效率和用此算法实现的方法的可拓展性，比如isCircle方法，如果采用并查集实现，那么未来提出在社交网络中删去某关系的新需求时，此时并查集对这种拓展性的需求包容性并不是特别高，所以实现方法的算法不应是一成不变的，应当随着需求的变化而变化，在效率和拓展性中做出权衡。