OO第三单元总结

---

1.1 JML理论基础

• 我觉得就是《离散数学》中的数理逻辑
• 由于我的《离散数学》是速成的，导致我不会写规格，只能勉强读读，因为写规格和写代码的逻辑完全不一样，第10次作业我就傻逼了。

JML知识点总结：

• pure：

  纯粹查询，无任何副作用。

• 数组：

  仅仅是规格层次的描述，不一定要数组实现

• no_null:

  该对象不能为空。

• \result：

  该方法的返回值。

• require：

  前置条件，即调用该方法时参数以及成员变量需要满足的条件。

• assaignable：

  副作用范围，列出所有可能会被修改的成员变量。

• \nothing：

  空

• ensure：

  后置条件，即调用该方法之后参数和成员变量需要满足的条件。

• \old()：

  表示调用该方法前的该对象或表达式的值。

• \type()：

  表示该类(type)的类型(class)。

• \typeof()：

  表示该表达式的类型。

• \forall()：

  相当于离散数学中的"任意"符号。

• \exits()：

  相当于离散数学中的"存在"符号。

• <=, =>, <=>：

  离散数学中的蕴含，等价等

• public_normal_behavior：

  正常功能规格。

• public_exceptional_behavior:

  异常功能规格。

• also：

  分开正常和异常两种规格。

• signals () ___ :

  满足条件抛出异常。

1.2 JML工具链

• 首先我在世界最大的搜索引擎搜索了“JML”关键词

  可见JML的应用程度之高，工业化应用的广泛。

• 其次我打开了JYC的博客【图略】

  当我发现配置如此复杂的一个工具链，得到结果也不尽人意的时候，我借用JYC的一句话：

  至少我觉得，如果让程序员抛弃程序效率，抛弃程序简洁度，甚至说是抛弃程序能否满足课程组要求（算法时间之类的），去满足一个比较低下的工具，我真的觉得本末倒置。

• 再借用ZYY助教的一句话

  遂放弃。

• 当我听到这个东西可以自动测试时，我的内心是激动的，至少我以后不用JUNIT写测试类了？

• 然后我打开了世界最大的搜索引擎搜索这个工具

  我发现了这么一个知名的高star、高fork的开源项目，看了看文档，下载下来不会用，遂放弃。

  (我还是老老实实肝对拍，老老实实写单元测试吧。)

3.1 第九次作业

这次作业是JML系列作业的第一次，我对JML的构架理解很浅，再加上需要实现的方法除了一个isCircle以外都是查询和添加之类的简单方法，我就机械的照着JML规格的格式，翻译了一遍，由于评测也没有卡复杂度，所以摸过了，无bug。

3.2 第十次作业

这次作业是JML系列的第二次，第一次吃了甜头，就不以为然，还是机械的照着反应规格，于是获得了强测0分的好成绩！

当我修复Bug的时候，主要发现了以下几个问题：

• 那一周我确实比较摸，有好几处规格的细节读错了。

• 容器全是ArrayList，查找只能遍历。

• 计算一些可以重复获得的值我全是一次一次算。

  导致了就算我把细节改对，运算时间也比别人慢了几个数量级，是我输了。

  经过我反复的重构，把ArrayList全换乘HashMap，又做了动态存储一些值，我终于修复所有bug，也为第试一次作业做好了铺垫。

3.3 第十一次作业

首先，我三次作业的基本构架没怎么变，都是实现了三个类 ;

第三次作业由于求最短路需要数对的数据结构，于是搓了个类。

这次作业相比于前两次作业主要多了从Group中删除Person和几个图算法的操作，删除Person操作较简单，都是O(1)操作；主要说说三个图算法：

• 求最短路径

  我这里使用的是dijkstra算法+堆优化的思想，直接把我C++的板子改了改，其中堆用的是Java自带的优先队列，还行。

• 求联通分量的数量

  我这里使用的是并查集的数据结构，在每次addPerson时更新并查集，每次请求的时候统计。

• 判断两点是否点双联通

  我一开始使用的是两次DFS的方法，虽然复杂度只有O(V)，但是这种算法存在着正确性问题，有可能前一次DFS会堵了之后的路。遂放弃。

  之后在OI_WIKI上看到了一个叫tarjan算法的东西，但是他找割点的方法我没怎么看懂，就没抄。

  走投无路，为了保证正确性，采用DFS回溯的办法进行暴力枚举，虽然正确性可以保证，但是时间复杂度高达O(V!)，神仙也救不了我。

  提交时间过了之后，有人发了其实枚举所有点都当做割点跑一遍就行了（O(V^2)）。我是傻逼。

  那咋办么，我都抱着强测0的想法交了，结果还进互测了，还被大佬刀了7刀。

  最后结果强测75(不得不说，ZYY永远滴神，强测数据出的真好)。

  BUG修复那就很简单了，抄个tarjan?或者枚举所有割点跑dfs，好像都成，不过第三单元既然都过去了，留点遗憾也好，吃一堑长一智，BUG就当我给大佬大礼包了，我不修了。

• 本单元作业结束了，我理解了规格的重要性，也体会了单元测试在实际开发中Debug的效用。<不过JML工具链真的是阴间玩意>

• 单从读规格来说，规格只是告诉你，用户提供满足规格的输入，你就得提供什么样的输出，至于你如何实现完全不Care。至于写规格，这就是一个十分数学化的东西了，跟DF Ma老师学几年再来吧，只有理解了形式化的东西，才能写好规格，对于一些对正确性要求很高的软件，你甚至要用形式化语言证明这些东西。

• 以后我立志当产品经理，你们开发的和测试的都得给我整JML

• 最后感谢各位老师助教和大佬对我的指点和支持(@ZTY老师 @GYF助教 @Hangsbug @蓝头像 @胡歌滚 @笑死羊 @林雨桐 @prime21 @t123yh @bear @cjb @wpb @my @yzm @jyc @kongyou………)