在本阶段的OO实验中，我们首次接触到了JML语言，也帮助我们学习了设计和实现的一般流程，将设计时的架构和实现时的细节分离开来，使具体需求更加明确，也降低了错误出现的概率。
JML语言(Java Modeling Language)用于描述程序中接口的规格，从而规范模块的具体行为，它提供了严格的形式语义，相较于自然语言更加无二义性，从而防止了模块的设计出现歧义。
JML主要用于 开展规格化设计，帮助代码实现者更好地理解设计需求，实现逻辑严格的程序 和 对已有代码书写规格，提高代码的可维护性。
在本单元的实验中我使用到的工具主要有以下几种：
在本地配置的过程中，由于奇怪的版本原因没有部署成功，于是选择了在服务器上部署使用
使用的Demo代码如下：
通过生成测试文件，编译生成文件，用jmlc编译自己的文件，测试，等几个步骤实现了通过JML生成测试样例对程序进行测试，这些步骤中使用的bash如下：
在本测试过程中，由于没有考虑算数溢出等情况导致了错误样例的产生。
可以看出的是，JMLUnit在自动生成样例的过程中，更多地考虑了对于极端条件的组合
本单元作业从PathContainer到Graph再到RailwaySystem是一个需求逐渐提升的过程，加强了我们对于OOP设计思想的体悟，也使得在完成作业的过程中需要良好的架构来支撑增量式设计。
在第一次作业中为了避免超时现象的产生，使用了两个HashMap(Path->ID,ID->Path)的方式来提高查询的效率。同时在Path中使用了一个HashSet来存储不同的结点数，在Container中使用了一个HashMap来存储不同结点及其出现次数，来优化查询独立结点数时的效率。
本次作业中架构较为简单，复杂度的控制也较为合理，就不贴图了??
在本次作业中主要需要设计优化的是对于最短路径的求解问题，由于本次作业中的图权值相等，所以我采用了BFS进行求解。每次算出从该出发点到图中其他所有顶点的最短路径，并将其缓存下来，提高后续查找时的效率。
在架构设计上，我将无向图及其计算部分以一个类单另完成，相对于上一次作业在PathContainer中增加了对于无向图计算的调用。
在复杂度控制上，BFS计算方法的逻辑判断较深，复杂度稍高。
在最后一次作业中增加了很多需求，主要是边权重变化和换乘的计算。在这次作业中我主要使用的拆分换乘点+带缓存的dij算法，在实现上新增了3个图计算类，在其他部分基本与上次保持一致（??????修改的地方也导致了此次bug的产生）。虽然有bug产生，但是程序运行的效率还是可以保证的。
在类的设计上，使用Graph类无向图的生成和完成带缓存的dij计算，继承出三个特定图PriceGraph、UnhappyGraph、TransGraph来设置边权重不同的生成方式。
在复杂度控制上，
两个图计算相关的方法的复杂度较高
在类的复杂度控制上，没有对MyRailwaySystem和图计算类Graph这两个类进行很好的拆分，单类中需要实现的功能过于复杂，也导致其复杂度较高。
在本次作业自我测试中，主要使用了自动化对拍+Junit的测试方式，在代码覆盖和正确性检查方面也具有一定的可靠度。在前两次作业中也没有出现问题，在第三次互测中，本以为还是云淡风轻的季节，直到有老哥交出了4/7??......
在公测结束后回头查看问题，发现是我在核查第三次作业中，由于希望节约查找时间，对第一次作业中MyPath类中判断本节点是否属于Path的方法进行了更改。
由于我的distinctSet是Lazy更新的，只有当调用PATH_DISTINCT_NODE_COUNT时才会进行计算，导致在这之前distinctSet都是空的????
在强测过程中也因为这个问题导致了18个点WA，感谢能让我踩线进C组互测赚分
回过头来反思自己在自我测试中出现的问题：
在规格化设计上，JML能够很好地起到约束的作用，也能帮助我们建立起规格化设计的思想。
在测试上，本单元作业的完成过程中，使用了Junit来进行单元测试，也使用了对拍器来验证程序的正确性。另外，第三次作业翻车也是一个惨痛的教训，在今后的代码完成和修改过程中，一定要充分思考再下手；在代码测试的过程中，不能偷懒，对于所有的代码都要进行测试来保证正确性。
原文：https://www.cnblogs.com/lebway/p/10905162.html