OO Unit3 博客作业

一、对 JML 和规格驱动开发的理解

规格驱动开发，应该是：先读规格，再设计状态，最后写实现。

1. JML 能减少自然语言需求的歧义

  • requires 说明方法在什么条件下正常执行
  • ensures 说明执行结束后必须满足什么状态
  • assignable 说明方法允许修改哪些对象
  • signals 说明异常情况应该如何处理。

    这样一来，实现者要保证异常正确、状态变化正确、副作用范围正确，要求更加明确清晰，大大减少由于自然语言语义不清晰不明确导致扯皮的情况。

2. JML影响数据结构设计

  • 比如 queryMutualFollowingSum 的规格可以用双重遍历描述互关用户对，但如果实现时每次查询都按这个形式暴力统计，就会在强测中超时。
  • 后来我改成在 followUser 和 unfollowUser 中增量维护互关数量，查询时直接返回结果,这个问题就解决了。

    这说明 JML 描述的是“应该满足什么”，而不是要求实现者机械照搬规格中的量词表达式。

二、JUnit 测试经验总结

我形成了比较固定的测试风格：参考 exp5 中参数化测试的形式，采用“固定边界样例 + 随机生成数据”的方式构造 JUnit。

  • 固定边界样例用来覆盖最容易出错的特殊情况
  • 随机数据则用来扩大覆盖范围，避免测试只对少数手写样例有效
  • 这样写测试结构清晰、样例数量充足，也比较容易复用到不同作业的方法上
  • 基本上可以全覆盖所有Junit特殊测试中的测试点

1. HW9 ： queryMutualFollowingSum

  • 固定样例：空网络、只有单向关注、一对互关、三人两两互关、存在无关用户等边界数据
  • 随机样例 ：随机生成一批用户和关注关系，用朴素方法在测试代码中计算期望值，再与被测方法返回值比较
  • 注意：由于是查询方法，要检查 repeated call 后状态不变，避免错误实现为了统计而修改 following 或 followers。

2. HW10 ： clean_spam_comments

  • 固定样例：空评论区、没有垃圾评论、全部命中、连续多条命中、keyword 位于开头/中间/结尾、keyword 为空串等边界情况
  • 随机样例 ：随机生成若干包含或不包含 keyword 的评论，自动计算应删除数量和最大出现次数。
  • 注意：检查返回的删除数量，剩余 commentIds 和 commentContents 是否仍然一一对应，其他视频是否没有被误改，目标视频的播放量、点赞数、转发数、投币数等非评论属性是否保持不变。这种状态快照检查能覆盖 assignable 层面的要求。

3. HW11 : recommend_Nth_up

  • 固定样例：覆盖 rank 非法、用户不存在、候选 up 主不足、得分相同但 tie-break 不同、rank 刚好等于候选数量等情况
  • 随机样例 ：构造更多用户、视频、观看和互动关系，利用测试代码中的参考计算逻辑得到期望推荐结果
  • 注意：推荐方法本质上是查询，也需要在调用前后保存用户状态，检查它没有修改用户、视频或关注关系

三、三次作业的迭代过程分析

1. 迭代内容

Unit3 的三次作业是在同一个视频社区系统上不断扩展。

第一次作业：搭建基础社交网络

  • 系统核心是 User、Video、Network 三个类，需要支持用户添加、视频上传、关注/取关、观看视频、查询未观看视频、查询粉丝年龄比例、查询互相关注数和最短路径。
  • 这个阶段主要解决的是“规格到代码状态”的映射问题：Network 维护全局 users 和 videos，User 维护 following、followers、receivedVideos，Video 维护 id 和 uploaderId。
  • 此时系统状态还比较简单，但已经能看出一些设计选择会影响后续，比如用户和视频最好用 id 建立映射，而不是每次都遍历查找。

第二次作业：加入硬币经济体系和视频互动

  • 新增内容包括：充值、点赞、投币、转发、评论、清理垃圾评论、购买粉丝勋章、查询最佳贡献者、查询最热视频等。
  • 这个阶段最大的变化是状态数量明显增加。User 不再只是维护关注关系，还要维护 coins、watchedVideos、likedVideos、medals、contributors、contributions 等；Video 也不再只是 id 和 uploaderId，而是新增 type、playCount、likes、forwardCount、coins、commentIds、commentContents 等。
  • 很多操作都变成了事务性操作：例如投币不仅要扣用户硬币，还要增加视频投币数，并维护 up 主贡献者信息；清理评论不仅要删除内容，还要保持 commentId 和 commentContent 的对应关系。

