题目回顾

本单元中指导书内容较少，题目要求主要依靠JML提供，大致要求为维护一个视频网站，实现User、Network、Video三个类及点赞投币等常见行为。具体要求JML见官方包，我已上传至我的GitHub主页

  • Week1：实现基础用户管理、关注关系、视频上传与观看、互粉查询、最短路径查询等功能。
  • Week2：新增点赞/投币/转发/评论系统、硬币与勋章机制、垃圾评论清理、各类热度查询（最受欢迎视频、最长递减关注链等）。
  • Week3：引入用户画像与兴趣计算、视频推荐与UP主推荐算法、影响力排名、全局最佳贡献者等高级查询功能。

JML与规格驱动开发

什么是规格驱动开发

本单元最大的特点是规格驱动开发。与第一、二单元先读指导书理解题意不同，本单元的核心需求几乎完全通过JML（Java Modeling Language）规格描述。JML使用requires、ensures、assignable、pure、signals等关键字精确刻画了方法的：

  • 前置条件（requires）：调用者必须满足的条件，如用户必须存在、ID不能重复、年龄范围合法等。
  • 后置条件（ensures）：方法执行后必须达成的状态，如互粉计数正确更新、视频成功加入集合、关注关系双向建立等。
  • 副作用范围（assignable）：明确方法可以修改哪些字段。这对于写测试和验证程序行为至关重要，也是判断一个方法是否是pure的依据。
  • 异常规格（signals）：定义何时抛出何种异常，是方法入口处参数检查顺序的重要依据。

从JML到代码的实践策略

在具体实现中：

  1. 先读异常规格：JML中signals子句定义了何时抛出何种异常，这决定了方法入口处需要哪些参数检查。顺序通常与JML中signals的书写顺序相关。
  2. 再读正常行为后置条件：理解操作完成后各字段应处于什么状态。例如uploadVideo不仅要在全局加入视频，还要让UP主的每个粉丝通过receiveVideo收到该视频。
  3. 注意纯方法约束：如queryMutualFollowingSum等查询方法被标记为pure，实现中不能修改任何状态。测试中对此有严格校验（调用前后对象状态必须完全一致）。
  4. 维护与JML一致的数据结构：由于JML中会遍历users数组或检查followings关系，代码中使用HashMap以ID为键存储用户和视频，既满足效率需求，也便于在JML层面理解集合关系。

JML的灵活性：只规定"做什么"，不规定"怎么做"

总结地说，JML只负责提供方法的 “起点” 与 “终点”，其中具体的实现路径与算法仍旧由我们自行发挥。实际上，强测与互测中也确实会多次测试实现的性能，因此其实规格驱动开发需经历 阅读JML了解方法作用 → 自行使用合适算法提高性能 → 再次阅读JML检查副作用 的过程，有利于既严谨又高效地完成项目。

例如，queryMutualFollowingSum的JML规格是双重循环遍历所有用户对的数学定义，但如果每次查询都如此实现，时间复杂度是O(n²)，在大量查询下必然超时。于是可以在followUser和unfollowUser时动态维护mutualFollowingSum，将查询降至O(1)。JML并不禁止这种优化，只要最终表现（返回值、副作用约束）符合规格即可。

JUnit测试

本单元引入了JUnit单元测试要求，重点在于验证纯方法的无副作用性和边界条件覆盖。

测试设计思路

与JML规格对齐的验证器

在QueryMutualFollowingSumTest中，我手写了一个getJmlTruth方法，完全按照JML的数学定义（双重循环遍历所有用户对，检查双向关注）计算互粉数。这使得任何维护mutualFollowingSum的优化实现都有了可对比的标准。

1
2
3
4
5
6
7
8
9
10
11
12
private int getJmlTruth(Network net) {
    UserInterface[] users = net.getUsers();
    int sum = 0;
    for (int i = 0; i < users.length; i++) {
        for (int j = i + 1; j < users.length; j++) {
            if (users[i].isFollowing(users[j]) && users[j].isFollowing(users[i])) {
                sum++;
            }
        }
    }
    return sum;
}

这种"用JML验证实现"的思路同样适用于其他查询方法。

纯方法的无副作用测试

对于queryMutualFollowingSum、queryShortestPath等pure方法，测试中会：

  • 记录调用前的网络状态（用户数量、互粉数、各用户年龄和硬币数、关注关系）
  • 多次调用查询方法
  • 断言调用后状态与调用前完全一致

这有助于发现不小心在查询方法里修改缓存或计数的问题。

