18373599 崔建彬
一、概述
第三单元主要完成内容为根据jml给定规格完成代码。整体而言较前两单元难度有下降，主要难点在于jml理解和算法优化（数据结构复习）。比较幸运的是我在这个单元的强测和互测中，均未发现bug。本问剩余内容也将从JML语言概述、部署SMT Solver进行验证、部署JMLUnitNG、按照作业树立自己架构设计、按照作业分带啊吗实现的bug和修复情况、阐述心得六个方面进行讲解。
二、梳理JML语言的理论基础、应用工具链
（如果以后有学弟看到了我的博客，想学习jml基础知识可以看这个网址https://blog.csdn.net/weixin_41412192/article/details/89527142 ）。
在我的理解中，jml就是规范的规格。通过jml告诉编程者，这个功能需要什么前提，要做什么功能，实现以后是什么样子。使得程序员可以通过直接看jml，不用额外的交流，就明白要完成什么。
要说优点那很清楚：有一种规范的统一的规格语言，读起来感觉就和离散数学一样，同时读多了也会觉得很简单明了，如果写的jml正确，那基本没有二义性。可以有效地解释一个函数的功能。
当然，这么好的东西也会有一些缺点：就是书写jml过长，通过这单元来看，经常出现jml代码长度远长于实现长度（辛苦助教了，想想就可怕）。同时，jml长度长也常常伴随阅读困难，理解困难。有时候简单的向一个类中数组加入一个元素，就需要写非常长的长度。这些也给jml的使用造成了不便。同时，通过查阅jml工具链相关资料，我们也可以发现jml的相关工具链不是很成熟，大部分都是停更/待埋坑，可能也是上述因素导致了jml最终没有普及。
jml作为我们第三单元内容，肯定不是为了精通jml，方便以后使用。更多的是理解其思想。了解一种java的规范式语言，有了jml这种规范化语言的约束，我们就可以更好的进行形式化验证、在团队合作中更为精准的知道别人需要我实现什么功能，也便于更好的找到bug，
应用工具链：
jml虽然新的及时更新的工具不是很多，但还是有不少工具链的。比如openjml。openjml可以对jml进行规范性检查。同时，其所含带的SMT solver可以对代码等价性进行检验（虽然我跑不成功）。
除此之外还有JML UNit。结合Openjml时候，可以实现对代码的自动化测试。主要是边界性测试。
下面就简单描述一下使用这些工具链的心路历程（悲惨历程。
三、SMT Solver进行验证
首先安装JML，从该网站下载zip包 https://github.com/OpenJML/OpenJML/releases/tag/0.8.46 （令我没想到的是，作者居然还在持续更新）。
此处安装 方面特别鸣谢：j哥，附上他的安装教学：https://www.cnblogs.com/pekopekopeko/p/12920417.html#4581709
Sovler是验证代码是否与jml符合的。但是在运行相关指令时，会疯狂报错jml规范问题，同时，因为前三次实际作业中，JMl与代码是分离的。为了更好的做展示，我使用了Person.java，并将部分函数魔改，加入自己实现代码，来测试Solver的功能。
（后来发现是中文路径的问题。）
上面只是简单的魔改Person，只剩下了9个警告，也算是功能测试成功了吧！
四、JMLUnitng测试
jmlunitng是为了自动化生成数据测试。但是因为实际中，无法直接利用我们前三次作业的规格和代码进行测试，会疯狂报错，为了体验JMLUnitng功能，我继续重写简单版Perosn.java，并在JML下面补充代码，来进行测试。
1.java -jar jmlunitng.jar test/Person.java 输入这个指令得到了如下图所示
2. javac -cp jmlunitng.jar test/*.java，将其编译
3.java -jar openjml.jar -rac test/Person.java
4.java -cp jmlunitng.jar test/Person_JML_Test
下图为最终结果：
都是失败和跳过（
而且即使得到这个结果，我自己也在原来的基础上魔改了很多，也算是尽力了吧（
但是很显然，只能进行一些简单的为了测试一些代码。并没有起到很好的辅助/减轻工作量的效果。主要原因应该是工具链还不够完善，期待后续能看到他们有较好的使用效果。
五、自己的架构设计
其实大的设计架构，比如分为Person Network这种类，Network处理所有Person之间的各种联系，这种事情都是JML已经给出了，我下面简单的过一下，这些大的框架，具体将选择几个较难的函数，
HW9:
从类图来看，整体构造比较简单， 就只有MyPerson和MyNetwork两个类，整体不复杂，耦合度来看，MyNetwork集成的功能较多，本单元最难的函数应该是isCircle，是一个简单的无向图连通性，使用bfs/dfs/并查集都可以解决，如果用了并查集，HW10、HW11中某些函数还可以做到算法用时更短。整体来说，并不复杂，更多的是理解JML语法和内容。
HW10:
从类图来看，依然是 NetWork比较臃肿，承担了绝大部分功能。这次作业新增了组类Group，并通过MyNetwork调用了MyGroup中的方法函数。这次作业整体难度适中，增加难度适中。我认为重点训练我们不能单纯根据JML规格写函数，而实理解JML要求的内容，并通过自己的想法来尽可能减少所需要的时间。所以在Group中，几乎每个函数我都用了缓存的处理，每当向group中增加一个人时候，我就更新一边年龄和、冲突值等等，通过将添加人的复杂度升为o(n),使得所有函数复杂度都变为o(1)，来避免达到6.66s的界限。
值得一提的是，就算方差也可以用缓存的方式，我们只需要记录下年龄平方的总和sum2,在求方差的时候利用公式： 方差 = （年龄平方的和 - 2 * 平局年龄 * 年龄的和 + n * 平局年龄的平方）/ n。 所以，Group中所有方法的复杂度都降到了O(1)。
HW11:
从类图来看，本次作业并无新增类（Node是为了方便我用堆优化dijk算法而写的）。同时。也可以看出，Network依然很臃肿。本次作业新增Group类删除功能，和Network一些功能。重点难点在于Network新增功能要在有限时间内跑完。
Group删除功能比较简单，注意多多测试一般不会出现大问题。难点主要集中在求连通块块数，强链接和最短路径上。
由于时间限制。最基础的dijk求最短路径可能有点慢，所以我选择了用小顶堆优化方法，降低复杂度。（虽然都是抄板子）。类似小顶堆的容器我选择java自带的优先队列，整体写起来比较顺利，不会出现超时情况。
求连通块个数这个函数主要难点在于读懂jml，事实上要不是同学给我讲解和函数名的按暗示，我确实没猜到这是求连通块。这个函数的实现方法也是非常的多，网上也有现成的板子。但最后为了方便我选择用dfs实现，整体复杂度在o(n)左右，也比较快，当然很多同学选择了连通块，那自然会更快。
最后是求强链接：即无向图中任意两个点都可以有两条截然不同的路径。这个函数许多同学用了tarjan算法。但听说助教的本意不是这样，可以遍历地图中所有点，依次删掉每个点，看看删掉以后，用iscircle看看两点之间是否还能通。如果不能就不是强连通的。但是考虑到我的iscircle是bfs，如果全跑完肯定很慢。所以可以先用bfsdfs跑出一条通路，再依次删除通路中的点，看看能不能满足，这样一来时间复杂度就降低了很多，也不会超时了。最后这个函数还需要注意一下如果两个点直接相连该怎么办。这个直接特判就ok了。
六、作业中的bug
本单元中，均未在强测和互测中发现bug。
课下采用的检查方式为：黑盒测试为主+辅助人工核对JML与代码是否行为一致。
同时还要注意边界测试+算法超时测试。
黑盒测试：这个单元的评测机就好写很多了，因为是单线程的。测试强度主要取决于测试数据量和生成函数。检验正确性的方式为：和多个同学对拍，这样就不用自己在评测机中维护一个新的图，也不用de评测机bug。但是生成函数有时候容易出问题，比如第二次作业中，有些同学的生成函数没有生成测试isCircle的指令，导致出现了分数低甚至0分的现象。但总的来说，这个单元的黑盒测试难度应该不高（白嫖使我快乐）。
人工核对：顾名思义，就是反复对着JML和自己代码看。让我印象深刻的bug就是第二次作业中，有个group人数>=1111就不再往里添加了，许多同学没有看到，使得他们在强测中没有取得良好的成绩。这个bug采用上面的黑盒测试显然是不容易被发现的。或者发现也要看运气，所以由此可见，人工核对代码和JML还是很关键的。
除此之外，本单元最大的难题还在于容易超时，似乎从第二次作业开始，有了较强、对算法有一定要求、不能按找JML硬抄的函数。比如isCircle，和第三次作业中的求连通块、最短路径和强链接等。这些都要求你对自己写的代码的时间有一个预估。大部分情况O(n^2)复杂度的都会被卡（但是第二次作业中助教似乎没卡到），除了采用合适的算法，也要用记忆化等方式，使自己的程序避开tle。我在除了第三次作业中，有的数据跑到了1.5s（因为第三次作业犯懒了）其余的都不会超过1.5s,还是很稳的。
最后就是边界测试：在本单元中，前两次作业的边界测试主要围绕着极端数据是否超时，这个都比较容易想到，可以归结为超时测试。但是在最后一次作业中，有的同学因为，加入的人的年龄可以达到2000，又用了记忆化存储，存储了年龄的平方和，导致最大达到32亿，超过了Int的范围。很奇怪的是，我在本地测试时候，这样并不会影响结果的正确性，但还是有同学因为int存储，强侧炸了10分。这也是边界测试偷懒了的结果。
综上所述，注意实现了JML的要求，注意算法超时问题，大量黑盒测试+（如果你想的话）手动生成的边界案例，就很容易做到0bug了。
七、总结
对规格的撰写
虽然在作业中未要求我们写jml，但是在试验中，仍然体验了一把写jml的感觉。整体来说，可能因为不够熟练，难度要大于填充代码。需要思考require部分、是否有异常可能、是否有多种情况、如何表述清楚自己的想法、是pure方法还是需要对其他内容有修改、需要思考ensure部分怎么表述最准确。这些都不是十分容易的事情。需要你对函数有非常清晰和完全的认识。由此可见，这个单元的助教有多惨（
理解上的心得体会：
JML确实要比语言描述严谨。是一种统一的规格化语言。如果让我用汉语来描述这个函数功能，我可能能做到2行就完成JML20行的内容，但是确实很容易有二义性，可能1000个人中对我这个函数的功能有10种不同理解。而用JML写就很好地避免了这个问题，如果你和我理解的不一样，那就是我们中有人JMl学错了（
最后：
总的来说，这个单元作为JML的单元，还是给我大开眼界，让我知道了JAVA中也有这种规格化语言，虽然好久没有人跟进了（因为一百度，全是17级博客）。理解JML的内容，并按照需求完成代码，大部分同学都能做到。更难的是如何做优化，所以在我看来，这个单元还像是数据结构复习，让我复习了dijk图搜，bfs，dfs等。可能也是因为不需要3次作业，要想每次作业都在上一次作业难度上有上升，只能做成这样，在算法上稍微要求一下同学们。相信这个单元助教确实很难（