第三次作业：加入推荐系统

  • 新增内容包括：推荐视频、推荐第 N 名 up 主、查询最有影响力 up 主、查询用户画像、查询全局最佳贡献者等。
  • 这个阶段的重点从“维护状态”转向“根据状态进行统计、排序和推荐”。用户新增了 typeCounts 和发布视频集合，很多旧方法也随之产生新意义。例如 watchVideo 不再只是从未观看列表中移除视频，还会影响播放数、观看历史和用户分区兴趣；uploadVideo 也不只是创建视频对象，还要维护上传者发布视频集合，并影响后续推荐和影响力统计。

2. 发现已有方法/容器在迭代中的变化

对比接口和指导书

  • 每次作业下发后，我会先看 UserInterface、VideoInterface、NetworkInterface 中新增了哪些 model 字段、哪些方法签名变了、哪些旧方法的 JML 改了。
  • 例如 HW10 中 uploadVideo 新增了 type 参数，Video 构造方法也随之变化；HW11 中推荐相关方法加入后，User 的 typeCounts 就意味着 watchVideo 必须维护用户观看分区统计。
  • 如果只机械地补新增方法，很容易漏掉旧方法需要维护新状态。

    从新增容器反推旧方法

  • 比如新增 likedVideos 后，likeVideo 既要修改视频点赞数，也要修改用户点赞记录；新增 contributors 和 contributions 后，coinVideo 就必须同步更新 up 主的贡献者信息；新增 commentIds 和 commentContents 后，clean_spam_comments 就必须保证两个容器同步删除。
  • 每新增一个字段，都要想一遍：哪些旧方法会读它？哪些旧方法会改它？哪些查询依赖它？

维护“方法—状态影响表”

  • 把users、videos、following、followers、receivedVideos、watchedVideos、likedVideos、coins、comments、typeCounts、contributions 等状态列出来，再逐个方法标记它会读取或修改哪些状态。
  • 这样做的好处是能防止“局部补丁式开发”。例如 watchVideo 在不同作业阶段承担的状态维护越来越多，如果没有这种表，很容易只保留第一次作业中的删除 receivedVideos，而忘记后续的播放量、观看历史和兴趣统计。

3. 发现性能瓶颈问题

性能瓶颈的发现则主要来自强测反馈和复杂度分析。
Unit3 让我认识到，JML 只规定结果正确，不保证实现复杂度合理。一个方法即使完全符合规格，也可能因为实现过于朴素而超时。(hw9没进互测的血泪教训)

因为只有hw9没做相关优化，所以重点说一下hw9

queryMutualFollowingSum

  • 一开始这个方法很自然地按照规格含义写成双重循环，遍历所有用户对，判断是否互相关注。这个实现逻辑正确，但强测中会被大量重复查询卡住。
  • 对于一个强测数据点，总指令数接近 9500，其中 query_mutual_following_sum 接近一千次，用户数又在两千左右。如果每次查询都做 O(n²) 判断，总判断量会达到几十亿级别，必然 CPU 超时。
  • 解决(增量维护):在 followUser 成功建立一条边之前，如果反向边已经存在，就让互关数量加一；在 unfollowUser 成功删除一条边之前，如果删除前双方互关，就让互关数量减一。这样查询时直接返回维护好的变量，复杂度从 O(n²) 降为 O(1)。

uploadVideo

  • receivedVideos 的核心操作是头插和取前五个，更适合用 LinkedList 或其他支持高效头插的数据结构，而不是普通 ArrayList。

query_up_followers_age_ratio

  • 每一次都遍历所有粉丝，在中心 up 主和频繁查询的数据下也会产生额外成本。
  • 比较自然的优化是在 User 中维护四个年龄段的粉丝计数，在 addFollower 和 removeFollower 时增量更新，查询时直接用计数计算比例。

