企业官网建设流程全解析

Unit3 总结博客：JML 与规格化设计

总体说明：U3 JML 与规格化设计

从个人体验来看，第三单元给我的第一印象并不是“难”，而是“规范”和“重视”不能像我一样因为U2基本无伤就大意美美栽跟头。前两个单元的困难更多来自题目本身：U1 表达式化简需要反复处理各种边界和性能问题，U2 电梯调度则要求在多线程环境下考虑互斥、同步、调度策略以及线程结束条件。相比之下，U3 的业务逻辑虽然也在不断扩展，但整体复杂度更加可控，实现过程也没有前两个单元那样强烈的不确定性。

第三单元的三次作业围绕一个在线视频平台逐步展开：HW9 搭建基础社交网络，HW10 在社交关系之上加入观看、点赞、投币、转发、评论和勋章等互动行为，HW11 进一步把已有的行为数据转化为视频推荐、UP 主推荐、用户画像和全局贡献查询。和前两个单元相比，本单元最明显的变化是：需求不再主要以自然语言描述，而是大量写在 JML 规格里。代码要做的事情不只是“看起来符合题意”，而是逐条满足 requires、ensures、assignable、pure 以及异常优先级等约束。

因此，虽然 U3 在算法难度和工程挑战上并不算突出，但它提供了一种完全不同的开发体验。它让我意识到，程序正确性不仅来自“样例能过”或“逻辑上差不多”，更来自清晰的契约约束。JML 将原本可能模糊的自然语言需求转化为更精确的规格，使实现者能够围绕同一套标准编写代码，也使测试者能够更有针对性地检查程序是否满足预期行为。

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

JML 是一种用于 Java 程序的形式化规格语言。它通过前置条件、后置条件、类不变式、副作用声明、异常行为等机制，精确描述一个方法或一个类“应该做什么”。

我认为 JML 的主要价值在于，它能够把程序应满足的条件和行为结果提前描述清楚。这样在编写 JUnit 测试时，就可以根据方法的前置条件、后置条件以及可修改范围来设计测试样例，测试思路会更加明确。

同时，JML 相比直接阅读 Java 源码更偏向于描述“程序应该做什么”，而不是“程序具体怎么做”。因此它能够减少复杂实现细节带来的干扰，使代码约束更加清晰，也更容易检查实现是否符合要求。

此外，JML 还比较适合与大模型辅助编程结合。由于规格说明本身比较规范，大模型可以依据这些条件生成初步代码或测试用例，从而在一定程度上提高开发效率。

规格驱动开发则是以规格作为开发的核心资产，而不是直接以代码为中心。它的工作流程大致可以分为三步。

第一步是先写规格。通过 JML 或其他形式化描述，明确方法的输入要求、输出结果、状态变化范围、异常行为和边界条件。这个阶段的重点是消除需求歧义。

第二步是根据规格编写实现。在实现时，开发者需要在requires、ensures、assignable和signals的约束下填充具体代码。JML 并不限制内部算法，因此可以根据数据规模和性能需求选择合适的数据结构。

第三步是通过测试验证实现是否满足规格。这里的测试不仅要检查返回值是否正确，还要检查异常是否按规格抛出、对象状态是否被正确修改、查询方法是否保持无副作用。尤其是在本单元中，JUnit 测试的意义就在于将 JML 规格转化为可执行的检查，从而验证代码是否真正符合契约。

通过第三单元，我对规格驱动开发的体会是：它把“读懂题目再写代码”的过程，转化为了“依据契约实现行为”的过程。相比自然语言题面，JML 更精确，也更容易让开发者、测试者和评审者围绕同一套标准讨论程序正确性。

二、JUnit 测试经验总结

本单元每次作业都要求为指定方法编写 JUnit 测试。三次测试目标分别对应queryMutualFollowingSum、clean_spam_comments和recommend_Nth_up。这使我对单元测试的理解从“构造几个样例看输出”逐渐转变为“根据规格系统性覆盖行为”。

