目录
OO第三单元作业(JML)总结
JML语言知识梳理
使用jml的目的
- 开展规格化设计
- 针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性
jml注释结构
在我目前看来，jml其实就是一门被规定好格式要求的注释语言，它的作用也是给方法、类等一个相比自然语言来说更加严谨完善的介绍。它主要有三种注释方法：
//@ public model non_null int [] elements;/*@ blablabla
@ blablabla
@*/public abstract/*@ blabla @*/intlargest(); jml表达式
jml表达式的语法还是比较贴近自然语言的，用起来感觉挺容易上手也挺有趣的，整理一下比较眼熟常用的表达式
-
原子表达式 （约定好的代表一个值的表达式）
\result ：表示非void方法返回值
\old(expr) ： 表示expr在执行方法前的样子
\not_assigned(x,y,...) ： 方法是否对x，y等变量赋值，boolean型表达式
\not_modified(x,y,...) ：方法是否改变x，y等变量的值，boolean型表达式
\nonnullelements(container) ： 容器中不会有null
-
量化表达式 （类似离散数学中的符号）
\forall表达式：全称量词修饰，用法如
(\forall int i,j; 0 <= i && i < j && j < 10; a[i] < a[j])\exists ： 存在量词修饰，用法类似 forall
\sum ： 求和，用法如
(\sum int i; 0 <= i && i < 5; i*i) 解释：对于int i;i满足的条件;求和对象\max ： 求最大，用法类似sum
\min ： 求最小，用法类似sum
-
操作符 （类似离散）
等价关系操作符：（没太理解<==>与==之间的异同）
b_expr1<==>b_expr2 or b_expr1<=!=>b_expr2推理操作符：
b_expr1==>b_expr2 or b_expr2<==b_expr1变量引用操作符：
\nothing：空集，\everything：全集
方法规格
-
正常行为规格与异常行为规格
/*@ normal_behavior @ bla bla bla bla bla @ also @ exceptional_behavior @ bla bla bla @*/ -
前置条件
/*@ ??_behavior @ requires P; //表示需要表达式P为真 @ bla bla bla @*/ -
后置条件
/*@ bla bla bla @ ensures P; //表示保证表达式P为真 @ bla bla bla @*/ -
副作用限制
assignable modifiable -
signals子句 （用来指示抛出异常）
// @ signals (***Exception e) b_expr //当 b_expr 为真时，抛出指定异常
类型规格
-
不变式invariant
要求在所有可见状态下都必须满足的特性，可根据invariant约定写出repOk函数，配合assert使用尤佳（荣老师的强烈推荐），可以直接有效的定位在何处导致代码出现违背不变式的bug
-
状态变化约束constraint
对象的状态在变化时必须满足的一些约束
SMT Solver
暂时先不研究
部署JMLUnitNG与使用
首先十分感谢伦佬在讨论区的精彩分享，教会我如何配置jmlunit进行测试
我测试的代码如下：
public class Testjml {
/*@ public normal_behaviour
@ ensures \result <==> (i1 == i2);
*/
public static boolean intEquals(int i1, int i2) {
return i2 == i1;
}
/*@ public normal_behaviour
@ requires s1 != null && s2 != null;
@ ensures \result <==> (s1 == s2);
*/
public static boolean stringEquals(String s1, String s2) {
return s1.equals(s2);
}
}按照伦佬的教程，将openjml和jmlunitng都设置成命令
之后，在源文件所在文件夹下依次执行以下命令：
jmlunitng Testjml.java
javac -cp jmlunitng.jar *.java
openjml -rac Testjml.java可以得到文件树：
.
├── jmlunitng.jar
├── PackageStrategy_int.class
├── PackageStrategy_int.java
├── PackageStrategy_java_lang_String.class
├── PackageStrategy_java_lang_String.java
├── Testjml.class
├── Testjml_ClassStrategy_int.class
├── Testjml_ClassStrategy_int.java
├── Testjml_ClassStrategy_java_lang_String.class
├── Testjml_ClassStrategy_java_lang_String.java
├── Testjml_InstanceStrategy.class
├── Testjml_InstanceStrategy.java
├── Testjml_intEquals__int_i1__int_i2__0__i1.class
├── Testjml_intEquals__int_i1__int_i2__0__i1.java
├── Testjml_intEquals__int_i1__int_i2__0__i2.class
├── Testjml_intEquals__int_i1__int_i2__0__i2.java
├── Testjml.java
├── Testjml_JML_Test.class
├── Testjml_JML_Test.java
├── Testjml_stringEquals__String_s1__String_s2__20__s1.class
├── Testjml_stringEquals__String_s1__String_s2__20__s1.java
├── Testjml_stringEquals__String_s1__String_s2__20__s2.class
└── Testjml_stringEquals__String_s1__String_s2__20__s2.java
0 directories, 23 files执行测试：
java -cp jmlunitng.jar Testjml_JML_Test可以得到测试结果：
发现程序运行出错，测试结果很明确的让我门发现了没有处理传入参数为null的情况，及时改正代码（瞎改改，主要为了测试jml）增加处理null的情况如下：
public class Testjml {
/*@ public normal_behaviour
@ ensures \result <==> (i1 == i2);
*/
public static boolean intEquals(int i1, int i2) {
return i2 == i1;
}
/*@ public normal_behaviour
@ requires s1 != null && s2 != null;
@ ensures \result <==> (s1 == s2);
*/
public static boolean stringEquals(String s1, String s2) {
if (s1 == null || s2 == null) {
return true;
} else {
return s1.equals(s2);
}
}
}再次按相同步骤运行可以得到：
这次就全部通过啦！
再次感谢各位大佬在讨论区精彩分享的帮助！
三次作业架构设计梳理
第一次作业
第一次作业要求我们实现两个类MyPath以及MyPathContainer来完成以下几个功能：
添加路径
删除路径
根据路径id删除路径
查询路径id
根据路径id获得路径
获得容器内总路径数
根据路径id获得其大小
根据路径id获取其不同的结点个数
接结点序列判断容器是否包含路径
根据路径id判断容器是否包含路径
容器内不同结点个数
根据字典序比较两个路径的大小关系
路径中是否包含某个结点
其中线性指令（需要构建path的指令）较少，而查询指令较多，且题目明确说明需要我们考虑时间复杂度以防超时，这就要求我们在设计之初便考虑好使用何种容器来保存相应的数据。
对于Path类，由于每条path的长度只有1000，而且构造path不可避免的需要遍历一遍输入的节点序列，因此我选择Arraylist作为存path的容器，又因为需要统计path不同节点数，为了简便，我使用java自带的treeset容器在构造path时就将节点扔进去，这样无论是增长路径或者截断路径，统计不同节点数方面都很好拓展。
对于PathContainer类，根据需求描述，最花时间的操作即确定路径id与路径间的对应关系，而我们在path中实现了compareto接口，因此我选择treemap来保存路径与路径id间的映射关系，且路径id是不会重复并且小于300的，那么可以直接使用数组来存储id与路径的映射关系，因为要确定不同节点的数量，我使用了treemap来维护节点的出现情况。
第二次作业
第二次作业新拓展的需求为
容器中是否存在某一条边
两个结点是否连通
两个结点之间的最短路径
这次作业中之前各类指令数量的比例不变，在考虑过后，认为可以直接继承上一次的代码，只需拓展构图即可。
构图方面，我也比较简单粗暴，直接在graph类里进行，为了防止重复连边，使用treeset保存一个点与哪些点之间直接相连，因为构图指令较少，每次图结构发生变化时，我都重新进行构图，并且使用n遍bfs求出每个点到其他点的最短距离保存下来。
然而由于个人太懒，而且没有仔细考虑代码的维护和拓展性，没有想到需要构造出多种不同的图，也就没有听从指导书的建议，将算法和建图封装成单独的类，这就导致整个类显得很冗杂。
第三次作业
第三次作业新拓展的需求为：
整个图中的连通块数量
两个结点之间的最低票价
两个结点之间的最少换乘次数
两个结点之间的最少不满意度
这次作业要新拓展的功能很多，不过基本上也都是对建图和最短路算法的改变，如果还像之前那样直接全塞在MyRailwaySystem中，那么这个类将变得“又臭又长”(可能我自己写得丑)，因此，我选择将构图和求最短路封装起来，每次要构图时，将已有的path信息交给图类，令其构造出符合条件的图，此外为了构图还新封装了edge类表示图中的边。
除了新加的需求外，之前的需求可以直接复用之前的代码，不再多说。
联通块的数量，我选择在第二次作业bfs时加入染色机制，求连通块，这也是这次作业最简单的需求。
其它三个需求其实本质上都可以使用同一个图连接结构，配以不同的权值，使用最短路算法求得，而这个构图方式需要一定技巧。即将不同路径的点都视作不同的节点，节点标号若相同，则都连在同一源点（类比地铁换乘站）上，并且给这条边给予合理的权值，使得两点间最低票价（不满意度）就是该图上两节点相应源点间最短路。
三次作业中代码的bug及修复
此次三次作业主要是按照提出的需求和给好的架构写代码，因此bu*生的几率也少了很多，三次强测中我都安全度过，happy
然而，如助教所说，度过强测并不意味着代码没有bug，第一次作业和第一次互测中都没被发现bug的我，在第二次互测中被人找到了如下bug
这智障的bug居然是经过我和同学一起检查之后都没发现的，这也从侧面反映了我的测试做的并不充分和全面，单元测试也没有做到100%的覆盖便偷懒收手，值得反思。（也从侧面反映了互测中真的很少有人会通过看别人代码来找bug，否则这么明显只要看代码就白给的bug第一次互测应该是能被发现的）
修复起来也很简单，把最后的return -1;改成 return 1;就ok了，ORZ
规格撰写与理解的心得体会
首先，规格撰写方面，经过两次课上实验写规格的经历，感觉确实如水群中助教所说，写出一个优秀的规格对一个架构师的离散数学基础以及逻辑思维能力都有很大考验，因此JML并没有在工业界广泛推广。写规格时需要跳出程序员的思维，这一点在多次看规格之后才慢慢理解，规格里主要需要写出这个方法的功能，这个方法运行之后元素的状态，而不是在规格中写出得到想要状态的具体实现的过程，个人感觉，一个好的规格规定不是一个过程，也不是一个由具体实现过程推导的结果，而是用逻辑语言描述的结果本身。
其次，个人对jnuit单元测试的理解，我觉得jnuit的正确使用方式应该是在写代码前先按照需求写junit测试代码，这样既可以预先考虑这歌方法需要处理什么情况从而写出完善的代码，还可以边写边测试防止代码bug拖到最后才发现。
最后，吐槽一下，在三次课下代码中，我们并没有写规格的过程，而是按照给定的规格写代码，但实际操作时，我们完全可以通过读指导书以及指令操作知道一个方法需要实现什么样的功能，而且并不觉得规格比自然语言易懂清晰，反而出现了同学们通过对自然语言的理解提出了规格存在的bug（这也从侧面反映了优秀规格的难得和重要），那么这单元的作业实际上对JML的练习完全是依靠个人的自觉自愿来进行的，实际上，就算完全忽略规格，不使用junit还是可以很好的完成作业，因此个人感觉这单元并没有很充分的让大多数人练习到 jml 和 junit 的部分。