JML单元总结
一、对JML和规格驱动开发的理解
JML 是一种基于 Larch 方法构建的行为接口规格语言（BISL），专门用于对 Java 程序进行规格化设计 。它是一种轻量级的形式化语言，通过与 Java 语言的紧密结合，将规格设计与 Java 的类型设计有机地融合在一起 。
JML 在实际工程和开发中主要有三种用途：
开展规格化设计：将需求转化为逻辑严格的形式化规格，交付给代码实现人员，从而避免使用带有内在模糊性的自然语言进行描述 。
提升代码可维护性：针对既有的代码（尤其是遗留代码）书写对应的规格，极大提高后续维护的可靠性 。
自动化测试与预言：基于规格和源代码，可以设计覆盖率更高的自动化测试，并且能够自动判断测试执行结果，形成测试预言（test oracle） 。
JML 规格主要分为方法规格和类型规格两大类，通过特定的关键字和扩展表达式（如\result,\old(),\forall等）进行严格约束 ：
方法规格 (Method Specifications)：规范了方法执行前后的状态和副作用 。
前置条件 (requires)：要求调用者确保输入参数或前置状态满足要求，否则方法执行结果不保证正确 。
后置条件 (ensures)：方法实现者需要保证执行结果满足该谓词的要求 。
副作用限定 (assignable / modifiable)：明确指出方法执行过程中允许修改的属性，如果方法不产生任何副作用（纯粹访问性），则使用
pure关键字 。行为区分：严谨地区分正常功能行为 (
normal_behavior)和异常功能行为 (exceptional_behavior)。同一个方法的正常前置条件和异常前置条件必须互斥，不能有重叠 。异常情况通过signals或signals_only子句明确抛出的异常类型 。
类型规格 (Type Specifications)：针对类或接口定义的数据成员设计的限制规则 。
不变式 (invariant)：要求对象在所有的“可见状态”（visible state，即对象状态完整的特定时刻，如构造结束、非静态方法执行前后等）下都必须满足的约束特性 。
状态变化约束 (constraint)：用于约束前序可见状态和当前可见状态之间的关系（例如，规定某个计数器变量每次只能加1） 。
而规格驱动开发（契约式设计）带来的思维转变和工程价值主要体现在以下两点：
驱动更好的架构与代码设计：采用规格设计，开发者往往能更容易地获得职责单一、结构简洁的设计与实现 。因为如果一个方法的职责过于复杂，往往会导致其规格难以准确清晰地表达 。这种“写不出规格说明代码设计有问题”的倒逼机制，能有效提升软件质量。
“设计重于实现”的范式转移：在规格驱动的开发模式中，思考和撰写规格的难度在很多情况下甚至高于编写代码本身的难度 。然而，一旦逻辑严密的规格被确定下来，除非涉及极度复杂的算法要求，具体的代码编写就会变成一件相对简单、按图索骥的工作 。
二、JUnit测试的经验
首先，先明确JML的目标：
- 规定方法必须做什么（前置 / 后置）
- 规定方法绝对不能做什么（副作用、异常、篡改数据）
- 覆盖所有正常 / 异常分支（不漏场景）
- 让测试 / 工具能自动验证（可证明、可测试）
其次，决定全局不变量、方法纯净度、副作用、区分正常与异常行为。
最后，需要做到对所有属性的覆盖，约束不可变数据防止偷偷改对象（第二次作业case8、第三次作业case7之类）。
三、分析代码
代码架构严格按照课程组推荐所写。从第一次到第三次迭代主要根据作业需求完成。其中实现了替换低效容器、从暴力遍历（O (n²)）升级为高效图算法排序算法、加入缓存、预计算、索引优化等......
对于“性能瓶颈”，可以通过观察各个方法在实现大规模输入情景下所用的时间、空间规格就能判断其性能。
四、大模型使用
这次作业由于较容易使用大模型完成，在大模型辅助下进了3次a房，以下是我的使用心得：
1、现有高级大模型在我国使用性能较为低下，故一般一次提示词无法完成所有题目要求。尤其是要求严谨的junit，所以再给提示词必须规范AI对所有属性进行维护，并严格符合题意。‘
2、对于过不了的数据点，拿测评反馈给AI会比直接叫AI自我检查效率更高，即使所有反馈都是一个显示，也给了AI检查方向，不至于让AI陷入自证难题。
3、对于无法一次发完所有提示词和原代码、官方包的AI可以分为多次发，但是切忌漏发少发，不然AI会让你见识到什么叫自创。
五、研讨课感悟
我在同学的JML发现了如下bug：不标pure、使用“==”比较字符串、三目运算符格式错误、未处理异常等。
我认为可以提供几个简单但是全面的例子，比如数组寻找最值，单纯的样例无法在现场写JML提供太多参考。
对于信息差，我认为应该规范自然语言书写的格式，统一按照xxx：xxxx之类书写每类条件，如（前置条件：传入数组不为NULL）。