问题的发现与解决

  • 高频指令，如果某个查询在输入中大量出现，就不能写成高复杂度。
  • 嵌套循环，尤其是双重遍历 users、videos、followers 的方法。
  • 容器操作的隐藏复杂度，例如 ArrayList 头插、线性 contains、边遍历边删除等。

性能瓶颈的发现与解决

JML 规格只说明“结果应该是什么”，并不说明“应该怎样高效实现”。
如果把规格里的 \sum、\max、\forall 直接翻译成每次查询时的全量遍历，功能上可能正确，但在数据规模变大时很容易出现性能问题。
因此，应该时刻警醒性能分析相关的问题。

  • 识别高频查询：对于只查询状态的方法，如果每次都要遍历所有用户、所有视频或所有关注边，就要提前警惕。例如 queryMutualFollowingSum 不适合每次都双重遍历用户对，而应该在 followUser 和 unfollowUser 中维护互关数量，查询时直接返回结果。

  • 前移统计计算：很多统计量只会被少数修改操作影响。例如粉丝年龄比例只会在关注和取关时变化，视频热度只会在观看、点赞、投币、转发时变化，用户兴趣只会在观看视频后变化。因此，与其在查询时重新统计，不如在状态变化发生时同步更新相关计数或缓存。

  • 匹配数据结构：容器不能统一用 ArrayList 解决，而要根据主要操作选择。对于需要通过 id 高频查询的 users 和 videos，应使用 HashMap；对于 following、followers、watchedVideos、likedVideos、medals 这类需要频繁判断是否存在的集合，应优先使用 HashSet；对于 receivedVideos 这种需要保持顺序、频繁头插、只查询前几个元素的容器，则要避免 ArrayList.add(0, x) 的整体搬移，可以考虑 LinkedList 或类似结构。

  • 维护有序索引：对于最值和排名类查询，例如查询某分区最热视频、查询最有影响力 UP 主，如果每次都遍历全体对象，就会产生重复计算。更合适的做法是用 TreeSet 等有序容器维护排序结果，在对象状态变化时先删除旧对象、更新字段、再插回容器，查询时直接取最优元素。

  • 缓存图上结果：对于 queryLongestDecSeq 这类图上的全局查询，结果只会在用户或关注边变化后改变，因此可以使用 dirty 标记：在addUser、followUser、unfollowUser 后标记缓存失效，在下一次查询时重新计算；如果图结构没有变化，连续查询就直接返回缓存结果。

四、程序 Bug 及原因分析

在完成作业和公测中我遇到的 bug，大多是来自对规格理解不完整、状态维护不统一等等。

  • 规格理解类 bug：有时会先按自然语言和业务直觉理解方法，再回头看 JML。
  • 状态同步类 bug：系统状态分散在 User、Video、Network 多个对象中，如果没有明确列出一个方法会影响哪些字段，就很容易漏改。
  • 方法复杂度/性能类 bug：强测的bug主要还是体现在性能上，这一块我们在上一部分已经提到并分析了，在此不过多赘述。

五、大模型在 Unit3 中的使用经验

在 Unit3 中，我使用了大模型辅助完成规格化设计相关工作。大模型最有价值的地方是帮助我完成从规格到实现的中间过程：理解 JML、拆解任务、讨论数据结构、补充测试场景，以及定位一些编译和实现问题。

1. LLM优势：降低理解成本

  • Unit3 的需求分散在指导书、接口 JML 和官方异常说明中，而且很多 JML 表达式包含 \forall、\exists、\sum、\old 等形式化语义。
  • 直接阅读时容易漏掉边界条件或副作用要求。
  • 大模型可以把这些规格翻译成更接近实现视角的任务清单，例如这个方法的正常行为是什么、异常分支有哪些、会修改哪些状态、哪些状态不能改变。这样我在写代码之前，可以先形成比较清晰的实现框架。
  • 检查“旧方法是否需要修改”。比如 HW10、HW11 都是在前一次作业基础上扩展属性和业务逻辑，如果只看新增方法，很容易忘记旧方法也要维护新状态。大模型可以根据新增字段提醒我有没有什么漏改。

2. LLM问题：效率

