面向对象设计与构造 第三单元 总结
一、JML规格化设计
JML，全称The Java Modeling Language，是用于对Java程序进行规格化描述的注释性质语言。
笔者在本文总结了常见的JML语法描述。
1. 注释结构
在注释行或注释块中，以@开头的行被认作JML注释行。
//行注释
//@ ensures
esult == id;
public /*@pure@*/ int getId();
//块注释
/*@ ensures
esult == (sum int i; 0 <= i && i < people.length;
@ (sum int j; 0 <= j && j < people.length &&
@ people[i].isLinked(people[j]); people[i].queryValue(people[j])));
@*/
public /*@pure@*/ int getValueSum();
2. 模型字段
在行为描述中所能够使用的变量，与实现相剥离。
/*@ public instance model non_null int id;
@ public instance model non_null Person[] people;
@*/
| 关键字 | 描述 |
|---|---|
instance |
实例成员，只能通过类型的实例化对象引用。 |
static |
静态成员，可以通过类型引用。 |
non_null |
非空成员修饰。 |
3. 表达式
（1）原子表达式
| 表达式 | 描述 |
|---|---|
esult |
表示返回非void方法的执行结果。 |
old(exp) |
表示在方法执行前exp的取值。 |
ot_assigned(x, y, ...) |
表示方法执行过程中，括号中变量是否被赋值，没有赋值返回true，用于后置条件约束。 |
ot_modified(x, y, ...) |
表示方法执行过程中，括号中变量取值未发生变化。 |
onnullelements(container) |
表示container集合或容器对象中没有存放null成员。 |
ype(type) |
返回type对应的类型。 |
ypeof(exp) |
返回exp对应的类型。 |
本单元的作业中只使用到了前三种描述。
（2）量化表达式
| 表达式 | 描述 |
|---|---|
forall |
对应离散数学中全称量词的概念，表示给定范围内的所有元素均满足约束条件。 |
exists |
对应离散数学中存在量词的概念，表示给定范围内存在元素满足约束条件。 |
sum |
对给定范围内的表达式求和。 |
product |
对给定范围内的表达式连乘。 |
max |
给定范围内表达式的最大值。 |
min |
给定范围内表达式的最小值。 |
um_of |
指定变量中满足相应条件的取值个数。 |
较为常用的是前三种描述，下面是第十一次作业中对于求连通块个数的描述。需要注意的是，sum只对其后紧跟的表达式i进行范围遍历求和，而不应当理解为对i、j的遍历均求和；需要参与求和的表达式位于描述的最后，需要细致观察括号的匹配，避免误解规格。
/*@ ensures
esult ==
@ (sum int i; 0 <= i && i < people.length &&
@ (forall int j; 0 <= j && j < i; !isCircle(people[i].getId(), people[j].getId()));
@ 1);
@*/
public /*@pure@*/ int queryBlockSum();
（3）集合表达式
JML规格可以构造局部集合，一般形式为new ST {T x | R(x) && P(x)}，在本单元作业中并没有出现这种描述。
（4）操作符
JML可以正常使用Java定义的操作符，还包括如下几类。
| 操作符 | 描述 |
|---|---|
<: |
子类型或相同类型返回true。 |
<==> <=!=> |
类比离散数学中的等价。 |
==> <== |
类比离散数学中的蕴含。 |
othing |
作用域访问空集。 |
everything |
作用域访问全集。 |
4. 方法规格
（1）前置条件约束
requires：对方法的输入参数进行限制，是对用户使用该方法的约束。也就是说，用户输入参数不满足规范，方法的执行结果将不可预测。
（2）后置条件约束
ensures：对方法执行后的结果进行限制，是程序员实现方法所必须遵循的约束，保证方法执行结果的正确性。
（3）副作用
assignable：指定方法可以对对象的哪些属性进行赋值，常与
othing和 everything搭配使用，也可单独指定类中的一个或多个属性。
/*@ public normal_behavior
@ requires contains(id);
@ ensures (exists int i; 0 <= i && i < people.length; people[i].getId() == id &&
@
esult == people[i]);
@ also
@ public normal_behavior
@ requires !contains(id);
@ ensures
esult == null;
@*/
public /*@pure@*/ Person getPerson(int id);
5. 其他
（1）pure标注
/*@ pure @*/：表示方法不对对象进行任何改变。
一些博客中定义其不需要提供输入参数，指导书也疑似定义其不需要提供参数。作业中出现了需要输入参数且标注了pure的方法。笔者查阅了讨论区dalao提供的JML英文手册，pure方法应当是没有对输入参数进行约束的（但笔者英语水平有些鸡肋，理解可能有疏漏），参考链接：7.1.1.3 Pure Methods and Constructors。
笔者更倾向于简单地理解作业中的pure表述为assignable
othing，这种方法可以直接在其他方法规格中被引用。
（2）正常行为与异常行为
①正常行为
public normal_behavior：描述方法的正常执行行为，需满足其前置条件约束。
②异常行为
public exceptional_behavior：描述方法的异常执行行为，需满足前置条件约束，与正常行为的前置条件不能存在交集。
signals (Exception e) P：当进入异常行为且满足条件P，抛出异常e。
在异常部分中也可以使用ensures来描述方法的执行结果。
③also
also：存在两种使用的场合。
- 父类中对相应方法定义了规格，子类重写了该方法，需要补充规格，这时应该在补充的规格之前使用also。
- 一个方法规格中涉及多个功能规格描述，正常功能规格或者异常功能规格，需要使用also来分隔。
/*@ public normal_behavior
@ requires contains(id1) && contains(id2) && getPerson(id1).isLinked(getPerson(id2));
@ ensures
esult == getPerson(id1).queryValue(getPerson(id2));
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) !contains(id1) || !contains(id2);
@ signals (RelationNotFoundException e) contains(id1) && contains(id2) &&
@ !getPerson(id1).isLinked(getPerson(id2));
@*/
public /*@pure@*/ int queryValue(int id1, int id2) throws
PersonIdNotFoundException, RelationNotFoundException;
6. 总结
JML实现了对代码规格的严格约束，既避免了一般语言进行注释描述的歧义性，又与代码具体实现相分离，提高了代码的可维护性，在工程中有很强的实践意义。
二、JML测试
1. open JML
用于检查JML的语法。
笔者未能成功配置环境并且部署，且普遍评价都是该工具功能有限，无法支持复杂JML语法，已经有多年未维护，遂放弃。
2. JMLUnitNG
用于随机生成测试用例。笔者体验后认为这个工具只是生成了大量的边界数据与异常数据，覆盖性较差，并不能起到很好的测试效果。
3. JUnit
Java语言的单元测试框架，也就是“白盒测试”。
十分成熟的测试工具，且目前已经普及。在对程序基本功能进行测试时有很大的帮助，可以减少程序员的疏忽导致的Bug，但是难以做到复杂逻辑的覆盖性，适合于开发过程中使用。
4. 手动构造对拍器
针对作业进行数据构造，然后与其他dalao完成对拍工作，也就是“黑盒测试”。
这种测试可以模拟强测条件，较为全面地测试程序的鲁棒性，适合开发完成后使用。
对比白盒测试Junit与黑盒测试对拍两种方式：
| 白盒测试 | 黑盒测试 | |
|---|---|---|
| 使用节点 | 开发过程中 | 开发完成后 |
| 测试要素 | 功能性 | 功能性、鲁棒性 |
| 检查错误 | 低级代码失误 | 逻辑错误、程序性能 |
| 测试缺陷 | 单元测试编写与代码的思维一致，可能都对规格理解有误；复杂数据难以手动构造。 | 对拍的程序可能存在相同错误；很多情况下不一定存在可对拍的程序。 |
三、程序结构分析
本单元三次作业基本依据JML规格进行代码编写，对于类的层次化设计并不明显。前两次没有自行设计类和接口，第三次只设计了简单的Edge类和DijkstraPair类，因此没有绘制UML类图。
1. 第九次作业
（1）Network方法分析
整个关系网呈现一个无向图结构，人作为点，关系作为边，value作为边的权值。
contains(int id)：检查图中是否包括编号为id的点。getPerson(int id)：获取图中编号为id的点对应的Person对象，如果没有，返回null。addPerson(Person person)：向图中添加点。addRelation(int id1, int id2, int value)：向图中两点添加权值为value的边。queryValue(int id1, int id2)：返回id1与id2的边权值。queryConflict(int id1, int id2)：返回id1与id2的character异或值。queryAcquaintanceSum(int id)：返回id的邻接点数量。compareName(int id1, int id2)：返回id1和id2name的字典序比较。queryPeopleSum()：图中点的数量。queryNameRank(int id)：id的name在所有人中的字典序排名。isCircle(int id1, int id2)：id1和id2在图中是否连通。
（2）应用的数据结构与算法
- 多数方法需要对
id进行查找，如果使用List存储会极大增加查找开销，因此使用HashMap，id作为Key，person作为Value，存储熟人使用person作为Key，value作为Value。 queryNameRank方法直接采用遍历的方式计算rank，维护一个排序的容器会增大addPerson的开销，得不偿失。isCircle方法判断两点是否连通，使用广度优先搜索（BFS）算法，依靠Java自带的Queue接口即可实现，难度不高。- 使用了
circleCache在BFS过程中进行连通性缓存，但由于查找次数太少，缓存策略反而增加了时间开销，得不偿失。
2. 第十次作业
（1）新增Network方法分析
加入了组的概念，即子图。
addGroup(Group group)：添加一个子图。getGroup(int id)：获取图中编号为id的子图。addtoGroup(int id1, int id2)：向子图id2添加点id1。（方法名字应该写成addToGroup2333）queryGroupSum()：子图数量。queryGroupPeopleSum(int id)：子图id中的点数。queryGroupRelationSum(int id)：子图id中的边数量的2倍，加上点的总数。queryGroupValueSum(int id)：子图id中所有边权值和的2倍。queryGroupConflictSum(int id)：子图id中所有人character的异或。queryGroupAgeMean(int id)：子图id中所有人age的平均值。queryGroupAgeVar(int id)：子图id中所有人age的方差。
（2）应用的数据结构与算法
- 子图的所有信息均可以维护。
- 在
addtoGroup时，遍历子图中的所有点添加边和边的权值，在addRelation时，遍历所有子图，判断是否包含指定两点。由于子图上限10个，所以时间开销极低。 - 维护
age的总和、平方和，调用平均值与方差询问时直接计算，特别注意方差的计算不能直接化简到概率统计的公式，需要从JML描述展开，否则会出现整型变量的乘除运算误差。
- 在
- 子图上限人数是1111人，算是一个坑点。
3. 第十一次作业
（1）新增Network方法分析
在上一次基础上，能够删除子图中的点。
queryAgeSum(int l, int r)：询问age在l、r范围内的人数。delFromGroup(int id1, int id2)：从子图id2中将点id1删除。queryMinPath(int id1, int id2)：id1和id2间的最短路径长度。queryStrongLinked(int id1, int id2)：id1和id2是否存在于同一个点双连通分量。queryBlockSum()：图中的连通块个数。borrowFrom(int id1, int id2, int value)：借钱，金钱守恒，总数为0。queryMoney(int id)：询问id现有钱数。
（2）应用的数据结构与算法
- 对于删除子图点，可以继续维护。
- 不能使用
int维护age的平方和，因为age最大值为2000，800人的情况下会溢出，可以使用long或者遍历计算方差的方式，笔者采用了后者，与JML规格描述相一致。 money主要考察对JML的细致阅读，id2向id1借钱。- 询问
age范围内人数直接遍历，由于age范围比人数大，使用其他算法维护得不偿失。 - 更改了连通判断的算法，由于不存在删除点和边的请求，可以使用
ArrayList存储每个点所连通的点，处于同一连通块的点共享一个容器对象引用。本质为并查集的思想，并且对连通块总数进行维护。- 添加点时，增加一个连通块，并将点放入。
- 添加关系时。
- 若两点的
ArrayList引用相同，不需要修改相关维护变量。 - 若两点的
ArrayList引用不同，使用addAll方法，将size小的集合向size大的集合合并，并更新size小集合的所有id的并查集为size大的集合，确保对象引用的共享。
- 若两点的
- 为每个点新增严格递增的顺序编号，使用
HashMap和ArrayList进行点的双维护查找。 - 最短路径使用堆优化的Dijkstra算法，基于优先队列
priorityQueue实现，新建了DijkstraPair类存储结点编号与当前最短路径情况，实现Comparable接口。为了增加访问性能，使用了数组存储最短路径值，每次查找使用Arrays.fill方法对数组赋予Integer.MAX_VALUE初始值，但事实上性能略逊于不初始化的空HashMap。 - 点双连通分量使用Tarjan算法，DFS的过程中将边
Edge压入栈中处理，同样使用数组增加访问效率。JML规格中约定了2点的点双不算在范围内，因此特判。 - 笔者参考的链接：浅谈Dijkstra、无向图的割点&&点双联通分量(Tarjan算法)总结。
4. 一些细节优化
一些作业中使用到的细枝末节处理，对整体性能影响很小。
（1）HashMap的一些特性
①HashMap的三种遍历方式
- 使用
keySet，每次使用get方法获取Value。 - 使用
entrySet，可以直接获取Key与Value，且遍历效率最高。 - 使用
values，直接获取Value值，遍历效率最低。
②HashMap的查找
containsKey：复杂度(O(1))，最坏情况(O(n))。containsValue：复杂度(O(n))到(O(n^2))之间，所有Value都分布于单独Key时为(O(n))。
笔者第九次作业误使用了containsValue方法，导致CPU时间略高。
（2）集合对比
- 数组的修改效率要高于
HashMap的put方法，put方法存在一定复杂度，基于HashMap的HashSetadd方法同理。 ArrayList的遍历效率高于HashSet，因此共享容器使用了ArrayList。- 使用下标遍历
ArrayList效率略快于使用foreach遍历。
（3）其他
- 对容器的容量进行初始化设置，可以减少扩容开销。
Arrays.fill方法类似于C语言中的memset，用于对数组的初始化，但实际可以使用空的HashMap实现最短路径的记录。
四、程序Bug分析
1. 第九次作业
- 自测：没出现Bug。
- 中测：中午开放后准时提交，全部通过，但官方修改了评测机后错了两个点，是发布作业后的JML规格有修改所致，与评测机错在一个地方了。
- 强测和互测：没出现Bug。
- 互测中其他人情况：只发现了一个Bug，在使用
isLinked询问两点连通时，一边对已有熟人遍历一边判断是否连通自己，在没有熟人时跳过了自连通判断，直接返回了false，随机数据下屡次复现。
2. 第十次作业
- 自测：在与其他dalao对拍时发现了方差化简过度导致出现误差的Bug。
- 中测：没出现Bug。
- 强测和互测：没出现Bug。
- 互测中其他人情况：共发现4位成员存在Bug。
- 维护子图变量错误的Bug。
- 手动构造(O(n^2))复杂度下最耗时的查询子图
value和的数据，发现两个超时Bug。 - 手动构造存在大量连通性询问的数据，发现了
isCircle超时的Bug。
3. 第十一次作业
- 自测：点双时没有特判两点情况，但是强测也没有出现此类数据，出现概率很低。
- 中测：没出现Bug。
- 强测和互测：没出现Bug。
- 互测中其他人情况：发现2位成员存在Bug。
- Tarjan算法或者其他地方出现时间复杂度超高情况，随机数据几乎全灭，手动构造了qsl指令测试，本地唯一一个出现了结果的数据跑到了120秒。
- 维护平方和使用了
long，且在计算方差时没有将第二项进行强制类型转换，导致第二项结果为int且溢出。该Bug由于互测数据数量的限制无法hack，同样是手动构造发现。
4. 实验
笔者很不幸在本单元第二次实验的唯一一次补交机会中出现了编译错误的情况，这也是笔者这学期第一次出现编译错误，就是如此的巧合——查询错误根源，是笔者的单元测试中出现了手滑打错自动导入的Java Oracle且被IDEA默认折叠。
百密一疏，但这其实是在警醒笔者CheckStyle的重要性（发现无用导入报错）。不论是作业还是实验，甚至于今后的工作，都应当做好代码风格的检查。
5. 关于CPU时间
笔者建议评测机开放一个测试CPU时间的窗口，只提供输入和运行服务，设置使用CD。
由于笔者CPU主频与其他dalao相差甚远（测Tarjan超时时疯狂咆哮），在第十次作业本地测试时认为算法实现存在一些难以发现的错误，后发现是CPU差异所致。高频CPU也不一定与评测机相一致，因此希望有个统一的标准来检查程序运行的时间是否符合预期并相应作出优化。
五、总结
第三单元笔者也有所收获。
- 有些领悟“契约式”编程的思想，并且体会规格与实现相分离的编程方式。
- 重温了图论的一些经典算法，并且学习了Tarjan点双连通分量。
- 细节决定成败，忽视掉任何一个细小的地方都可能会产生致命的错误。
同时存在一些需要改进的地方。
- 这单元的重点都聚焦在了算法的设计上，而略微忽视了架构，虽然没有重构，但如果把算法单独封装起来会更佳。
- 还需增强代码阅读能力。
另对JML有些主观的评价：JML虽然对规格进行了约束，但是书写JML比书写代码更为复杂，且不易理解过于复杂的JML逻辑，有些本末倒置的感觉。JML的工具链非常不成熟，且无人维护，网络上的JML信息大量来自于往年的OO博客，说明JML本身也没有得到普及。
很感谢老师助教们的辛勤付出，给笔者带来了良好的课程体验，并且及时解决笔者的问题与困难。OO课程到了第三单元的确存在不成熟、不完美的地方，需要时间来不断改进，笔者希望今后的OO能够更好。