首先，JUnit 测试应从 JML 出发，而不是只从样例出发。以queryMutualFollowingSum为例，测试时不仅要验证互相关注数量是否正确，还要覆盖以下情况：空网络、只有单向关注、形成互相关注、取消互相关注、多组互相关注并存等。同时，由于该方法是查询方法，还要检查调用前后用户关系、视频列表等状态没有发生改变。

其次，测试要关注边界和状态变化。对于clean_spam_comments，不能只测试“有评论被删除”的普通情况，还应测试没有关键词命中、所有评论都被删除、关键词在同一评论中出现多次、删除后评论 ID 与评论内容仍然一一对应等情况。由于评论系统涉及两个并行容器commentIds与commentContents，测试时要特别检查删除操作是否破坏了二者的对应关系。

再次，推荐类方法更需要关注排序规则和 tie-break。recommend_Nth_up的核心不是简单返回某个用户，而是按照用户兴趣和 UP 主影响力计算得分，再按名次返回候选 UP。测试时必须覆盖分数不同、分数相同按 id 决定顺序、用户已经关注的 UP 不能被推荐、候选数量不足时抛出冷启动异常、rank 非法时抛出异常等情况。

我在测试中的一个重要经验是：不要只写“正向样例”，还要写“反向样例”。正向样例证明程序在常见情况下能工作，反向样例才能暴露边界错误、异常错误和副作用错误。尤其是 JML 作业中的评测会使用带有特定错误的方法实现，JUnit 的目标不是证明自己代码正确，而是尽量区分正确实现和错误实现。因此，测试用例应具有针对性，能够击中常见错误点。

因此，我总结出的 JUnit 测试策略是：

1. 先从 JML 中提取正常行为、异常行为和副作用要求；
2. 再为每个行为设计至少一个基本测试和一个边界测试；
3. 对查询方法额外检查调用前后状态是否一致；
4. 对修改方法检查应修改的状态是否修改、不应修改的状态是否保持；
5. 对排序、排名、最大值、最小值等方法重点测试 tie-break；
6. oo评测反馈也是一个很好的信息，借助大模型或可以快速定位bug

三、三次作业的迭代过程分析，以及如何发现已有方法和容器的变化

1. 第一次作业：建立基础网络模型

第一次作业主要实现用户、视频和关注关系。我的设计以Network作为全局管理类，使用HashMap<Integer, User>和HashMap<Integer, Video>分别维护用户和视频。User内部维护关注列表、粉丝列表和接收视频列表，Video只保存视频 id 和上传者 id。

这一阶段最核心的操作包括添加用户、上传视频、关注与取关、观看视频、查询未观看视频、查询粉丝年龄比例、查询互相关注数量和最短路径。由于图结构已经出现，queryShortestPath使用 BFS 进行搜索；而queryMutualFollowingSum如果每次全图遍历，复杂度较高，因此我从第一次作业开始就维护了mutualFollowingCount。

具体而言，当id1关注id2时，如果id2已经关注id1，则说明新形成了一组互相关注关系，此时互相关注数加一；当id1取消关注id2时，如果原本id2也关注id1，则说明破坏了一组互相关注关系，此时互相关注数减一。这样一来，queryMutualFollowingSum只需要直接返回缓存值即可。

这一阶段让我意识到，虽然 JML 给出的通常是“结果定义”，但实现时应尽早识别哪些查询会被频繁调用，并将其转化为增量维护问题。

2. 第二次作业：加入互动系统与性能优化

第二次作业在第一次作业基础上加入了硬币、点赞、投币、转发、评论、勋章、贡献者、最长下降序列等功能，状态复杂度明显上升。此时如果仍然沿用第一次作业中简单的容器结构，很多操作会退化为线性扫描，容易在强测中出现性能问题。

这一阶段我做了几类重要迭代。

第一，针对视频热度查询，我使用videosByType将不同分区的视频分别维护在TreeSet中，并按照热度降序、id 升序排序。这样queryMostPopularVideo可以直接取对应分区集合的首元素，而不必每次遍历所有视频。

第二，针对粉丝年龄比例，我不再每次查询时遍历所有粉丝，而是在User中维护followerAgeCnt数组。当新增或删除粉丝时同步更新对应年龄段计数，查询时只需要用计数除以粉丝总数即可。