大模型根据 JML 编程时确实容易忽视效率问题。

  1. 复杂度分析：它往往会把规格中的量词和求和直接翻译成循环。因此，复杂度分析不能完全交给大模型，仍然需要自己通过指令引导大模型发现相关问题，并一步步优化给出解决方案。

  2. 架构和容器问题：JML 描述的是抽象状态，不规定一定使用什么容器。大模型有时会倾向于统一使用 ArrayList，因为它直观、容易模拟规格中的数组或集合。但实际实现时，不同状态适合不同容器，这时候也是需要我们通过指令引导大模型针对问题给出更好的容器选择建议。

3. LLM单元测试

  • 在单元测试方面，大模型比较适合用来生成具体的测试代码，而不是给出合适有效的测试思路。
  • 我在写 JUnit 时，会让大模型参考上机实验中的参数化测试风格，帮我整理“固定边界样例 + 随机生成数据”的结构。

六、JML“击鼓传花”游戏的感悟

这个游戏的过程是把一个自然语言需求先翻译成 JML，再由后面的同学根据 JML 反向翻译成自然语言，经过多轮传递后比较最终结果和原始需求是否一致。
JML“击鼓传花”游戏让我对规格传递中的信息损失有了比较直观的感受，它看起来很像多人协作开发中的需求传递过程。

1. 游戏感受

简单需求的复现率比较高，但复杂需求很难在短时间内完整表达清楚。 如果需求只是“返回数组最大值”或“判断某个元素是否存在”，大家通常比较容易写出等价的 JML，也比较容易从 JML 还原出原意。但一旦需求包含多个连续步骤、多个边界条件或隐含的业务语义，传递就很容易出问题。

我们组有一个很有意思的例子：

  • 有同学写的自然语言需求是完成一个方法，要求把数组中的 int 整数“先去重，再去掉合数，最后升序排序”。
  • 这个需求本身包含三个连续操作，而且每一步都有细节：去重要保留什么集合，合数如何定义，排序是对剩余元素排序还是对原数组原地修改，返回结果长度如何确定等。
  • 因为时间比较短，第一步把 NL 翻译成 JML 就很不顺利。第二步轮到我根据上一位同学写的 JML 反向翻译时，我甚至完全没看出来它原本想表达什么。
  • 这说明复杂需求如果没有拆开写清楚，后面的人很难仅凭一段形式化规格恢复出完整语义。

在 NL 和 JML 反复转换的过程中，自然语言会逐渐变成 JML 的文字翻译，而不是人类真正理解的需求描述。 一开始的 NL 通常会带有业务场景和操作意图，但经过几轮之后，后面的 NL 往往变成“对于任意 i，存在某个 j，使得……”这样的逻辑句子。它看起来更接近 JML，也更形式化，但反而离最初的人类需求更远。这样的 NL 对写规格有帮助，却不一定对理解业务有帮助。

有些自然语言需求其实只有作者自己能看懂。 在游戏中，有的同学写的 NL 如果不额外解释，别人很难判断其中的关键词具体是什么意思。多人开发中也很容易出现类似问题：需求提出者以为自己写清楚了，但实现者看到的是另一个含义。

2. 发现bug

很容易发现大家的bug都是有共性的：

  • 遗漏边界条件：比如没有说明空数组、重复元素、特殊数值如何处理。
  • 把操作过程和最终结果混在一起：没有明确方法到底是修改原数组还是返回新数组。
  • JML 写得形式上很复杂：没有准确表达原始需求，导致后面的人无法还原语义。

3. 降低信息差的措施

  • 需求必须同时保留“业务描述”和“形式化约束”：自然语言负责说明这个方法想解决什么问题，JML 或类似规格负责说明输入、输出、边界和副作用。两者不能互相替代。
  • 组内要统一术语表：每个词都应该有明确含义。不能让每个人按自己的理解解释。
  • 写完规格后要进行反向复述：一个人写完 JML 后，另一个人不看原始需求，只根据 JML 复述方法行为，再由原作者确认是否一致，提前发现需求传递中的偏差。
  • 关键边界要用测试样例固定下来：对于容易产生歧义的地方，只靠文字说明仍然可能不够。可以通过单元测试明确规定特殊输入下的输出，这样实现者和测试者对需求的理解会更一致。