OOJML系列总结

目录

• 0x0 JML理论相关
  • 0.0 概念及作用
  • 0.1 JML语法学习
• 0x1 使用openJml以及JMLUnitNG
  • 1.0 使用openjml
  • 1.1使用JMLUnitNG
• 0x2 作业架构设计与分析
  • 2.0 第一次作业
  • 2.1 第二次作业
  • 2.2 第三次作业
• 0x3bug分析与测试
  • 3.0 bug分析
  • 3.1 Junit4测试
  • 3.2 python对拍
• 0x4 感想

0x0 JML理论相关

0.0 概念及作用

• JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。

• JML为严格的程序设计提供了一套行之有效的方法。通过JML及其支持工具（openJML与SMT Solver、JMLUnitNG等），不仅可以基于规格自动构造测试用例，还可以以静态方式来检查代码实现对规格的满足情况。

• 逻辑化规约代码实现人员与调用者，同时提高代码的可维护性与复用性。

0.1 JML语法学习

仅列举作业中常出现的

• 注释结构：块注释的方式为 /* @ annotation @*/，类似于Javadoc

• 量化表达式：

  • forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。 (forall int i,j; 0 <= i && i < j && j < 10; a[i] < a[j]) ，意思是针对任意 0<=i<j<10，a[i]<a[j] 。

  • exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。 (exists int i; 0 <= i && i < 10; a[i] < 0) ，表示针对0<=i<10，至少存在一个a[i]<0。

  • sum表达式：返回给定范围内的表达式的和。 (sum int i; 0 <= i && i < 5; i) ，这个表达式的意思计算[0,5)范围内的整数i的和，即0+1+2+3+4==10。

  • max表达式：顾名思义，返回给定范围内的表达式的最大值。

  • min表达式：顾名思义，返回给定范围内的表达式的最小值。

  原子表达式：

  • esult表达式：表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值。

  • old( expr )表达式：用来表示一个表达式 expr 在相应方法执行前的取值。

    • warning：针对一个对象引用而言，只能判断引用本身是否发生变化，而不能判断引用所指向的对象实体内容是否发生变化。注意区分v.size() 、old(v). size() 和old(v.size())。

  • 等等

  方法规格：

  • 前置条件(pre-condition)：requires：例如requires P1||P2;

  • 后置条件(post-condition)：ensures：例如ensures P1||P2;

  • 副作用范围限定(side-effects)：JML提供了副作用约束子句，使用关键词assignable或者modifiable。

    • /*@
      @ ...
      @ assignable 
      othing;
      @ assignable everything;
      @ modifiable 
      othing;
      @ modifiable everthing;
      @ assignable elements;
      @ modifiable elements;
      @ assignable elements, max, min;
      @ modifiable elements, max, min;
      @*/
      
      

    • assignble表示可赋值，而modifiable则表示可修改。 othing和everthing等表示作用域。

  区分方法的正常功能行为和异常行为：

  • public normal_behavior表示接下来对方法的正常功能给出规格。

  • 关键词 also，它的意思是还有其他正常功能或异常功能。

  • public exceptional_behavior表示接下来对方法的异常功能给出规格。

    • signals子句用来声明将会抛出的异常：

      • 结构为 signals (Exception e) expr ，意思是当 expr 为 true 时，方法会抛出括号中给出的相应异常e。

  不变式invariant

  状态变化约束constraint

0x1 使用openJml以及JMLUnitNG

JML工具链在这

warning：路径不能含有中文，血的教训，浪费了很多时间

1.0 使用openjml

openjml下载地址在这

环境：Windows，使用z3-4.7.1，jdk-8u251-windows-x64.exe

使用的命令：

*静态检查*：java -jar .openjml.jar -exec (SMT Solvers的路径) .Solvers-windowsz3-4.7.1.exe -esc -dir (项目目录)

针对本单元第三次作业的效果：貌似zyy带师的JML有些许问题？咱也不知道

1.1使用JMLUnitNG

JMLUnitNG1.4下载地址在这

环境同上

使用的命令：

