OO_U3 - JML

本文就是本人的博客作业。本单元除了优化方法外乏善可陈，因此我没什么额外要说的。

前言

本单元以一个简单的社交网络为背景，要求各位同学按照题目给出的JML规格，进行规格化开发。

此外，本单元中还要求各位同学对部分关键方法构建JUnit单元测试，同时也引导了同学们利用大模型辅助规格化开发。

测试过程

不同类别的测试

按照要求，我们把集中类型的测试先简要介绍一遍：

• 单元测试：从开发者角度，对最小可测试单元的测试，比如方法
• 功能测试：从用户角度，对程序的某个特定功能进行测试
• 集成测试：各个功能组合起来，整体进行测试
• 压力测试：集成测试上更进一步，以大数据量/多边界条件等，测试程序的性能和正确性
• 回归测试：在原有程序基础上进一步开发后，测试修改后程序是否保证原有功能的正确性

这集中测试，在我看来，是软件开发的不同阶段进行的：

• 单元、功能、集成测试：在开发过程中进行，旨在验证当前完成的开发工作是否正确
• 压力测试：在开发工作已有整体成果后进行，旨在验证Corner Case等严格条件下的正确性/效率
• 回归测试：在原有基础上继续开发后进行，旨在验证原有功能不受新增功能影响

数据构造策略

我选择使用数据生成器，并按照一定的指令出现权重来随机生成指令。

possible_instructions = [
"ap", "ar", "mr", "at", "dt", "att", "dft",
"qv", "qci", "qts", "qtav", "qba", "qcs", "qsp",
"coa", "doa", "ca", "da", "foa", "qbc", "qra",
"am", "arem", "afm", "aem", "sm", "sei", "dce",
"qsv", "qrm", "qp", "qm"
]

weights = [
12, 15, 8, 10, 6, 7, 6, # ap, ar, mr, at, dt, att, dft
7, 4, 3, 4, 4, 3, 4, # qv, qci, qts, qtav, qba, qcs, qsp
8, 4, 10, 5, 8, 4, 5, # coa, doa, ca, da, foa, qbc, qra
10, 8, 8, 10, 15, 8, 3, # am, arem, afm, aem, sm, sei, dce
6, 5, 5, 6 # qsv, qrm, qp, qm
]

注意到，本单元作业的输入，可能存在以下情况：

• 增删密集型（频繁ap/mr/coa等）
• 查询密集型（频繁qtvs/qcs/qsp/...）
• 上述两者兼备

我们由此可以对应调整数据生成器中，各类指令的权重，以生成多种情况下的测试数据，补足随机测试过于随机的短板。

大模型辅助

本单元中，我主要利用大模型，辅助了规格阅读、自动测试两个部分。

当前的大模型在具备了思维链等技术后，并不需要过多的提示词，多了反而会影响模型的表现。 我们要做的，就是给足大模型需要参考的信息。就本单元而言，大模型需要的信息，无非指导书，以及各个文件里存放的JML规格。

如果需要模型按某个流程执行任务，再在提示词里面描述清楚自己想要的流程，就可以了。

规格阅读

随着大模型的日趋成熟，以及JML语料每年的增长，当前的大模型已经可以做到：用户用极少的提示词，给足必要的信息，即可让大模型在JML有关问题上，输出质量较高的结果。

以下是我使用Deepseek辅助阅读JML的一次尝试；其输出结论确与规格描述的结果一致。

考虑到AI输出有时仍不可靠，在本单元中，我均采用了先本人阅读一遍规格，得出规格想要规定的结果后，再让AI阅读一遍，随后将自己的结论与AI的结论进行比较的模式，以确保我对规格的理解正确。

自动测试

在第二单元尝到了利用已有评测机框架，由AI代劳数据生成与Checker的甜头后，我在本单元继续延续了这一自动测试思路。

具体而言，我向AI提交了这些输入：

• 课程指导书（通过网页审查元素，可以得知其存在一个content.json中）
• 存有规格内容的各个.java文件，合并为一个文本文档，规避AI工具的文件上传次数限制
• 示例datagen.py与checker.py，旨在让AI在已有评测机接口下，编写数据生成与正确检查器
• 一定的提示词

