一、JML规格理论基础
-
JML 中常用的表达式：
-
\old(expr)表达式用来表示一个表达式expr在相应方法执行前的取值； -
\result表达式表示方法的执行返回结果； -
\forall表达式是全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束； -
\exists表达式是存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束； -
\sum表达式表示返回给定范围内的表达式的和； -
\product表达式表示返回给定范围内的表达式的连乘结果； -
\max\min表达式分别表示返回给定范围内的表达式的最大值和最小值； -
<==><=!=>等价关系操作符：b_expr1<==>b_expr2或者b_expr1<=!=>b_expr2分别表示表达式相等或不等； -
==><==推理操作符：b_expr1 ==> b_expr2或者b_expr2 <== b_expr1。
-
- JML 中常用方法规格：
- 前置条件
requires：requires P表示要求调用者确保 P 为真； - 后置条件
ensure：ensures P表示方法实现者确保方法执 行返回结果一定满足谓词P的要求，即确保 P 为真； - 副作用范围限定：关键词
assignable表示可赋值，modifiable表示可修改； -
pure：表示方法是纯粹的访问方法，不会对对象进行任何修改；
- 前置条件
二、实现规格的设计策略
（1）第一次作业
第一次作业需要理解的JML规格不多，按照规格设计中的相应说明参照着写就行；在MyPerson中定义JML规格中说明的相应的属性，并实现相应的函数方法，其中需要仔细思考一下的是iscircle和queryblocksum两个函数，iscircle在后面的debug中改用了并查集的写法，queryblocksum也不再按照规格说明中调用iscircle来实现，而是在addrelation时就辅助实现该函数。
（2）第二次作业
第二次作业整体难度不高，只是需要阅读的JML规格更多了，充分理解JML规格说明，按照相应逻辑实现就行。第二次作业中没有复杂度特别高的需要实现的函数，我第二次作业基本上是在修复第一次作业的bug。
（3）第三次作业
第三次作业中比较难于设计的是搜索最短路径的函数，这里我是用的是dijsktra算法，也就是贪心算法，并对其进行适当地优化。与此同时，需要注意JML规格中细节的地方，比如这次的作业规格相比于上次增加了什么，规格想要说明的逻辑规则是什么等等。
三、容器选择和使用的经验
（1）ArrayList
ArrayList以数组的方式存储数据，里面的元素是有顺序，可以重复的，用户能够使用索引（元素在List中的位置，类似于数组下标）来访问List中的元素。然而，在查询时，必须遍历整个ArrayList查找相应的数据，执行效率较慢，适合顺序存储的数据。
（2）HashMap
HashMap将数据以键值对的方式存储，键的哈希码（hashCode）不可以相同，相同后面的值会将前面的值覆盖，值可以重复，里面的元素无序，用户通过键值访问元素。在查询时，根据key就能找到相应的元素，执行效率较高，适合无序存储且需要快速查找的数据。
四、历次作业和Bug分析
（1）第一次作业
架构类图：
Bug分析：最开始写第一次作业的时候，isCircle函数我是用递归的方法实现的，queryBlockSum也是按照规格说明中调用isCircle实现的，于是强测过程中出现了超时；bug修复中我改用了并查集的方法以及加连通块的方法降低时间复杂度。
（2）第二次作业
架构类图：
Bug分析：在按照规格编写代码时，我单纯地按照JML规格中的说明，会在一个函数里多次调用同一个函数而造成超时，修改函数只相应地调用一次就解决了。
（3）第三次作业
架构类图：
Bug分析：最短路径算法中出现了一些错误；在处理异常时，没有注意到JML规格中的异常顺序，弄反了两个异常的顺序造成错误；在群发红包时，没有理解JML规格中，整除之后剩余的钱全部退还本人造成错误。
五、总结
本单元作业架构很接近之后工作中可能会遇到的后端接口的逻辑实现，我认为最重要的地方在于如何理解这个接口应该实现什么功能，如何验证接口的正确性。JML规格很好的明确了接口的相应功能，我们需要做的就是正确理解这一规格并保证其正确性。在验证正确性这方面，我们可以编写功能测试接口，但需要我们把所有可能出现的情况都要考虑到，才能保证我们接口的正确性。