第三单元博客作业

一、JML

JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言（Behavior Interface Specification Language，BISL），基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。

1.1 JML语言的理论基础

首先是注释结构，JML以javadoc注释的方式来表示规格，每行以@起头，可以采用行注释和块注释。

JML的表达式

​ 类型规格：

• 不变式(invariant)是要求在所有可见状态下都必须满足的特性。
• 状态变化约束(constraint)是对前序可见状态和当前可见状态的关系约束，即对象的状态在变化时满足的一些约束，这种约束本质上也是一种不变式。

​ 方法规格：

• requires 子句 ：定义了方法的前置条件

• assignable 子句 ： 给出了方法会修改的类成员属性。\nothing表示不改变任何类成员属性。

• ensures 子句：定义了方法的后置条件

  原子表达式：

• \result ：方法的返回值

• \old(expr)：表示expr在执行该方法前的取值。

• \type(type)表达式：返回类型type对应的类型（Class）

• 量化表达式：

• \forall()：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。

• \exists()：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。

• \sum表达式：返回给定范围内的表达式的和。

• \max表达式：返回给定范围内的表达式的最大值。

  操作符：

• 等价关系操作符： b_expr1<==>b_expr2 或者b_expr1<=!=>b_expr2 ，其中b_expr1和b_expr2都是布尔表达式，这两个表达式的意思是b_expr1==b_expr2 或者b_expr1!=b_expr2。

• 推理操作符： b_expr1==>b_expr2 或者b_expr2<==b_expr1。

还有许多可以在JML的手册中查到，上面是我认为经常会用到的表达式。

1.2 工具链

​ OpenJML,JUnitNG等等都是与规格化设计相关的工具。

• Openjml主要帮助我们检查规格化语言JML的语法和保证基本逻辑的正确性。
• JUnitNG则是对JML规格进行测试，可以根据JML生成对应的测试用例，用于进行单元化测试。

1.3 JMLUnitNG

测试代码

public class Demo{    private /*@ spec_public @*/ int demoNum;    public Demo(int demoNum) {        this.demoNum = demoNum;    }    //@ ensures \result == this.demoNum;    public /*@pure@*/int getDemoNum() {        return demoNum;    }    //@ ensures \result == (this.demoNum >= 2);    public /*@pure@*/boolean isValid() {        return demoNum >= 2;    }    /*@ requires o != null;      @ assignable \nothing;      @ ensures \result == this.demoNum - o.getDemoNum();      @*/    public /*@pure@*/int TestOverflow(Demo o) {        return this.demoNum - o.getDemoNum();    }}

测试结果：

可以看到在TestOverflow的测试时出现了o为null的问题。

二、作业设计

第一次作业

​ 在MyPath类当中，我选择使用ArrayList来存储构造Path中的点序列，主要目的是为了存储点序列的排列信息，同时我也使用了HashMap来存储点元素的信息，即每个点在Path中存在个数，为了解决Path中对点种类的访问。但是在重写CompareTo方法的时候没有考虑减法溢出。在MyPathContainer类中，我选择使用了3个HashMap的结构分别来存储，Path与id的对应，id与Path的对应，点和Path集合中该点的个数的对应。前两个HashMap是为了方便各种add和remove的操作，不用遍历Path的集合，加快速度。第三个HashMap为了加快getDistinctNodeCount方法的速度。

第二次作业

​ 前两个类没有修改。MyGrapy类中，我是直接将MyPathContainer的类中的方法复制过去，更好的做法应是用MyGrapy继承MyPathContainer类，重写部分方法即可。本次的主要问题是如何降低isConnected和getShortestPathLength的时间。主要是通过根据每个Path的信息，将每个Node之间连边构成图，我是使用邻接表存储的。因为这是一个每个边权值都是一样的图，所以在求最短路径的时候直接使用了BFS。现在想来，应该封装一个类，这个类完全符合图计算时的要求，具有图基本的数据结构，这样来实现会使下一次作业轻松很多。

第三次作业

​ 本次作业中，我采用的是拆点的方法，将每个相同id的点都与一个与该id对应的标准点相连，且权值为换乘的代价的一半。对于新增3个询问，本质上都是求最短路径，只是边的权值不同。所以我写了一个标准的图的类，即具有点集和边集，且具有求最短路功能的类，对于3个询问，建立3个这样的对象，在增减Path的时候对3个图进行更新即可。关于连通块就是无脑bfs莽加上保存之前结果。

三、作业中的bug与修复

第一次作业中，重要的问题是没有对溢出的考虑，也是在思考的时候没有在意这方面，在Junit单元测试的时候也没有覆盖到。

第二次作业实现思路比较清晰，所以没有出现什么问题。

在第三次作业中，在完成的过程中发现了两个重要的bug。

• 设计方法没有考虑到自己到自己的情况，会导致结果增加一次换乘代价，这是该方法的特殊性，经过特判才能解决。
• 在dijkstra当中，采用了优先队列的写法，在更新的点的最短距离时，直接更新，没有对优先队列进行维护导致的bug，这是由于对优先队列理解不足导致的。

四、心得体会

在这三次作业当中，对JML有了基本的了解和认识，可以理解JML的语句并且能够自己写出JML的规格。发现了JML较自然语言更加精确地描述代码所完成的任务，便于我们有效地发现和纠正错误，比如在写作业的时候，有的时候偷懒就直接按自己对题意的理解去写代码，之后对照JML，发现自己的理解具有偏差，也能够快速精准地发现自己的错误。同时它具有一定的规则，便于自动化地测试，这个有丶酷。但是有一个比较明显的不足， 在第三次作业中，3个求最短路的方法的规格十分复杂，难以让人有耐心去理解，当然我也认为写出这样的规格也十分费力，我觉得不亚于写代码本身，这是它在实际中存在的问题。