本单元中，我的提示词如下：

请参考main.txt中，各类的JML规格描述及Runner类的行为，以及exception.txt中各种异常的输出，参考content.json中指导书的数据范围限制，为我编写本次作业的数据生成器（datagen）与正确性检查器（checker）。上传的datagen与checker作为示例，你需要保留其中的接口。

而在第二单元，一次作业的指导书，依赖上一次作业的指导书补全不变的设计要求的情况下，我的提示词是这样的；此时，我在文件中上传了各次作业的指导书。

请帮我生成一个第七次作业的数据生成器（datagen）和正确性检查器（checker）；你应该先查看第五、第六次作业，再查看第七次作业在先前两次作业上做的修改，再开始工作；我已附上写好的datagen和checker，请仿照其格式进行编写。

在自动生成datagen/checker的过程中，我尝试了Deepseek-R1/Gemini 2.5 Pro/o3-mini等模型，均能取得一定成果。生成的datagen一般不存在问题，但生成的Checker虽整体框架无误，但在边界条件的检查上往往会存在疏漏。

针对这个问题，我选择“边测试，边修改”：在出现Checker报错时，先检查我自己的程序是否有问题，在确认自己的程序无误后再检查checker的问题。如果修改起来很方便，自己改了即可，不方便则直接指出问题，让AI工具进行修改。这一模式我已在多次作业中确认可行，且获得了可观的成果，可以在后续的第四单元继续使用。

生成的datagen出问题的情况也存在，主要表现在部分指令不在生成范围内。这个问题，一般给AI指出问题，并让其修正即可。（假设之前你已经给足了参考信息）

架构设计

实不相瞒，这单元的架构已经给定了设计，可发挥的空间并不大，也没有什么重复介绍的必要。这一部分介绍的，主要是优化方法。

并查集

这主要是为isCircle()方法服务。我们需要快速判断关系图内，两个人是否连通。诚然，使用BFS更通用，但是利用并查集，查找的最好情况，复杂度可以达到O(1)。

具体而言，就是对于关系图内各节点（人）进行聚类：

• 每个聚类，选取一个节点作为代表
• 每个节点记录自己所在聚类的代表
• 通过比较每个节点的代表是否相等，得出二者是否在一个聚类内
• 一个聚类中，可以保证各节点关系连通

注意到，并查集的维护是个严重的问题。我选择在Network内维护一份完整的关系图，同时引入脏位机制；在发生关系删除时，脏位置高；在查询时，若脏位有效，则按照关系图重建并查集。

并查集内部引入路径合并，以及按节点数的启发式合并，避免退化成链表带来的性能下降。

脏位

众所周知，当我们修改了一个状态后，只要我们不查询它，我们是不知道它改变了的！

因此，我们引入脏位：

• 对于某个不好维护的状态
• 状态受到影响，要发生改变，且有其他信息知道如何改变时，不改变状态，而是把脏位置1
• 在查询状态时，若脏位有效，则按照其他信息重建状态，否则直接返回状态

利用这一思路的方法：

• queryCoupleSum() ，在关系权重发生变化时，难以一下就得知配对数变化
• getBestContributor()，文章删除导致贡献变化，不遍历很难得知最佳贡献着
• queryBestAcquaintance()，在关系权重发生变化时，不遍历当前熟人，很难得知最佳熟人

动态维护

在我们向一个集合加入一个元素时，我们便可动态维护一个集合整体的属性，从而避免查询该属性时遍历整个集合，导致效率下降的问题。

以queryTagValueSum()为例，每发生一次关系的加入/更改/删除，Tag内的valueSum属性就对应进行加减。

queryTagVar()思路与之类似，不再赘述。

链表的维护

主要是为了处理queryReceivedArticle()。

在文章发生删除时，我们需要对Person接到的该文章进行删除。链表的删除一直是个问题，一般采取遍历链表，找到目标再删除的方法；很显然，在链表大小较大时，如此删除的开销实在太大。

