BUAA面向对象迭代开发总结-JML规格化方法

BUAA第三次迭代作业总结

架构设计

类图

本次作业主要任务是维护一个社交网络，由于三次迭代之间为增量设计，故此处仅展示第三次作业的UML类图。 uml_lab3

第一次作业实现Network，Person，Tag，三个类，第二次作业实现OfficialAccount类，第三次作业实现Message类。

图模型

在社交网络的维护过程中，实际上是在对一个以Person为节点，边为社交关系的无向图进行维护，Person加入Network即为向次无向图中加入孤立点，为两个Person增加社交关系即为向此无向图加边，其余属性（如Message等信息）均可以视为在图中节点的附加属性进行维护。

大模型辅助规格化设计

本次迭代作业中，使用大模型的体验主要有以下几点：

  • 目前大模型适用于根据实际要求生成JML规格。
  • 对于一部分不需要使用其他数据的方法，可使用大模型根据该方法的JML规格直接实现代码。
  • 大多数方法可能与其他方法直接相关，直接使用大模型较难实现具体代码，需要不断地向大模型输入其他类或其他方法的接口和返回值才能实现具体代码。

性能

根据社交网络维护这一目的，本次迭代作业涉及大量图的算法问题，需要大量进行图的遍历，下面是一些我个人在迭代过程中遇到的性能问题。

性能问题与修复

三元环查找

我起初直接使用了无向图转有向图，再进行遍历的方法。对于一条边的两个节点，将该边转换成由度少的节点指向度多的节点的有向边，若度相同则将id小的节点指向id大的节点。这种方法的时间复杂度为\(O(m\sqrt{m})\)，m为图的边数。

这种方法对于稀疏图有较好的性能，但是一旦边数很多，时间复杂度依旧很高，因此我后来采用了动态维护的方法进行管理。

在每个Network中维护当前三元环的数量，每次增加或删除边时动态维护这个数量，使查询三元环这个操作的时间复杂度降为\(O(1)\)。这种方法会增加增加删除边的开销，但增加和删除边的时间复杂度不会超过\(O(n)\)，综合来看优于前一种方法。

对每个人收到的文章进行增加和删除

由于在查询每个人收到的文章时需要同时查询最新收到的5篇文章，因此我起初直接使用ArrayList管理收到的文章，直接在其尾部进行插入操作，查询时从尾部反序查找5篇文章，但是由于ArrayList的删除元素过程为\(O(n)\)的，大量地删除文章可能导致TLE，因此采用另一种方法。

采用双向链表维护收到的文章，以文章id为键，链表节点为值，用HashMap进行文章到节点的索引，增加文章时直接从头部进行插入，查询时从头部查询5篇文章，删除时根据id直接查找到对应的节点，再进行链表节点的删除，从而保证插入，查询，删除的时间复杂度均为\(O(1)\)，优化了删除时的性能问题。

对于组群中每个人之间的关系值之和的查询

直接在一个组群中按边遍历各个关系值并求和时间复杂度为\(O(m)\)，如果该图近似为一个完全图，这个遍历操作可能导致TLE，因此还是采用动态维护的方法，维护每个组群中的关系值之和。

在Person类中维护其所加入的组群，每当增加，删除，修改两个人之间的关系值时，修改该人所在组群中的关系值和，从而实现动态维护。

规格与实现

规格与实现大致概念如下：

  • 规格：JML规格主要描述一个方法执行前的条件和执行后的结果，并不关心具体实现过程。
  • 实现：实现满足JML规格要求的代码。

因此，实现代码时不能死板地按照规格进行，在满足规格要求的基础上可以进行各种优化。

测试

首先回顾测试的不同种类

  1. 单元测试：对代码最小单元（如：函数、方法、类等）进行测试。
  2. 功能测试：验证代码功能是否满足要求，不关心内部实现。
  3. 集成测试：验证各个模块之间的协作。
  4. 压力测试：探测系统的极限承载力。
  5. 回归测试：保障既有功能不被破坏。

数据构造

本次作业中，为了充分测试待测代码的正确性，主要的数据构造思路有以下两种。

随机生成测试数据

以查询三元环个数为例，先向图中加入一定数量的点，然后根据一定概率为每个点之间加边，这种方法能够测试一些普通情况下的代码正确性，因此我们还需要其他数据以进一步测试。

生成极端数据

仍然以查询三元环个数为例，主要考虑如下极端情况。

  • 根据图论知识易得，简单无向图三元环数量最多时，该图为完全无向图，构造方法为先向图中加入一定数量的点，两层遍历所有点使每个点两两之间存在边。
  • 不正确的代码可能在图中存在空指针问题，可以构造一个空图以测试这种情况，只需要向图中加入点，但是不加任何边即可。

Junit测试

数据构造

本次作业中，以查询三元环个数为例，采用10组随机数据，1组完全图数据，1组空图数据进行简单的单元测试。

正确性验证

根据JML规格，严格按照JML规格编写测试代码，保证测试代码准确无误，使用assertTrue，assertEquals等方法进行正确性判断。

副作用检查

对于一些查询方法，我们不希望在该方法的执行过程中修改被维护的一些关键数据，因此需要进行副作用检查。

在数据生成阶段，构造两份一模一样的数据（避免浅拷贝问题），一份用作被测代码执行前的快照，一份用于代码的测试，比较两份数据在代码执行后的各个关键数据是否有差别即可检测被测代码的副作用。

学习体会

JML规格为代码提供了严格的规范，如果需要解决一个较复杂的问题，可以先根据基本要求，设计接口，然后为每个接口编写规格，按照规格的要求实现该接口，测试时只需要测试待测代码是否满足规格的各项要求即可。规格化的设计让我体会到了一种工程思维——以“数学证明”的严谨性看待代码，这种思维可以大大提高代码质量。