OO第三次博客作业
(1)jml基础知识梳理：
常用：
pure：
纯粹查询，无任何副作用。
数组：
仅仅是规格层次的描述，不一定有数组定义。
no_null:
该容器不能为空。
esult：
该方法返回的对象。
require：
前置条件，即调用该方法时参数以及成员变量需要满足的条件。
assaignable：
副作用范围，列出所有可能会被修改的成员变量。
othing：
空
ensure：
后置条件，即调用该方法之后参数和成员变量需要满足的条件。
old()：
表示调用该方法前的该对象或表达式的值。
ype()：
表示该类(type)的类型(class)。
ypeof()：
表示该表达式的类型。
forall()：
相当于数学中的"任意"符号。
exits()：
相当于数学中的"存在"符号。
<=, =>, <=>：
推理。
public_normal_behavior：
正常功能规格。
public_exceptional_behavior:
异常功能规格。
also：
分开正常和异常两种规格。
signals () ___ :
满足条件抛出异常。
jml工具运用：
本地装的jdk11和eclipse4.8.0无法使用openjml：
询问林佬之后得知需要在jdk8和jdk11之间切换两次才能跑完，windows未能找到此功能，遂放弃。
jml uniting/jml unit使用：
本人一直在作业中使用自动生成大量数据对拍，而openjml都运行不起来，无力使用对jml的单元测试，遂放弃
第三单元架构迭代分析：
第九次作业：
MyPath类：
使用了Hashset来记录点，以实现快速查询点数和点是否存在。
PathContainer类：
使用了两个HashMap互相映射path和id，方便查询点数等。
第十次作业：
Mypath类:
不变，继承第九次作业。
Graph类：
继承第九次作业的PathContainer，添加建图和BFS，建图使用邻接表，点的id进行映射，以便使用静态数组，提升效率。
第十一次作业：
MyPath类：
不变，继承第九次作业。
MyRailwaySystem类：
继承第九次作业，添加并查集完成除最短路以外的查询。
Tu类：
新添加的类，完成建图、最短路查询，在MyRailwaySystem中完成四次实例化，来计算四种不同的最短路，最短路使用拆点+SPFA。
代码实现&bug修复：
代码实现：
基础的path相关的查询和插入使用HashMap来存储、查询。
连通性使用并查集查询。
最短路新开类Tu实现建图和查询，建图使用拆点+邻接表，因为边数少，点数多；最短路算法使用spfa。
拆点具体做法见传送门
bug修复：
无bug。
规格撰写体会：
首先看是否会异常，即，是否对不满足前置条件的情况进行异常抛出。
其次，写出前置条件和后置条件，理清思路和方法需要完成的工作。
最后写返回值。
这样的顺序能够使条理更加清晰，工作量更小。
就像OS中的注释，虽然也有前置条件和后置条件，但是没有一个很同一的格式来约束，导致写出来的注释没有jml那样规范，而且很容易出错，对写代码的人造成误解。