而且，包装好的LinkedList中的方法，无法做到高效移除链表中所有符合某一规则的元素。在这个情况下，我们希望一下移除链表中，所有文章ID为指定值的节点。

注意到，对于双向链表，如果已知要移除的节点，那么，只需修改其前后节点的连接即可，时间复杂度可以做到O(1)，十分诱人；由此，我萌生了一个想法：在原有双向链表的基础上，再使用哈希表+链表，记录一个文章ID值对应的所有节点。时间复杂度是O(n)，不过n取决于已有的同文章ID节点数，相较遍历整个链表，效率也已经足够了。

随后，我自行实现了一个IndexedLinkedList类，实现了上述思路。较我原有的实现方法，这么做的时间、空间复杂度均有所下降。原有思路见下文“性能优化”。

这么做的性能瓶颈，在于额外HashMap的维护。

杂项 - 增量化开发

众所周知，解引用、条件分支等等都是有时间开销的；为了尽可能减少这一开销，我们引入“增量式编程”。

举一个例子：

// 两次解引用开销
int var1 = persons.get(id).getVar1();
int var2 = persons.get(id).getVar2();

// 一次解引用
Person p = persons.get(id);
int var1 = p.getVar1();
int var2 = p.getVar2();

这能够带来一定程度的效率提升。

性能相关

上面提到，我在选择带索引双向链表前，使用了另外一个方法，这里简要做一个介绍。

既然链表删除要遍历，那我可不可以不删呢？ 答案是可以的。

注意到，articles容器只可能有两种操作：

• 在头部插入新节点
• 删除容器中所有ID为特定值的节点

且：

• 在ID为特定值的所有节点删除后，后续仍有可能加入ID位为该值的节点
• 删除和加入不可能同时发生
• 删除的区间，和删除后新加入的区间不相交

因此，我们可以：

• 链表只增不删
• 用一个HashMap<Int, Int>，记录当前链表中，一个ID有效节点的个数
• 每加入一个节点，对应ID有效次数加1，没有键值就设为1
• 全部删除时，直接撤销键值对应

并在query/getReceivedArticle处动手脚：

• 从头遍历，对于某个ID的节点，以HashMap对应键值，作为遍历中，读取该ID节点的次数
• 若次数<=有效节点数，则认为该节点有效，将其加入返回的容器中
• 若次数大于有效节点数，则认为该节点是被删除操作删除的操作，忽略之，从下一个节点继续遍历

这样就可以规避删除的遍历问题。

但是，这么做有两个严重的问题：

• 内存溢出：这一机制对链表只加不减，得亏强测强度仍然不算大，不然这样是有可能MLE的
• 极端情况：考虑两个节点之间，间隔了数量极大个无效节点；这样的话，我们遍历的效率会急剧降低，且这一代价每次查询都存在，我们无法保证这种情况不发生

因此，我换到了上面使用带索引双向链表的方法。换了之后，对于Hw10的强测测试点，不仅有时间效率的提升，也解决了上面两个严重的问题。

对规格的理解

在谈这些问题之前，我们需要明确，规格描述的是什么？ 事实上，规格描述的是方法执行后的结果，而非方法执行的过程。

• 规格中出现的“过程”，可以认为是测试流程，也可以认为是用来描述结果的过程。
• 规格中出现的容器实现等等，只是为了举例描述一个结果，可以认为其实现是一个抽象概念

因此，我们能发现一个显而易见的结论：规格不规定达到结果的过程，规格与实现分离因此合理，我们自然也可以在实现过程这一部分自由发挥，只要保证结果符合规格即可。

JUnit有关

我认为测试可以分为两部分，一是不同测试上下文，二是方法自身的正确性检验。

我们先谈方法正确性检验的部分吧。

上面提到，规格中出现的”过程“，可以认为就是测试流程。因此，按照规格中描述的过程来编写测试，即可保证测试通过与符合规格等价，这是最简单的办法。

当然，我们也可以根据规格描述的结果，以另一个测试流程来检验；不过，既然规格已经告诉你测试流程了，除非这一新的测试流程，在保证检测正确性的前提下，效率更快， 我们没有不按照规格给的测试流程编写测试的理由。

