一、JML理论基础

JML就是用于对JAVA程序设计逻辑的预先约定的一种语言，以便正确严格高效地完成程序以及展开测试，是一种行为接口规格语言。

1.原子表达式：

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

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

　　\not_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。

　　\not_modified(x,y,...)表达式：与上面的\not_assigned表达式类似，该表达式限制括号中的变量在方法执行期间的取 值未发生变化。

　　\nonnullelements( container )表达式：表示 container 对象中存储的对象不会有 null 。

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

　　\typeof(expr)表达式：该表达式返回expr对应的准确类型。

2.量化表达式：

　　\forall表达式：全称量词修饰的表达式。

　　\exists表达式：存在量词修饰的表达式。

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

　　\product表达式：返回给定范围内的表达式的连乘结果。

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

　　\min表达式：返回给定范围内的表达式的最小值。

 

　　\num_of表达式：返回指定变量中满足相应条件的取值个数。

3.操作符：

　　1.子类型关系操作符： E1<:E2，如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假。如果E1和E2是相同的类型，该表达式的结果也为真.

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

　　3. 推理操作符： b_expr1==>b_expr2 或者 b_expr2<==b_expr1 。对于表达式 b_expr1==>b_expr2 而言，当b_expr1==false ，或者 b_expr1==true 且 b_expr2==true 时，整个表达式的值为 true 。

　　4.变量引用操作符：除了可以直接引用Java代码或者JML规格中定义的变量外，JML还提供了几个概括性的关键词来引用相关的变量。\nothing指示一个空集；\everything指示一个全集.

　　5.关键词 also ，它的意思是除了正常功能规格外，还有一个异常功能规格.signals子句的结构为

 

　　　　Signals(***Exception e) b_expr.意思是当 b_expr 为 true 时，方法会抛出括号中给出的相应异常e。

4.应用工具链：

　　与规格化设计相关的工具主要有:OpenJML,JUnit,JUnitNG,SMT Solver等。

二、JMLUnitNG/JMLUnit

针对Mypath.java里面的部分方法进行测试：

三、架构设计梳理

1.第一次作业：这次作业主要是实现Mypath与MypathContainer两个分别继承两个官方提供接口的类。

主要做法就是在path类里面用一个arraylist存储每一个结点，然后用一个treeset来存储不同的结点，以便于getDistinctnode时直接返回treeset的长度即可；在MypathContainer类里面则是定义了三个hashmap,其中pathlist的key和value分别是id和path,pidlist当中的key和value则相反，ppathlist的key和value分别是结点和这个结点的个数。在增删路径的是时候就同时在三个hashmap里用put和remove方法就可以了。

第一次作业的架构：

 

第二次作业：

第二次作业主要是增加了无向图的操作，做法同样是使用hashmap，但是使用的是hashmap嵌套hashmap的方法来构造图，主要就是保存一个结点和与它相连的所有结点，增删路径的时候也算是照例使用put和remove方法来进行操作。

第二次作业架构：

第三次作业：

由于我第三次作业没有通过中测，所以就不多做阐述。

四、bug分析

第一次作业我没有在互测中被hack，但是在强测中挂掉了三个测试点，原因是我最先使用的都是arraylist方法所以导致了cpu时间过长，之后在Bug修复环节将mypathcontainer类里面的pathlist,pidlist,ppathlist全部改为hashmap,再使用hashmap方法进行操作即修复了所有bug。

第二次作业我没有成功进入互测，但是在测评结果出来的时候很无语，因为只是一行的简单错误，就是在containedge方法里没有仔细阅读规格，导致我在判断的时候漏掉了判断是否含有起始结点的这一判断，结果导致所有的评测结果都是空指针异常，在bug修复时增加了这一判断就全部通过了。

第三次作业由于我没有通过中测，不多做阐述。

五、心得体会

在这一单元初次接触了JML规格化设计，对于小白来说还是有点困难，但是在仔细学习过相关只是之后，读懂一般的规格并不是那么艰难。我现在对规格化的了解还是不够深，在课上实验自己撰写规格的时候还是会感到一点吃力，当然在这几次作业中我也吃过了没有仔细理解阅读规格的亏，在未来希望自己能够对规划化有更加深刻，自己也能够深入理解规格化设计的意义。