第三，针对未观看视频列表，我从简单的LinkedList进一步演化为链表加索引结构。由于转发和上传会频繁把视频插入接收列表头部，而观看视频时又需要删除某个视频的所有接收记录，单纯链表删除会产生较高复杂度。因此我维护了receivedIndex，将视频 id 映射到链表节点列表，实现更高效的批量删除。

第四，针对最短路查询，我将普通 BFS 优化为双向 BFS。因为关注关系图可能较大，从起点和终点同时扩展可以显著减少搜索空间，尤其是在路径较短但图较大的情况下效果更明显。

第五，针对queryLongestDecSeq，我使用 dirty flag 和缓存。只有在用户关系发生变化时才把缓存标记为失效；查询时如果状态没有变化，则直接返回缓存值。这样可以避免重复计算。

这一阶段最大的体会是：迭代开发不是不断堆功能，而是要重新审视已有容器是否仍然适合新需求。新方法一旦引入新的高频查询，原有容器就可能成为瓶颈。

3. 第三次作业：推荐系统与全局排名维护

第三次作业新增了智能推荐视频、推荐 UP 主、查询用户画像、查询最有影响力 UP、查询全局最佳贡献者等功能。相比前两次，这一次对“派生状态”的维护要求更高。

为了支持推荐系统，我在User中新增了typeCounts，用于记录用户在各分区观看过的视频数量，并基于此计算用户对不同分区的兴趣度。同时，UP 主的影响力也需要按分区维护，因此我在用户中加入influence数组，并在视频热度变化时同步更新上传者的对应分区影响力。

为了支持queryMostInfluentialUp，我维护了usersByInfluenceType，即每个分区一个按照影响力排序的TreeSet<User>。当某个视频的热度因为播放、点赞、投币或转发发生变化时，需要先从排序集合中删除对应 UP 主，更新影响力，再重新插入。这个过程体现了使用有序集合时必须注意的一点：如果排序关键字发生变化，不能直接修改对象后留在集合中，否则集合内部顺序可能失效。

为了支持queryGlobalBestContributor，我维护了每个用户成为多少个 UP 主“最佳贡献者”的全局排名。每次投币后，某个 UP 主的最佳贡献者可能变化，因此需要比较更新前后的最佳贡献者 id，并同步维护全局TreeSet<ContributorRank>。这比每次查询时扫描所有 UP 主更复杂，但查询效率更高。

这一阶段我对“规格等价实现”的理解更加深入。JML 可能用量化表达定义“第 N 个推荐 UP”，但真正实现时，可以使用优先队列维护前 rank 个候选者，而不必对所有候选完整排序。只要返回结果满足规格中的排序和过滤条件，内部实现可以自由优化。

4. 如何发现已有方法和容器在迭代中的变化

我总结出一套比较有效的迭代检查方法。

首先，对比接口变化。每次新作业发布后，我会先查看新增方法、修改方法和删除方法，重点关注方法签名、异常列表、返回类型和构造方法变化。例如第二次作业中Video构造方法新增了type参数，第三次作业中推荐相关方法加入了新的异常类型，这些都会直接影响类设计。

其次，对比对象状态变化。新增方法往往意味着新增状态。第二次作业中，用户新增硬币、观看记录、点赞记录、勋章和贡献者；视频新增播放量、点赞数、转发数、投币数和评论区；第三次作业中，用户又新增分区观看计数和已发布视频集合。这些状态不能零散地添加，而要思考它们之间的同步关系。

再次，从查询方法反推容器设计。如果某个查询要求频繁返回最大值、第 N 名、最短路径、全局最优对象，那么简单ArrayList或全量遍历通常不是最合适的选择。此时应考虑是否需要HashMap、HashSet、TreeSet、优先队列、缓存或索引结构。

最后，检查派生状态的更新点。凡是通过缓存、计数器、有序集合维护的状态，都必须列出所有可能改变它的方法。例如视频热度会受到观看、点赞、投币、转发影响；UP 主影响力依赖其视频热度；用户兴趣依赖观看记录；互相关注数依赖关注与取关。只要漏掉一个更新点，就会造成查询结果与真实状态不一致。

