OO_Unit3总结

一、JML情况

理论基础

JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言，为严格的程序设计提供了一套行之有效的方法。通过JML及其支持工具，不仅可以基于规格自动构造测试用例，并整合了SMT Solver等工具以静态方式来检查代码实现对规格的满足情况。

JML有两种主要的用法：

（1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。

（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。

由于本次作业中未涉及JML的类型规格，故下文不做进一步讨论。

在JML最核心的语言特征，即level 0中，JML构建了一套完整的语法体系，在这个语法体系里，我们使用表达式来表示方法执行过程中可能涉及的数据，使用前置条件、副作用范围限定和后置条件构建了方法规格。这样做的意义是多方面的，其一给规格的设计者以合理的表达方式，剔除了自然语言的模糊性的前提下，使得规格的设计者需要更全面的思考以涵盖需求的各个方面；其二为规格的实现者指明了实现的方向，通过阅读JML可以直接从逻辑上理解方法应该做到哪些方面；其三为测试人员测试代码提供了途径，测试人员测试代码时只需要判断方法是否实现了规格，而这在一定程度上可以由工具代劳，减少了程序测试对人的依赖。

应用工具链

OpenJml：用于检查JML语法

SMT Solver：检查实现和规格的等价性

JMLUnitNG：基于JML的单元测试工具

二、关于SMT Solver

第一次尝试：在阅读了往届博客以及其他同学的博客之后，我已经对其不报太大希望，由于SMT Solver只能做静态验证，我选择了第一次作业的Person.java进行验证，因为其方法不是很依赖以往的执行情况。第一次尝试以发现JML域和java域不能重名告终。

第二次尝试：修改了JML域的名称后我进行了第二次尝试，使用z3-4.3.2.exe，得到了以下报错信息。

使用另外两个exe运行得到了以下报错信息。

在善用搜索引擎后，我发现这些错误我无法处理，遂放弃。

三、关于JMLUnitNG

修改了Group.java和Person.java，去除了其缓存机制，保证每次调用对应方法时不依赖以往的执行结果，使之能适应JMLUnitNG的要求，依次输入下列指令

 java -jar jmlunitng.jar test/Group.java
 javac -cp jmlunitng.jar test/*.java
 java -jar openjml.jar -rac test/Group.java test/Person.java
 java -cp jmlunitng.jar test.Group_JML_Test

得到如下信息：

看起来除了第一个不明意义的fail之外其他都passed了，这在我的意料之中，因为修改后的代码照搬了jml的定义，是最原始的实现方法。

但是我注意到，这些信息中传入的参数不是INT_MAX，0，INT_MIN就是null，这似乎是希冀于边界数据能够测出程序的问题，通过阅读其他同学的博客可以发现，这似乎就是其所有的测试策略。我认为这对于一个工具而言只能是不合格，可能存在其他的测试方式我没有找到，希望其他同学看到后可以补充。

四、架构设计

基本架构已经由JML给出，几次作业只需要注意容器的选择和方法采用何种算法即可。

hw9

MyPerson中，由于频繁出现根据id访问对应的person的需求，兼之考虑到，person和value的一一对应，故采用了HashMap<Integer, Pair<Person, Integer>>，以id值作为键，person，value对作为值保存。
MyNetwork中，由于也需要根据id访问对应的person的需求，且有遍历people的需求，故牺牲空间，同时维护HashMap<Integer, Person>，ArrayList< Person >两个容器，但这也同时牺牲了addPerson的时间，故最后结果孰好孰坏取决于输入情况。
isCircle的实现使用了最简单的bfs，因为并查集如果涉及delRelation我还不会处理，故采用保守策略。

hw10

新增了Group相关代码，为了提高相关方法的效率，我采用了缓存中间变量的做法，每次增加人时更新这些变量。但这种方式有一定局限性，如果person先加入group再加关系，就无法更新relation相关的中间变量。为此，只得牺牲部分封闭性，给MyNetwork以更新这些变量的能力。
需要注意求方差的数学公式不能过度化简，否则会和JML的精度相悖。

hw11

这次作业着力点在于对图的相关算法的考察，分别是求最短路，求点双连通分量，求连通块数量。
求最短路我采用了dijkstra算法，测试后发现时间复杂度较高，在询问其他同学后使用了优先队列，优化了dijkstra过程中获取最小值的复杂度。
点双连通分量我采用了在讨论过程中牟钰同学提出的一种方法，即遍历每个点，如果删去这个点后，id1和id2不再连通，则这个点是割点，如果不存在割点则点双连通。需要注意两点，一是，两者仅直接相连的情况不符合题意，不能被这种方法排除，只能另行判断；二是，可以先bfs找到一条路径，再遍历路径上的点而不是全部点，因为割点一定存在于所有路径上。

Bug相关

在第一次作业中，由于理解JML时出现偏差，对isCircle的异常处理顺序错误，导致某种应当抛异常的情况被我漏过去了，因此第一次作业强测仅得了40分。让我充分认识到了中测=不测的事实，在后两次作业中更谨慎地读JML。
第二次作业强测没有出现问题，在互测中被hack了tle，因为isCircle方法太暴力了，没有充分利用person的acquaintance，导致时间复杂度较高。
第三次在吸收前两次教训的基础上谨慎读JML且注意各个方法的时间复杂度，最后没有出现问题。
互测hack他人的策略就是利用自己的随机数据生成器，大量生成随机数据对其他成员进行测试。第一次测出了其他6名成员的8个bug，第二次也测出了其他成员的tle问题，第三次测出了一位同学的tarjan算法的实现问题。

心得体会

JML似乎给出了一种理想的契约式编程的方式，在分工明确的基础上，一部分进行规格设计，一部分进行代码实现，使得架构设计可以被形式化验证，为我们写代码提供了正确的方向。

三次作业出现的bug也证明了这一点，没有正确实现规格->强测40分；没有高效实现规格->互测被hack；正确且高效地实现规格->没有问题。我对JML的作用的认识依次增加。

但是我也认识到了JML的一些不足。

其一是读JML：读JML需要理解规格所用的谓词逻辑语言，虽然保证了不存在歧义，也大大加大了读JML人的理解难度。在离散数学里，我们有许多定义，如连通分量等，就是为了每次表述这些高频使用的概念时不用每次都写一长串的表达式。因此我觉得JML也应该有一些高阶表达式以类似自然语言的形式描述相关要求，并且由于这仅仅是一种助记符，自然语言的歧义性也不存在，对写规格和实现规格的人都更友好。

其二是工具链的不完善：理想情况下，我们可以，1.写出规格并用相关工具验证正确性；2.实现规格并用相关工具验证等价性；3.测试代码以完成对规格的补充。然而这三方面我均没有看到有好用的工具。

这两点都需要更多的人参与开发JML的工作，希望在今后能看到JML继续发展，给我们带来更好的体验。