综上，照抄规格，就是实现方法正确性检验的最简便方法。在这个选择下，“Junit测试检验代码实现与规格的一致性的效果”这个问题更不成立，因为我们的method测试流程，本来就是跟规格描述完全一致的。

方法正确性检验后，就是构建不同的测试上下文了，换言之，构造测试数据。事实上，我在本单元作业对JUnit的测试中出现的问题，都是因为构建的测试数据不够强大，未能考虑到部分边界条件。

那我们怎么知道要考虑什么边界条件？这就是“利用规格信息”要做的了。我们需要从规格中得知：

• 待测试方法要求哪些属性不变，要变的属性怎么变
• 待测方法涉及的属性，会受其它什么方法的影响

明确好这两点后，我们基本就能找出所有的边界条件了。

本单元学习体会

算法的重要

如果说前两个单元是为了考察同学们对程序整体架构的设计能力，这个单元考察的就是：同学们在架构确定的前提下，进行具体实现的能力。

长期以来，我都对算法不甚重视，期望用架构或多线程等方法，代替算法解决问题。本单元打消了我这一错误的偏见，让我真正认识到了算法的重要性。

具体而言，查询关系是否连通这一问题，在并查集以外，我实在想不出效率更高的办法，这就是算法影响程序效率的一个实例。

测试的重要性

本单元开始的第一次作业，我认为严格按照规格描述的结果实现，就不会产生问题，我因此没搓评测机。然后在强测就出现了问题，最后检查发现，是自己的一处愚蠢的笔误（笑，把value赋值到id上）造成的；在有评测机的情况下，这个问题很好发现，但我没搓评测机，这个问题我就没发现。

自此以后，我每单元都搓一次评测机，避免这种事情再次发生；后面也确实没有发生过。

时刻认为自己写的程序有Bug， 这个思维模式还是很重要的。

JML为何难以推广？

形式化验证的需求的确很小，但我认为JML难以推广，是可读性出了问题。

我们简要比较一下，几种语言如何描述结果：

自然语言：操作后，id1对应成员的 | 包含id2对应的成员的 | 所有tag内，不再包含id2对应的成员

JML语言：

@ ensures  (\forall int i; 0 <= i && i < getPerson(id1).tags.length;  
@                      \old(getPerson(id1).tags[i].hasPerson(getPerson(id2)))==>!getPerson(id1).tags[i].hasPerson(getPerson(id2)));

（伪）数学语言：
$$\forall t \in Persons[id1].Tags[], prev(t.hasPerson(id2))\rightarrow !t.hasPerson(id2)$$

不可否认，自然语言在表达上最直观凝练，但是它无法避免产生歧义的问题；在形式化验证/规格化开发等严谨的前提下，自然语言一般不被使用，或仅作为辅助说明出现。

这就是我们为何要引入规格语言。

但是，不难注意到，与我们上面的（伪）数学语言相比，描述相同的结果，JML语言花费了显然更多的篇幅；这是为什么？

一言以蔽之，JML的抽象程度还不够，没有脱离具体实现。 事实上，JML在尝试用一种基础的，具体的实现（比如容器认为是数组），或一种基础的，具体的过程（比如容器的查找过程），来尝试描述自己想要的结果。

在本人对形式化验证的简单了解后，我了解到了TLA+这门形式化验证语言。其完全基于数理逻辑，而非软件开发思想，从而做到了高度抽象、脱离具体实现。最后的描述效果，与我们上面随手写的（伪）数学语言基本一致，严谨而简明。

当一个工具带来的收益，远远小于其带来的负面影响时，是否采用它就很值得商榷了。JML确实做到了严谨描述结果，但其带来的可读性问题十分严重。与之比较，作为当前主流的形式化验证语言，TLA+采用了数理逻辑语言进行结果的描述；虽然有初始的学习成本，但其保证了描述的可读性。相信这就是JML难以推广的原因吧，这也让我认识到了选好工具的必要性。

在研究这个问题的时候，我也再次感受到了 “抽象” 这一哲学，在计算机科学中的重要作用。抽象不仅有利于找出通用的解决方法，更有利于准确地描述问题。