java -jar .jmlunitng-1_4.jar *.java
javac -cp .jmlunitng-1_4.jar *.java
java -cp .jmlunitng-1_4.jar myitem.MyGroup_JML_Test

针对本单元第三次作业的MyGroup的使用效果：

评价：

学长诚不欺我，JMLUnitNG果然鸡肋，可以看到就是针对

• 以对象为参数的方法传诸如null
• 以整数为参数的方法传INT_MAX或INT_MIN
• 无参数的直接调用

测试力度仅此而已，相较之下自己写的JUnit覆盖性都要高得多，更无法相比黑盒测试了。

另外，注意到Failures都是出在不符合正常行为规格的传参上，因此也无关紧要

0x2 作业架构设计与分析

本单元作业不涉及重构，只有加构。

2.0 第一次作业

实现起来有难度或有坑的方法：isCircle和isLinked

isCircle直接使用BFS，小策略：每次isCircle都会记录结果，只要没有addRelation下次也可以使用。

isLinked要注意自己和自己也是返回true

难度较低，自主测试、公测、互测均无bug，互测对同屋同学无差别轰炸无果，遂放弃

2.1 第二次作业

实现起来有难度或有坑的方法：Group内部的诸如relationSum/ValueSum的查询方法

进行复杂度分析后认为无脑照着规格填代码有ctle风险，因此着重考虑尽量避免循环

采取策略思想：hashmap O(1)查询 + 操作离散化 + 数据破坏分析与维护

在此仅拿conflictSum举例，只有atg指令才有可能破坏数据，因此在MyGroup的addPerson中每次都进行更新操作即可

public class MyGroup implements Group {
		//...

	    @Override
    	public void addPerson(Person person) {
        	//...
        	conflictSum = conflictSum.xor(person.getCharacter());
        	//...
   	 	}

 		@Override
    	public BigInteger getConflictSum() {
        	return conflictSum;
    	}
    	
    	//...
}

addPerson可以做很多文章，最大化避免循环

值得一提的是：getAgeVar()方法可以使用概统的方差公式进行维护，不过要注意与规格精度相同。

2.2 第三次作业

实现起来有难度的方法：quaryStronglinked，blockSum，quaryMinPath等。

第三次作业考虑到blockSum实际上是求连通块数量：

• 一个思路是维护互相之间有关系的人的集合，这样子ap和ar就是将人加入集合以及集合合并的操作，有几个集合就有几个block，解决了blocksum；同时，isCircle就是看二者在不在一个set。

• 另一个思路就是并查集，第一个进入集合的人就是整个集合的boss（初始化每个人都是自己的boss），每次ar就对双方进行判定，看谁是谁的boss，使得关系层次变低，提高效率(路径压缩)，isCircle就是对两个人进行最高层boss查找（找整个集合的boss相当于树的祖先节点）同时路径压缩，这样子blocksum也就是看people中自己是自己的boss的情况的个数。

最终采用qsl:Tarjan + qmp:迪杰斯特拉算法与堆优化 + isCircle AND qbs:并查集等等算法，分别用边权内部类PersonAndLength以及边边内部类Edge开展Tarjan算法和dijkstra算法。充分的测试带来的也就是理所应当的公测、互测无bug。

附上第三次作业UML类图

不足：network太过臃肿，内含两个内部类，边权相关，应该与图论算法封装成一个图类，便于管理，同时优化架构，降低耦合。

0x3bug分析与测试

3.0 bug分析

前两次作业难度较低，自主测试、公测、互测均未发现bug

第三次作业对于性能方面要求不容小觑，自主测试时发现qsl所使用的Tarjan算法结束判定有问题，导致未搜索完全便结束，另外极端测试用例也暴露出性能上的危险。

发现同屋bug分析：

• 第二次作业hack了一个WR，无外乎规格看漏了或者理解不到位。
• 第三次作业hack了一个除零，在组内删除人更新方差的时候没有考虑人数为0的情况。

3.1 Junit4测试

针对MyNetwork的每个方法的JML描述情况进行覆盖性测试，以期基本功能的完善，复杂逻辑还须靠对拍

下面附上了第一次作业的Junit代码，有针对性的覆盖了isCircle和isLinked两个容易出错的方法

