BUAA-OO-Unit3总结
JML和规格驱动开发
JML，即Java Modeling Language，是一种用形式化语言来描述程序行为的语言，用于对Java程序进行规格化设计。在三次作业中，我认为程序规格就是要描述清楚程序的输入、输出、变量变化、对外接口等内容，以达到用严谨的语言对程序功能进行无二义性的描述的效果。
恰好在学习这一单元的时候，我看到了一句话，说“一直以来所谓的Computer Science，其实既不是Computer，也不是Science，而是形式化的过程。无论是图灵机、打孔纸带，还是机器学习、人工智能，无一例外。“我现在对这句话深以为然。计算机的世界，其实就是人类用逻辑构建出的一个确定输入输出的世界，而实现这一点，就是用形式化的语言去描述——算法也好、输出规格也罢。JML当然没有描述算法，但这只是因为JML的用途如此——Anyway，JML的学习和前面对形式化的思考，让我深刻理解了，整个计算机科学是建立在离散数学的基础上的这句话。
JUnit测试的经验
在面对JML进行JUnit测试时，思路往往会清晰许多。所有不符合要求的输入的情况是否抛出了规定异常、正常输入是否得到了符合要求的输出、保证不会改变的状态是否没有改变、边界输入或特殊情况是否得到了正确输出、压力测试是否也能符合要求，是JUnit测试必须包含的几个方面。
值得一提的是，我在JUnit测试的编写中大量借助了AI的力量，也由此产生了一些思考，这会放在后面大模型的使用部分说明。
迭代过程
三次作业的迭代，困难的其实并不是架构设计（因为方法都在JML中唯一定义了），而是性能产生的瓶颈。而性能问题，在我的作业中，基本上属于容器问题和算法问题这两大类。容器问题，也就是选择的容器并不合适，尤其是使用List等线性容器，可能涉及到大量的遍历导致性能下降，或者本次作业性能尚可而下次作业的方法使用该容器会导致复杂度爆炸。算法问题，更关键的并不是会不会这个算法——因为这些算法或多或少在大一程设时都听过，就算真的不会或者没想到的，让AI思考一下最优算法现在的AI是可以做到的；相反，是你在编写过程中受到JML描述影响，无脑选择了最朴素的暴力算法，或者没有规定AI的算法选择，AI受到JML的影响，很容易写出这样的算法，导致性能下降。最朴素的检查方式我认为是去计算每个方法的时间复杂度，重点关注那些O(n^2)或者更大的，在强测的压力下这些方法大概率会超时。
Bug及原因
由于JML唯一定义了方法的行为，所以本单元出现的Bug不多（尤其在AI的加持下），更多的则是性能问题。不过值得一提的是，我的代码和互测中其他同学的代码中大量出现了一个问题，就是由于一些原因，为同一个事物（比如同一个视频）创建了多个不同的对象，并在链表等容器中重复添加时，删除行为只删除了其中一个对象，导致结果出现错误，而且这一bug在前两次作业的不同场景中均有涉及。（由于多个同学的代码均出现了此问题，我不得不怀疑是不是模型厂商互相蒸馏，出现了相同的短板）
JML下大模型的使用
下文全部基于个人的大模型使用经验，大模型选择为Claude Code+DeepSeek v4 pro、Antigravity+Gemini 3.5 Flash。
JML与Coding
前文说过了，计算机的世界，就是形式化的世界，这对于我们编写Prompt一样适用。理论上现阶段我们可以相信，如果我们给出了对我们想要做的事情的绝对严谨的表述——包括但不限于输入的要求、输出相对于输入的关系、算法的选择、所有需要考虑的特殊情况、不满足要求时的行为等，AI能够给出完美符合我们要求的代码（或者其他）。而自然语言，永远不可能百分百精确描述——尽管现在人们在做的，不管是prompt也好、skills也好，都是在试图用自然语言构造形式化的表述，以此来规范AI的行为。而JML，恰好就是另外一个选择。我们可以使用一种形式化语言，在不去真的编写代码的情况下，完成对输入输出的形式化规范，以此限定大模型的行为。当然，由于JML并未规范具体的算法选择，而受限于底层原理，AI往往倾向于给出接近JML描述的暴力算法，而这往往是不符合我们的性能要求的。我的解决办法是强调使用最优算法，并进行了时间复杂度的限制，同时强调我们的数据规模和运行时间要求，尤其对于常见算法，直接给出具体的算法选择，以及容器的选择上，直接给出尽可能使用HashMap等时间复杂度为O(1)的容器的要求，这样AI往往能给出比较符合我们的性能要求的算法。
JUnit单元测试
在编写单元测试时，AI往往不能一次给出全面的、能通过所有测试点的JUnit测试方案。此时，如果反复强调考虑所有可能的情况、加强边界测试压力测试、严格检查JML的每一个要求或类似的指令，他会在一次次的修改中增加无数冗余的测试，直到最后测试长度达到近两千行——而事实上只需要七八十行就可以覆盖评测机的要求。相反，我给出具体的测试要求——具体到不同的不符合要求的组合抛出的异常的规定，他反而能一次改对。当然，前一次是使用DeepSeek v4，后一次是使用Gemini 3.5 flash，不排除模型能力差距——毕竟在Gemini新版本刚刚推出且发布会大肆宣传的时期，他还不至于变成大号豆包。
不管怎么说，根据JML要求编写JUnit单元测试，这两个模型仍有缺陷，不过在给出严格的prompt后，大模型是可以胜任这个任务的。
JML“击鼓传花”
本单元最后一次研讨课，我们进行了JML的击鼓传花游戏，具体规则是每个人用自然语言写一个题目场景和所要实现的功能，并规定了函数签名。这张纸向下传递，每一个人都进行自然语言-JML描述/JML描述-自然语言的翻译，直到最后，去核对最后的描述和第一人的描述是否一致。这个游戏的结果是可预见的——只使用自然语言完成该实验都会有很大的信息损失，更不要说要在短时间内进行大部分人都不太熟悉写法的JML的转译以及其他人的JML的理解了。在实际完成的过程中，我们对最终结果进行复盘，可以发现出现了很多JML的描述与自然语言不符或不完整、自然语言描述对JML进行了大量的简化、JML完全错误、自然语言与JML有较大偏差等情况，导致很多人的最终结果与初始题目存在较大的偏差，甚至可能是驴唇不对马嘴、前门楼与胯骨轴、令人啼笑皆非的结果。由此，我认为，在组队编程时，我们需要有一个经过商讨的、全组同意的方案，并形成正规的文件，内容包括但不限于开发环境与运行环境、开发工具、实现的核心功能、分工情况、每个分工的具体内容、每个任务的功能与副作用、暴露的接口、算法的性能要求、编码规范、测试方案等，规定越细效果越好。同时对于测试方案，应当有规范统一的测试方案，保证团队成员编写的代码通过符合规定的测试后方可并入主分支（或者说是有标准的CI/CD流程，尤其对于庞大复杂的项目而言）。并且该指导书也通过Git或其他方式共享，在发生更改时应通知所有人并得到所有人的确认。并设置歧义、异议申诉解释流程，确保每个成员都能得到正确的理解。只有这样，才能对齐团队成员的颗粒度，保证每一个成员都可以获得正确的要求。