双对象对照测试

compare方法和双Network设计：对net1和net2执行相同操作后，不仅比较查询结果，还深度比较每个用户的内部状态（通过strictEquals）。这种对称测试能暴露状态同步错误。

异常路径覆盖

针对JML中的各种signals子句，编写了对应的异常测试：

  • InvalidAgeException（负数年龄、超110岁）
  • SelfSubscriptionException（自己关注自己）
  • DuplicateSubscriptionException（重复关注）
  • FollowLinkNotFoundException（取关未关注的人）
  • VideoUnwatchedException（未看视频就点赞/投币）
  • InsufficientCoinsException（硬币不足）
  • UncessException（两点不可达）

复杂功能的白盒测试

CleanSpamCommentsTest中测试垃圾评论清理的多个维度：

  • 删除包含关键词的评论数量是否正确
  • 最大出现次数统计是否准确（包括重叠情况如"aaaaa"中"aa"出现4次）
  • 清理后剩余评论的ID和内容顺序
  • 不同视频之间的评论隔离性

RecommendNthUpTest中测试推荐UP主的：

  • 基础排序逻辑（按兴趣与影响力乘积降序，ID升序打破平局）
  • 纯方法特性（调用不改变网络状态）
  • 各种异常抛出条件（用户不存在、排名非法、无视频、冷启动）

测试策略心得

  • 不要信任"看起来对"的优化：mutualFollowingSum的实时维护逻辑比重新计算更容易出错，必须有一个基于JML原始定义的参考实现做对照测试。
  • 关注pure方法的副作用：JUnit测试中对纯方法调用前后的状态快照比对非常有效。
  • 边界数据构造：全部用户互相关注、全部不关注、只有两个用户互粉/不互粉等极端情况是测试的重点。

三次作业的迭代过程

Week1 → Week2 的变化

  1. 视频增加类型与热度系统

    • Video新增type字段
    • 引入热度计算公式
    • Network增加popularMap缓存每类最热门视频，通过updatePopularCache和reScanCategory维护

  2. 用户交互系统

    • 新增硬币coins
    • 新增观看记录watchedVideos
    • 新增点赞likedVideos
    • 新增贡献者系统contributors/contributions

  3. 评论系统

  4. 最长递减序列

    • 新增queryLongestDecSeq，使用记忆化DFS + ldsCache实现

Week2 → Week3 的变化

  1. 兴趣计算与用户画像

    • User新增typeCounts记录各类视频的观看次数
    • getInterest公式
    • getProfile返回7个类型的兴趣值列表，构成用户画像

  2. 影响力系统

    • User新增influenceMap，UP主的影响力按类型累计
    • 观看/点赞/投币/转发都会给UP主对应类型增加不同权重的影响力

  3. 推荐算法

    • recommendVideo：基于用户兴趣与视频热度的乘积推荐
    • recommendNthUp：计算候选UP主与当前用户的匹配度，取第n名
    • queryMostInfluentialUp：查询某类型影响力最高的用户

  4. 全局查询

    • queryGlobalBestContributor：统计所有UP主的最佳贡献者，找出现频率最高的用户ID

如何发现已有方法/容器在迭代中的变化？

Week2和Week3发布时，官方包会提供新的接口文件，仅根据IDEA的报错提示进行修改可能会有遗漏。可以进行 逐文件diff对比。

容器层面的变化主要通过阅读新JML中assignable子句和ensures子句发现。例如Week3的JML中如果提到User需要维护typeCounts，那么我就知道需要在User类中新增HashMap<String, Integer>容器，并在watchVideo中更新它。

如何发现程序的性能瓶颈？

性能瓶颈主要通过方法的时间复杂度分析和互测/强测的TLE反馈发现：

  1. 警惕嵌套循环和全量遍历：

    • Week1的queryShortestPath使用BFS是O(V+E)，在稀疏图上可接受。但如果图很稠密且查询很多，需要考虑优化（本单元中未做进一步优化，因为BFS已经是相对优的解法）。
    • queryLongestDecSeq如果对每个用户做DFS不缓存，复杂度会爆炸。记忆化搜索（ldsCache）是必须的。

  2. 利用数据结构的特性：

    • HashMap的O(1)查找替代ArrayList的O(n)查找，用于users、videos、following等核心容器。
    • HashSet用于watchedVideos、likedVideos等需要去重和快速判断包含关系的场景。

  3. 实际测试验证

架构演进心得

