//@annotation/*@ annotation @*/\result：表示一个非void 类型的方法执行所获得的结果，即方法执行后的返回值\old( expr )：用来表示一个表达式expr在相应方法执行前的取值。\not_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。\forall表达式：全称量词修饰的表达式\exists表达式：存在量词修饰的表达式\sum表达式：返回给定范围内的表达式的和\max表达式：返回给定范围内的表达式的最大值\min表达式：返回给定范围内的表达式的最小值方法规格的核心内容包括三个方面，前置条件、后置条件和副作用约定。
前置条件(pre-condition)：前置条件是对方法输入参数的限制
具体的实现形式为通过requires子句来表示：requires P;
后置条件(post-condition)：后置条件是对方法执行结果的限制
具体的实现形式为通过ensures子句来表示：ensures P;
副作用范围限定(side-effects)：副作用指方法在执行过程中对输入对象或this对象进行了修改
具体的实现形式为使用关键词assignable或者modifiable。
pure关键词：设计中会出现某些纯粹访问性的方法，即不会对对象的状态进行任何改变，也不需要提供输入参数，这样的方法无需描述前置条件，也不会有任何副作用，且执行一定会正常结束。对于这类方法，可以使用简单的（轻量级）方式来描述其规格，即使用pure关键词。
异常处理规格：在JML中，
public normal_behavior
表示接下来的部分对方法的正常功能给出规格。与正常功能相对应的是异常功能，即
public exceptional_behavior
signals：signals子句的结构为signals (Exception e) b_expr;，意思是当b_expr为true时，方法会抛出括号中给出的相应异常e。基本上只是简单实现了课程组给出的接口，没有做太大扩展。下面给出三次作业的类图。
第一次作业：
第二次作业：
第三次作业：
唯一在结构上的拓展是在第三次作业使用了并查集的数据结构，对其单独进行了封装。
第一次在强测和互测中都没有找到bug。
第二次作业是历次作业最惨，但最后发现的bug都是没有判断除数是否为0以及忘记乘2等低级错误。主要是由于那一周太忙，几乎没有进行单元测试。充分说明了单元测试的重要性，尽量在每写完一段代码后都要进行单元测试，甚至在写代码之前就要写好单元测试的代码。
第三次作业还是有不少的bug，但是由于这周一直在忙别的事情，还没来得及去查看，非常抱歉。
这一单元主要是进行规格的学习，规格可能是进行团队协作时很重要的东西，但受限于编程经验，对规格在实际项目中的具体作用体会还是不够。但这一单元让我最大的收获就是意识到了单元测试以及利用框架进行自动化测试的重要性。说实话这一单元比前两单元简单的多，但我却犯了比之前多得多的bug。一是投入的精力确实减少了，二是单元测试的力度还是不够。这对我之后写代码提供了很大的启示。
原文：https://www.cnblogs.com/maxu/p/12943009.html