四、如何发现程序性能瓶颈，以及对性能优化的反思

我主要通过三种方式发现性能瓶颈。

第一是复杂度估算和与同学对比新增的关键方法复杂度 要是差很多就是自己的问题了。根据指令条数和数据范围，先估计每个方法的最坏复杂度。如果某个查询是 O(n²)，而它可能被频繁调用，就需要优先优化。例如互相关注数量、分区最热视频、最有影响力 UP、全局最佳贡献者等，如果每次查询都全量扫描，在强数据下风险较大。

第二是构造压力数据。针对某个方法构造极端输入，例如大量用户形成稠密关注关系、大量视频集中在同一分区、大量评论包含同一关键词、大量投币导致贡献者排名频繁变化等。通过运行时间和输出结果观察瓶颈位置。

我搭建了评测机并采用不同的数据生成策略，通过诱导GPT针对后续新增的查询方法设计不同的数据点生成模式来定向测试/hack。

第三是从容器操作本身判断以及用空间换时间。ArrayList的中间删除、链表的按值查找、全量排序、重复 BFS 都是常见瓶颈。比如未观看视频列表既需要头插，又需要按视频 id 删除所有节点，因此我最终使用链表加索引；视频热度排名需要频繁查询最大值，因此使用TreeSet；第 N 个 UP 推荐只需要前 rank 名，因此可以用优先队列降低排序成本。

这说明，在本单元中，很多算法优化更像是“理论上的最优实现”，而不是通过强测必须采用的实现方式。部分测试数据（KMP）没有强行卡住朴素方法，使得不少同学即使按照最直接的方式实现，也能顺利通过。

五、自己程序中的 bug 与原因分析

第一次作业中因为过完了U2进入新手膨胀期多个方法复杂度超标导致强测多个CTLE败北。但吸取教训之后的两次作业均无bug出现。

因此，在之后的开发中，我会更加重视以下几点：

1. 谨慎
2. 编码前整理每个方法的正常行为和异常行为；
3. 对每个派生状态列出所有更新入口；
4. 对使用TreeSet等依赖排序关键字的容器，统一封装修改流程；
5. 对测试辅助方法也进行认真实现；

六、大模型与第二次研讨课“JML 击鼓传花”的感悟

1. 大模型在规格驱动开发中的优势

我并没有把代码实现完全交给大模型完成，但在开发过程中确实会把它作为辅助工具使用。例如，当我不确定某段逻辑怎样实现更高效，或者需要比较不同实现方案的复杂度时，我会向大模型寻求思路和建议。

在规格驱动开发中，大模型的作用相对明显。JML 本身具有较强的形式化特征，语义描述也比较明确。因此，当我把官方接口中的方法规格提供给大模型，让它根据规格分析或尝试实现时，它通常能够给出语义上较为准确的代码。不过，这类结果有时会更关注“正确性”，而忽视性能问题。若在提示中明确要求考虑复杂度或优化实现，得到的方案往往会更加实用。

相比之下，在单元测试编写方面，我对大模型的使用更多一些。我会将方法对应的 JML 规格以及作业要求一并提供给它，让它辅助生成测试用例。整体来看，大模型生成的测试通常覆盖面较广，质量也较高。但它对assignable约束的检查不够敏感，因此这部分我一般会再进行人工补充和修正。

在第三次作业的互测阶段，我尝试用大模型排查其它可能的bug并hack成功。

2. 第二次研讨课：“JML 规格传声筒”小游戏感悟

在 Unit3 第二次研讨课中，课程安排了一个名为“规格传声筒（JML Telephone）”的小游戏。游戏以 6 人为一组，每个人准备一个带有边界条件的方法签名和业务场景。随后，纸张在组内依次传递，同学们在自然语言规格（NL）和 JML 规格之间反复翻译。最后，再比较最初的自然语言需求和最终的 JML 规格是否保持逻辑等价。

我拿到的题目是“最高优先级任务轮询（Priority Task Query）”。题目要求：查询并返回当前任务队列中优先级最高的任务 ID，但不将该任务移出队列；如果多个任务优先级并列最高，则返回其中任务 ID 最小的那个；如果任务队列为空，则抛出EmptyQueueException。