三次迭代保持了较好的向后兼容性：

  • 核心数据结构（users、videos的HashMap结构）始终未变
  • User和Video的内部容器随着功能增加而扩展，但通过封装良好的方法对外提供服务

Bug分析

本单元在编写过程中几乎没有出现很复杂的Bug，且都能简单修复。但在强测/互测中确实出现了以下问题：

  • 列表维护不当。这是在第二单元中就困扰我许久的问题，这次依旧让我栽了跟头。Week1的实现只从unreadVideos移除，Week2要求同时从receivedVideosList中移除，否则queryReceivedUnwatchedVideos可能返回已观看的视频。
  • Week1中一开始使用了双向BFS，但是由于算法功底不熟练，导致出现了逻辑问题。后续改成普通BFS后成功修复了。

Bug出现的原因归纳

  • 顺序依赖的忽视：很多Bug源于"先做A再做B"和"先做B再做A"结果不同。在关注关系维护中，判断状态和修改状态的顺序极其敏感。
  • 迭代时未回溯已有方法：Week2改了watchVideo的语义，但Week1的queryReceivedUnwatchedVideos依赖的数据结构没变，导致新旧逻辑不一致。
  • 边界情况的遗漏：如空集合、全互粉、无贡献者等极端情况，往往是JML有明确定义但实现时容易忽略的。

大模型使用心得

规格驱动开发时大模型的优势

在本单元中，大模型主要在以下场景提供了帮助：

  1. JML阅读辅助：将复杂的JML规格翻译成自然语言描述，帮助快速理解方法的前置/后置条件。这是我认为大模型与任务结合最完美的一次，也让我心安理得的频繁用大模型进行JML阅读。不过，大模型偶尔产生会产生偏差，关键约束仍需人工核对。

  2. 测试用例生成：为复杂方法（如cleanSpamComments、recommendNthUp）生成边界测试思路和异常场景，补充了手动测试的盲点。

JML"击鼓传花"游戏感悟

逻辑Bug分析

传递过程中难免出现逻辑Bug，但大多数Bug并不是JML书写者的问题。

自然语言到形式化语言的转换是有损的。即使是同一个中文需求，不同人写出的JML可能对应完全不同的实现。很多"Bug"不是在代码层面，而是在规格层面就已经产生了。

换句话说，许多自然语言的描述就是不严谨的。即使是很熟练的JML使用者，写出的JML也难免出现逻辑偏差。

在传递过程中，需求、边界是否发生了变化？

  • 需求意图变化：原始需求是"A功能"，传了两轮后变成了"A功能的子集"或"A功能的过度泛化版"。例如最初只是"关注用户"，后面被加入了"不能关注已注销用户"等原本不存在的约束。

  • 边界条件变化：最初需求没有考虑边界，传着传着有人补上了边界，但补上的是自己的理解而非原始需求。比如对空列表的处理，有人写requires size > 0，但实际上需求允许空列表。

  • 副作用范围变化：一个人写assignable \nothing表示纯方法，下一个人添加了ensures后置条件却忘了同步修改assignable，导致规格自相矛盾。

错误的JML比错误的代码更隐蔽，编写JML比编写code更考验思维的严谨性。

统一理解&减少信息差

建立规格评审机制： 在写JML之前，先用所有人都能看懂的自然语言明确描述需求意图、业务规则和边界条件，JML只是需求的"实现"而非替代品。关键方法的JML应当由多人审阅，重点不是语法，而是"这个JML是否准确翻译了自然语言需求"。

约定架构和容器规范： 动手写代码前，团队需要统一核心数据结构、性能底线以及异常抛出顺序。统一的约定可以避免不同人写出不同的实现。

增强信息同步： 击鼓传花中信息差的核心原因是"每个人只看到了上一个人的输出，不知道最初的需求"，因此需求变更必须同步给所有相关成员而非仅直接下游。关键决策（如为什么用HashMap而非ArrayList、为什么增量维护）要留痕在代码注释或设计文档中。

利用测试统一认知： 测试用例是比JML更直观的文档，团队共享边界测试用例能大幅减少理解偏差。对于复杂查询方法，可以维护一个严格按JML字面意思实现的参考版本，任何优化实现都需与其在大量随机数据上对比，确保语义一致。

总结

规格是团队开发的契约。契约一旦模糊，后续所有基于此契约的代码都会偏离方向。在多人协作中，与其追求"每个人都读懂了JML"，不如追求"每个人都参与了JML的制定和评审"——只有参与过，才能真正理解设计背后的业务意图。