package test.java.MyItem;

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 myitem.MyNetwork;
import myitem.MyPerson;
import org.junit.BeforeClass;
import org.junit.Test;

import static org.junit.Assert.*;

import org.junit.After;

import java.math.BigInteger;

/**
 * MyNetwork Tester.
 *
 * @author <Authors name>
 * @version 1.0
 * @since <pre>4月 25, 2020</pre>
 */
public class MyNetworkTest {
    private static MyPerson person1 = new MyPerson(1, "a", BigInteger.ONE, 1);
    private static MyPerson person2 = new MyPerson(2, "b", new BigInteger("12345678901234456"), 2);
    private static MyPerson person3 = new MyPerson(3, "c", BigInteger.ZERO, 10);
    private static MyPerson person4 = new MyPerson(100, "ab", BigInteger.TEN, 100);
    private static MyPerson person5 = new MyPerson(5, "c", BigInteger.ZERO, 10);
    private static MyNetwork network = new MyNetwork();

    @BeforeClass
    public static void before() throws Exception {
        network.addPerson(person1);
        network.addPerson(person2);
        network.addPerson(person3);
        network.addPerson(person4);
        network.addPerson(person5);
    }

    @After
    public void after() throws Exception {
    }

    /**
     * Method: contains(int id)
     */
    @Test
    public void testContains() throws Exception {
//TODO: Test goes here...
        assertTrue(network.contains(1));
        assertTrue(network.contains(2));
        assertTrue(network.contains(3));
        assertTrue(network.contains(100));
        assertTrue(network.contains(5));

        assertFalse(network.contains(4));
        assertFalse(network.contains(-1));
    }

    /**
     * Method: getPerson(int id)
     */
    @Test
    public void testGetPerson() throws Exception {
//TODO: Test goes here...
        assertEquals(person1, network.getPerson(1));
        assertEquals(person2, network.getPerson(2));
        assertEquals(person3, network.getPerson(3));
        assertEquals(person4, network.getPerson(100));
        assertEquals(person5, network.getPerson(5));

        assertNotEquals(person1, network.getPerson(4));
        assertNotEquals(person1, network.getPerson(-1));
    }

    /**
     * Method: addPerson(Person person)
     */
    @Test
    public void testAddPerson() {
//TODO: Test goes here...
        try {
            network.addPerson(person1);
            network.addPerson(new MyPerson(6, "ls", new BigInteger("10000"), 20));

            assertTrue(network.contains(6));
        } catch (EqualPersonIdException e) {
            e.print();
        }
    }

    /**
     * Method: addCircle(int id1, int id2)
     */
    @Test
    public void testAddCircle() throws Exception {
//TODO: Test goes here... 
    }