这个题目看起来只是一个简单查询，但实际写成 JML 时并不简单。它不仅要说明返回值来自队列中的某个任务，还要用全称量词表达“该任务优先级不低于所有其他任务”，同时还要补充“优先级相同时返回 ID 最小者”这个边界条件。这个 tie-break 规则很容易在传递过程中丢失。

3. 发现的 JML bug 与规格漏洞

在这次游戏中，我主要发现了三个问题。

第一，异常行为容易被遗漏。题目明确要求当任务队列为空时抛出EmptyQueueException，因此 JML 中不能只写requires size > 0，还应在exceptional_behavior中用signals描述size == 0时的异常行为。否则，空队列情况就会变成未定义行为。

第二，查询方法的副作用约束容易被忽略。题目要求“查询”而不是“删除”，因此方法不能改变队列内容。JML 中应使用assignable \nothing，方法也可以标注为pure。如果忘记这一点，实现者可能会把这个方法误写成取出并删除最高优先级任务。

第三，最高优先级并列时的 ID 比较容易丢失。如果 JML 只写“返回某个优先级最高的任务 ID”，那么当(id=3, priority=10)和(id=1, priority=10)同时存在时，返回 3 也会被认为合法。但原始需求要求必须返回 1。因此，规格必须同时约束“优先级最高”和“同优先级下 ID 最小”。

4. 传递过程中的需求变化

这次游戏让我明显感受到，需求在传递中很容易被弱化。对于这个题目来说，最典型的变化就是：最初需求是“返回优先级最高且 ID 最小的任务”，但经过几轮 NL 和 JML 转换后，可能只剩下“返回优先级最高的任务”。虽然只少了一个条件，但方法的确定性已经发生变化。

另外，“队列为空时抛异常”和“不将任务移出队列”也属于容易被忽视的边界要求。它们不像“返回最高优先级任务”那样显眼，但却直接决定了方法在特殊情况下的正确性。

5. 对多人组队编程的启发

这个游戏说明，在多人协作编程中，需求不能只靠口头理解。即使每个人都没有故意修改需求，多次转述后，边界条件和业务细节仍然可能丢失。

因此，在组队编程时，我认为应当建立统一的需求文档，并在接口实现前进行简单评审。对于类似本题的方法，文档中必须明确写出：队列非空时返回最高优先级任务 ID；优先级并列时返回 ID 最小者；队列为空时抛出异常；查询方法不能修改队列状态。

同时，还应配合测试样例验证理解是否一致。例如，测试用例中应包含空队列、单个任务、多个不同优先级任务，以及多个最高优先级任务并列的情况。这样才能避免规格看似正确，但实际已经偏离原始需求的问题。

通过这次“规格传声筒”游戏，我更深刻地理解到，JML 的价值不仅是让规格看起来严谨，更重要的是把自然语言中容易遗漏的边界条件固定下来，帮助团队在实现前形成统一、可验证的理解。

总结

！！！重视和仔细必须一以贯之！！！

通过本单元三次作业，我对面向对象设计的理解从“类和方法的组织”进一步扩展到“规格、状态与性能的统一”。JML 规格告诉我们程序应当表现出什么行为，JUnit 测试帮助我们验证程序是否满足这些行为，而数据结构和缓存设计决定程序能否在较大规模下高效运行。

与此同时，本单元也让我看到，规格驱动开发最大的价值在于减少歧义。只要严格依据 JML，就可以把“我觉得应该这样”转化为“规格要求必须这样”。但同时，规格只定义行为，不保证性能。因此，一个高质量实现不仅要正确翻译规格，还要根据指令规模和查询频率设计合适的数据结构。

总的来说，U3 虽然没有 U1 和 U2 那样强烈的算法压力或并发压力，但它让我更系统地理解了规格化设计的意义。今后在类似任务中，我会继续坚持先读规格、再建状态模型、再设计容器、最后写测试和优化的开发流程。只有这样，才能在保证正确性的基础上，写出结构清晰、行为稳定、易于维护的程序。