1 JML语言总结

1.1 注释结构

JML注释一般被放置在被注释成分的近邻上部，结构主要有以下三种：

1 //@ annotation
2 
3 /*@ annotation @*/
4 
5 /*@ annotation
6   @ annotation
7   @ annotation
8   @*/

1.2 JML表达式

1.2.1 原子表达式

\result表达式：表示一个非void类型方法执行的返回值

\old(...)表达式：在括号内的表达式应取方法执行前的旧值

\not_assigned(x, y, z, ...)表达式：括号内的表达式在方法执行过程中未被赋值

\nonnullelements(container)表达式：container对象中存储的对象不会有null

\type(type)表达式：type类型的类型

\typeof(expr)表达式：expr表达式的精确类型

1.2.2 量化表达式

(\forall ...; ...; ...)表达式：全称量词表达式

(\exists ...; ...; ...)表达式：存在量词表达式

(\sum ...; ...; ...)表达式：求和表达式

(\product ...; ...; ...)表达式：连乘表达式

(\max ...; ...; ...)表达式：最大值表达式

(\min ...; ...; ...)表达式：最小值表达式

(\num_of ...; ...; ...)表达式：满足条件的元素总数

1.2.3 操作符

E1 <: E2表达式：类型E1是类型E2的子类

expr1 <==> expr2表达式：左右布尔表达式值等价

expr1 ==> expr2表达式：左布尔表达式推出右布尔表达式

\nothing：表示一个空集

\everything：表示当前作用域下能够访问的所有变量

1.3 方法规格

方法规格由前置条件(pre-condition)、后置条件(post-condition)和副作用(side-effects)构成

前置条件：requires expr

后置条件：ensures expr

副作用：assignbale a, b, ...

纯粹访问性方法：pure

signals (Exception e) expr语句：当expr被满足时，抛出异常

1.4 类型规格

不变式限制(invariant)：数据成员需始终满足的条件

状态变化约束(constraint)：前序可见状态与当前可见状态之间满足的条件

2 架构设计

上图为homework11程序的UML图，其中显示了主要的依赖关系，针对Person, Group, Network这3个给定接口，分别用MyPerson, MyGroup, MyNetwork来实现，在MyNetwork中涉及到的一些图的复杂算法，则另外设计了Dijkstra, Circle, HalfMatrix来实现和优化。现在看来，这个架构并不好，MyNetwork过于冗长，其中一些关于图的算法是直接在其中实现的，而另一些确是单独设计类来实现的，这造成了架构的混乱，耦合性高。考虑到本单元是一个人际关系网络的管理系统，其数学抽象是图，所以应当专门设计一个图的类来管理整个人际关系网络，并且提供各种图的算法的实现，这样一来将图的管理和算法实现与人际关系管理系统相分离，使得架构更加清晰明了。

3 JMLunitNG

JMLunitNG能够自动生成测试样例进行测试，在经过实验后发现JMLunitNG生成的是一些边界数据，比如0、MAX_VALUE、MIN_VALUE、null等，这些数据在代码实现完成、开始测试的初期可能有一定的作用，但并不能更具实际约束进行测试，例如像本次作业中age被约束在0~2000之间，value被约束在0~1000之间等等，针对这些具体化的约束，还应当使用Junit手动编写具有特征的测试样例来进行代码测试，如下一部分所展示的。

4 Bug与修复

这次人际关系网络管理系统程序的bug主要出现在关于图的算法的具体实现与优化的过程中。homework9程序中，采用深度优先搜索的方式来实现qci请求，在初次实现后，经手动测试发现程序会发生死循环。在homework11程序中，qmp请求、qsl请求、qbs请求的实现都与图算法有关，实现起来较为复杂，也容易出现bug，采用Junit工具进行单元测试，针对homework11中容易出错的新增请求进行测试，在单元测试过程中发现了不少的bug，收获显著。如图所示：

本单元的另一大重点在于程序的性能，homework10和homework11都在时间复杂度上栽了跟头。在homework10中，qrs请求和qvs请求的实现最初采用的是普通的遍历方式，导致测试时cpu超时，之后改成了再每一次发生ap请求和ar请求时，动态修改qrs请求和qvs请求的请求值。在homework11中，qsl请求的实现过于复杂，在图的规模增加到10^2以上的数量级时难以在有效时间内计算出结果，后来改用删点法来实现。qci请求和qbs请求的实现也过于复杂，后来意识到，qci请求的实现其实可以完全依赖于qbs请求的实现，而qbs请求本质是计算图的连通分量，连通分量可以在每一次发生ap请求和ar请求时进行动态更新，这大大提升了程序性能。qmp请求的本质是计算最短路径，运用堆优化的Dijkstra算法可以有效地提升程序性能。

5 规格的理解与感悟

 规格为一个类的属性和方法进行了形式化的规范，规格为程序的不同层次、不同类之间提供了一种形式化统一化的接口，使得在不同层次进行开发的程序员不需要关心他所依赖的其它层面的具体实现，只需要严格按照实现写好的规格进行调用，就能保证不同层次在衔接过程中不会出错，当然这依赖于每个程序员都需要严格按照规格去开发。JML的编写并不比代码本身的编写轻松，JML的编写应当非常注重逻辑性，考虑是否覆盖了整个域，同时也需要考虑JML的可读性，我发现，逻辑完备的JML可能甚至比代码实现本身还长，也许规格语言本身还有一定地改进和优化的空间。虽然说JML其实是比较头大的，但是规格的思想本身是很有价值的，即便是在一个人编写整个程序的过程中，也往往会遇到由不同的类组成不同层次，最不容易发生混乱的方式是划清不同层次之间的界限，定义好它们之间的交互关系，然后逐个实现，这其实就是规格的思想，在实现一个层次时不需要考虑另一个层次的细节。

原文地址：https://www.cnblogs.com/buaa18373088/p/12940131.html