    /**
     * Method: addRelation(int id1, int id2, int value)
     */
    @Test
    public void testAddRelation() throws Exception {
//TODO: Test goes here...
        network.addRelation(1, 1, 100);
        try {
            network.addRelation(1, 2, 100);
        } catch (EqualRelationException e) {
            e.print();
        }
        assertTrue(person1.isLinked(person2));
        assertTrue(person2.isLinked(person1));
        assertTrue(person1.isLinked(person1));
        assertTrue(person2.isLinked(person2));
        try {
            network.addRelation(-1, -1, 100);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
        try {
            network.addRelation(1, -1, 100);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
        try {
            network.addRelation(-1, 1, 100);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
        try {
            network.addRelation(1, 2, 100);
        } catch (EqualRelationException e) {
            e.print();
        }
    }

    /**
     * Method: queryValue(int id1, int id2)
     */
    @Test
    public void testQueryValue() throws Exception {
//TODO: Test goes here...
        try {
            network.queryValue(-1, 1);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
        try {
            network.queryValue(2, 1);
        } catch (RelationNotFoundException e) {
            e.print();
        }
    }

    /**
     * Method: queryConflict(int id1, int id2)
     */
    @Test
    public void testQueryConflict() throws Exception {
//TODO: Test goes here...
        assertEquals(person1.getCharacter().xor(person2.getCharacter()), network.queryConflict(1, 2));
        try {
            network.queryConflict(-1, 1);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
    }

    /**
     * Method: queryAcquaintanceSum(int id)
     */
    @Test
    public void testQueryAcquaintanceSum() throws Exception {
//TODO: Test goes here...
        assertEquals(person1.getAcquaintanceSum(), network.queryAcquaintanceSum(1));
        try {
            network.queryAcquaintanceSum(-1);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
    }

    /**
     * Method: compareAge(int id1, int id2)
     */
    @Test
    public void testCompareAge() throws Exception {
//TODO: Test goes here...
        assertEquals(person1.getAge() - person2.getAge(), network.compareAge(1, 2));
        try {
            network.compareName(1, -1);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
    }

    /**
     * Method: compareName(int id1, int id2)
     */
    @Test
    public void testCompareName() throws Exception {
//TODO: Test goes here...
        assertEquals(person1.getName().compareTo(person2.getName()), network.compareName(1, 2));
        try {
            network.compareName(1, -1);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
    }

    /**
     * Method: queryPeopleSum()
     */
    @Test
    public void testQueryPeopleSum() throws Exception {
//TODO: Test goes here...
        assertEquals(6, network.queryPeopleSum());
    }

    /**
     * Method: queryNameRank(int id)
     */
    @Test
    public void testQueryNameRank() throws Exception {
//TODO: Test goes here...
        assertEquals(1, network.queryNameRank(1));
        assertEquals(2, network.queryNameRank(100));
        assertEquals(3, network.queryNameRank(2));
        assertEquals(4, network.queryNameRank(3));
        assertEquals(4, network.queryNameRank(5));
        try {
            network.addPerson(new MyPerson(6, "ls", new BigInteger("10000"), 20));
        } catch (EqualPersonIdException e) {
            e.print();
        }


        assertTrue(network.contains(6));
        assertEquals(6, network.queryNameRank(6));
    }

    /**
     * Method: isCircle(int id1, int id2)
     */
    @Test
    public void testIsCircle() throws Exception {
//TODO: Test goes here...
        network.addRelation(1, 2, 10);
        network.addRelation(2, 3, 10);
        network.addRelation(3, 5, 10);
        network.addRelation(5, 100, 10);
        try {
            network.addPerson(new MyPerson(6, "ls", BigInteger.ZERO, 20));
        } catch (EqualPersonIdException e) {
            e.print();
        }

        assertTrue(network.isCircle(1, 1));
        assertTrue(network.isCircle(100, 100));
        assertTrue(network.isCircle(5, 5));
        assertTrue(network.isCircle(3, 3));
        assertTrue(network.isCircle(2, 2));

        assertTrue(network.isCircle(1, 2));
        assertTrue(network.isCircle(1, 2));
        assertTrue(network.isCircle(100, 2));
        assertTrue(network.isCircle(5, 3));
        assertTrue(network.isCircle(100, 5));
        assertTrue(network.isCircle(1, 100));
        assertFalse(network.isCircle(1, 6));

        try {
            network.isCircle(1, -1);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
        try {
            network.isCircle(-1, -1);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
        try {
            network.isCircle(-1, 1);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }

    }


}

3.2 python对拍

对拍是真的好使用，拉上几个hxd，xdm一起多人运动，发现bug效率倍增。

在此附上目录与效果，check为简单字符串比对，normal_data为规模可调全随机数据，extreme为精心构造的极端数据

0x4 感想

本单元体验依旧极佳

终于有一单元bugClear六根清净

第三单元主要是按照规格实现接口，认真阅读JML十分重要，不能放过任何一个细节，另外，还要要结合课程组给出的数据范围以及标程复杂度从全局出发考量方法实现的复杂度。

此单元迭代开发较容易，原因是大框架课程组已经给出，但是，还是要从全局方面设计算法架构，以带来更好的实现体验以及更优的算法复杂度，此次作业除了给定的几个接口，其他的类都可以为所欲为，可以选择将算法独立出来为一个类，提供相应方法供network调用，如此一来，便于换算法，可扩展性提高了。

照例还是要夸一波课程组的，如此好的课程体验最大的功臣就是我们的老师和助教大大！！

希望OO越来越好！！