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 还比较适合与大模型辅助编程结合。由于规格说明本身比较规范大模型可以依据这些条件生成初步代码或测试用例从而在一定程度上提高开发效率。关键字 / 表达式含义示例requires前置条件规定方法正常调用前必须满足的条件requires x 0;ensures后置条件规定方法正常结束后必须满足的结果ensures \result x y;invariant类不变式规定对象在稳定状态下必须始终满足的条件invariant age 0;assignable副作用声明规定方法允许修改哪些状态assignable size, elements;pure纯方法表示方法不应修改对象状态public pure boolean contains(int id);signals异常行为规定特定条件下应抛出的异常signals (Exception e) condition;\old(expr)表示方法执行前表达式的值ensures x \old(x) 1;\result表示方法的返回值ensures \result ! null;\forall / \exists一阶逻辑量词用于描述“所有”或“存在”(\forall int i; 0 i i size; arr[i] 0)规格驱动开发则是以规格作为开发的核心资产而不是直接以代码为中心。它的工作流程大致可以分为三步。第一步是先写规格。通过 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 测试策略是先从 JML 中提取正常行为、异常行为和副作用要求再为每个行为设计至少一个基本测试和一个边界测试对查询方法额外检查调用前后状态是否一致对修改方法检查应修改的状态是否修改、不应修改的状态是否保持对排序、排名、最大值、最小值等方法重点测试 tie-breakoo评测反馈也是一个很好的信息借助大模型或可以快速定位bug三、三次作业的迭代过程分析以及如何发现已有方法和容器的变化1. 第一次作业建立基础网络模型第一次作业主要实现用户、视频和关注关系。我的设计以Network作为全局管理类使用HashMapInteger, User和HashMapInteger, 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即每个分区一个按照影响力排序的TreeSetUser。当某个视频的热度因为播放、点赞、投币或转发发生变化时需要先从排序集合中删除对应 UP 主更新影响力再重新插入。这个过程体现了使用有序集合时必须注意的一点如果排序关键字发生变化不能直接修改对象后留在集合中否则集合内部顺序可能失效。为了支持queryGlobalBestContributor我维护了每个用户成为多少个 UP 主“最佳贡献者”的全局排名。每次投币后某个 UP 主的最佳贡献者可能变化因此需要比较更新前后的最佳贡献者 id并同步维护全局TreeSetContributorRank。这比每次查询时扫描所有 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出现。因此在之后的开发中我会更加重视以下几点谨慎编码前整理每个方法的正常行为和异常行为对每个派生状态列出所有更新入口对使用TreeSet等依赖排序关键字的容器统一封装修改流程对测试辅助方法也进行认真实现六、大模型与第二次研讨课“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”那么当(id3, priority10)和(id1, priority10)同时存在时返回 3 也会被认为合法。但原始需求要求必须返回 1。因此规格必须同时约束“优先级最高”和“同优先级下 ID 最小”。4. 传递过程中的需求变化这次游戏让我明显感受到需求在传递中很容易被弱化。对于这个题目来说最典型的变化就是最初需求是“返回优先级最高且 ID 最小的任务”但经过几轮 NL 和 JML 转换后可能只剩下“返回优先级最高的任务”。虽然只少了一个条件但方法的确定性已经发生变化。另外“队列为空时抛异常”和“不将任务移出队列”也属于容易被忽视的边界要求。它们不像“返回最高优先级任务”那样显眼但却直接决定了方法在特殊情况下的正确性。5. 对多人组队编程的启发这个游戏说明在多人协作编程中需求不能只靠口头理解。即使每个人都没有故意修改需求多次转述后边界条件和业务细节仍然可能丢失。因此在组队编程时我认为应当建立统一的需求文档并在接口实现前进行简单评审。对于类似本题的方法文档中必须明确写出队列非空时返回最高优先级任务 ID优先级并列时返回 ID 最小者队列为空时抛出异常查询方法不能修改队列状态。同时还应配合测试样例验证理解是否一致。例如测试用例中应包含空队列、单个任务、多个不同优先级任务以及多个最高优先级任务并列的情况。这样才能避免规格看似正确但实际已经偏离原始需求的问题。通过这次“规格传声筒”游戏我更深刻地理解到JML 的价值不仅是让规格看起来严谨更重要的是把自然语言中容易遗漏的边界条件固定下来帮助团队在实现前形成统一、可验证的理解。总结重视和仔细必须一以贯之通过本单元三次作业我对面向对象设计的理解从“类和方法的组织”进一步扩展到“规格、状态与性能的统一”。JML 规格告诉我们程序应当表现出什么行为JUnit 测试帮助我们验证程序是否满足这些行为而数据结构和缓存设计决定程序能否在较大规模下高效运行。与此同时本单元也让我看到规格驱动开发最大的价值在于减少歧义。只要严格依据 JML就可以把“我觉得应该这样”转化为“规格要求必须这样”。但同时规格只定义行为不保证性能。因此一个高质量实现不仅要正确翻译规格还要根据指令规模和查询频率设计合适的数据结构。总的来说U3 虽然没有 U1 和 U2 那样强烈的算法压力或并发压力但它让我更系统地理解了规格化设计的意义。今后在类似任务中我会继续坚持先读规格、再建状态模型、再设计容器、最后写测试和优化的开发流程。只有这样才能在保证正确性的基础上写出结构清晰、行为稳定、易于维护的程序。