BUAA_OO 第三单元JML规格编程总结

本单元主要以图算法问题锻炼同窗们按照规格编程的能力，主要考察点在于同窗们对于单元测试的使用和对于JML规则的理解。另外实际编程中存在的难点为对于图算法时间复杂度的分析。本次做业我写的是至关的惨烈。第一次第三次都在测试环节被发现bug，并且错的都十分低级，只有第二次做业写的较顺利没有被查出bug。下面我将对本单元进行分析。

 

1、JML知识梳理

1.1 JML语言理论基础

JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言 ，基于Larch方法构建。BISL提供了对方法和类型的规格定义 手段。所谓接口即一个方法或类型外部可见的内容。JML主要基于Larch上的工做，并融入了计算机科学家关于Design by Contract的研究成果。JML为严格的程序设计提供 了一套行之有效的方法。经过JML及其支持工具，不只能够基于规格自动构造测试用例，并整合了SMT Solver等工具以静态方式来检查代码实现对规格的知足状况。

通常而言，JML有两种主要的用法： （1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的天然语言描述，而是逻辑严格的规格。

（2）针对已有的代码实现，书写其对应的规格，从而提升代码的可维护性。这在遗留代码的维护方面具备特别重要的意义。

 

JML主要语法以下:

（1）原子表达式 ：

\result表达式：表示一个非 void 类型的方法执行所得到的结果，即方法执行后的返回值

\old( expr )表达式：用来表示一个表达式 expr 在相应方法执行前的取值

\not_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程当中被赋值。若是没有被赋值，返回为 true ，不然返回 false 

\not_modified(x,y,...)表达式：该表达式限制括号中的变量在方法执行期间的取值未发生变化

\nonnullelements( container )表达式：表示 container 对象中存储的对象不会有 null

\type(type)表达式：返回类型type对应的类型(Class)

\typeof(expr)表达式：该表达式返回expr对应的准确类型

（2）量化表达式

\forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每一个元素都知足相应的约束

\exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素知足相应的约束

\sum表达式：返回给定范围内的表达式的和

\product表达式：返回给定范围内的表达式的连乘结果

\max表达式：返回给定范围内的表达式的最大值

\min表达式：返回给定范围内的表达式的最小值

\num_of表达式：返回指定变量中知足相应条件的取值个数

（3）操做符

JML表达式中能够正常使用Java语言所定义的操做符，包括算术操做符、逻辑预算操做符等。此外，JML专门又定义 了以下四类操做符。

子类型关系操做符：E1<:E2，若是类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，不然为假

等价关系操做符：b_expr1<==>b_expr2 或者 b_expr1<=!=>b_expr2，b_expr1和b_expr2都是布尔表达 式，这两个表达式的意思是 b_expr1==b_expr2 或者 b_expr1!=b_expr2

推理操做符： b_expr1==>b_expr2 或者 b_expr2<==b_expr1 对于表达式 b_expr1==>b_expr2 而言，当 b_expr1==false ，或者 b_expr1==true 且 b_expr2==true 时，整个表达式的值为 true 。

 变量引用操做符：。\nothing指示一个空集；\everything指示一个全集，即包括当前做用域下可以访问到的全部变 量

（4）方法规格

方法规格的核心内容包括三个方面，前置条件、后置条件和反作用约定。

前置条件经过requires子句来表示： requires P;。其中requires是JML关键词，表达的意思是“要求调用者确保P为 真”。

后置条件经过ensures子句来表示： ensures P;。其中ensures是JML关键词，表达的意思是“方法实现者确保方法执 行返回结果必定知足谓词P的要求，即确保P为真”。

反作用约定用关键词 assignable 或者 modifiable表示 ：反作用指方法在执行过程当中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行带来影响。

对于设计中不会对对象状态改变，于是不会产生反作用；无需提供输入参数，于是无需描述前置条件的方法，称为纯访问方法，使用pure关键词标记。

（5）行为规格

normal_behavior 关键字代表这些规范是针对方法不抛出任何异常时的状况。

public exceptional_behavior 注释能够用来描述抛出异常时的行为。

案例：

/*@ normal_behavior @ requires (\exists Path path; path.isValid() && containsPath(path); path.containsNode(fromNodeId)) && @ (\exists Path path; path.isValid() && containsPath(path); path.containsNode(toNodeId)); @ assignable \nothing; @ ensures (fromNodeId != toNodeId) ==> \result == (\exists int[] npath; npath.length >= 2 && npath[0] == fromNodeId && npath[npath.length - 1] == toNodeId; @ (\forall int i; 0 <= i && (i < npath.length - 1); containsEdge(npath[i], npath[i + 1]))); @ ensures (fromNodeId == toNodeId) ==> \result == true; @ also @ exceptional_behavior @ signals (NodeIdNotFoundException e) (\forall Path path; containsPath(path); !path.containsNode(fromNodeId)); @ signals (NodeIdNotFoundException e) (\forall Path path; containsPath(path); !path.containsNode(toNodeId)); @*/

 

（6）类型规格

类型规格指针对Java程序中定义的数据类型所设计的限制规则，经常使用的是不变式限制和约束限制 。不管哪种，类型规格都是针对类型中定义的数据成员所定义的限制规则，一旦违反限制规则，就称 相应的状态有错。

不变式（invariant P )：invariant 为关键词，P为谓词。要求在全部可见状态下都必须知足的特性。其中，可见状态是指，修改为员变量的方法执行以外的状态。

状态变化约束（constraint)：对对象的状态在变化进行约束的不变式。对前序可见状态和当前可见状态的关系进行约束。

 

1.2 JML应用工具链

OpenJML：能够对代码进行JML规格的语法的静态检查，还支持使用SMT Solver动态地检查代码对JML规格知足的状况，所以OpenJML通常也自带有其支持的JML solver。

JML UnitNG：根据JML描述自动生成与之符合的测试样例，重点会检测边界条件。

总的来讲，经过这些工具能够确保咱们规格实现的正确性，由此肯定咱们过程性的模块的正确性，进而使咱们对象设计拥有稳定安全的基础。

 

 

2、SMT测试

尝试着配置了一下可是一直报错...

 

 

3、JML测试

 

利用讨论区大佬的方法使用testMe检查了MyPath类中compareto方法，检查比较是否依照字典序进行，并重点检查了int型极端比较状况，防止出现溢出致使判断错误的问题。另外检查了equals方法，看是否能成功实现路径是否相等的判断。

使用过程当中我着实感觉到了单元测试的便利性。以往为了检查一个嵌套在深层的函数经常须要绞尽脑汁的设计样例并思索怎样才能成功调用到该函数。另外为了看具体结果经常须要加入大量的print语句，人工审阅判断。而使用单元测试以后无需费力构造，只需针对要检测的函数进行测试就好，另外现象也极易看出对不对，真的是十分便捷。

 

 

4、做业架构梳理

此次做业架构自己我写的仍是不错的，基本上每次做业都不用对以前已经有过的函数进行什么更新，只须要额外考虑新增长的函数就能够。助教说这是由于咱们架构能力增长的缘由，但我以为咱们每次基本都不用大改以前代码的核心缘由仍是这几回做业自己层次感比较强，层层推动，每次都为下一次作铺垫。

4.1 第一次做业

 第一次做业较为简单，循序渐进写好了，架构和算法方面没有任何值得强调的部分。

 

4.2 第二次做业

 第二次比起第一次做业增长了部分难度，开始涉及图算法问题，但图算法只在两个函数中涉及，所以函数自己不须要像第三次做业那样封装（第三次做业同一个算法出现了4次），只要在须要时直接使用就好。

 

 

 

4.3 第三次做业

 第三次做业不管是算法复杂度仍是架构复杂度都增长了许多。第一次做业我只有三个类，第二次做业四个类，第三次做业是6个类，同时总代码量也增长了许多。此次做业最难的三个方法——求最低票价，求最少换乘，求最低不满意度实际上均可以用迪杰斯特拉算法实现。所以我这三个函数都是用bfs+优先队列实现迪杰斯特拉算法。

下面是我此次的架构设计：

 

 

 

5、代码实现bug与修复

惨烈，太惨烈了。这个单元明明感受写的都挺顺的，结果由于许多小错（好吧，代码只要错了就是大错，不存在大小错一说，不过从观感上来讲确实感受是小bug）致使分数惨不忍睹，好在终归从这个惨痛的教训中学到了一些。下面我将具体说明我每次做业具体犯的错及修改方法。

5.1 第一次做业

本次做业compare方法中我不是直接比较大小而是对两个数做差比较，这种比较方式在int边缘时会发生溢出，致使结果错误，而后直接错8个点60了，最后修改了两行就改完了。那么本次做业我或者不少人为何会作出如此愚蠢的抉择呢？不用更直观的大小比较而是选择作差比较？我认为咱们都是受到了string类源码中compare的误导所致。

字典序比较在string源码中有包含，源码compareto实现以下：

public int compareTo(String anotherString) { int len1 = value.length; int len2 = anotherString.value.length; int lim = Math.min(len1, len2); char v1[] = value; char v2[] = anotherString.value; int k = 0; while (k < lim) { char c1 = v1[k]; char c2 = v2[k]; if (c1 != c2) { return c1 - c2; } k++; } return len1 - len2; }

以上摘自源码。我看源码后感受这种设计更规范就直接采用了这种设计，却忽略了String类与Int类不同，string以char为单位，每一个char换算成int范围在0-128之间，不存在越界状况。Int类型却可能出现越界的状况。这也提示了我不能迷信源码，在参考源码或别人代码的时候必定要具体状况具体分析，不少时候两个状况尽管十分相近但仍不能直接化用而须要修正。

 

5.2 第二次做业

本次做业程序没有被查出任何bug，从总体反馈来看此次做业虽然设计存在难度，但设计出来后你们基本都没什么错，所以不进行过多讨论。

 

5.3 第三次做业

本次做业设计和算法都没毛病，可是由于一个笔误，最后做业连错6个点，直接70分。即我在迪杰斯特拉算法运行时添加了一个visit数组判断该点是否出现过以免重复通过一样的点，以增长效率。该visit数组设计为HashSet<Node>类型，应该判断我本身设计的Node类，但我运行时却使用了另外一个Integer类型变量，致使判断条件任何状况都为错，判断失效，程序会不断通过已经访问过的点。最后改了把判断条件给改了一行就修复完毕了。

具体错误状况以下：

画蓝线上面那里我原本想写的是Node类型的x，结果笔误写成Integer类型begin了。

表面上看这只是个小错，但却反映出个人不少很差的编程习惯。这个问题十分低级，其实只要我在写完后再通读一遍代码就能解决，但遗憾的是我并无这样作，而是在debug阶段盯着判断出错的代码块改，以后也没再复查。

其实原本这种类型不符合是会有提示的（上面代码块begin部分缺失被标黄了），但我设计的时候有问题，最少换乘，最少票价，最低不满意度三个函数彻底能够经过调用同一个函数并向里面传递不一样的参数来处理，但我却直接将函数在代码块里面实现，大量部分被黄线标记，致使我忽略了begin上面的判断。这是设计上的大失误，这也提示我之后必定要尽可能在设计过程当中进行缜密思考，尽可能让本身写的代码知足高内聚，低耦合的设计原则。

 

6、JML规格心得体会

JML的出现仍是十分有必要的。还记得大一上C语言程序设计课时有时咱们会由于题意不清而进行激烈的讨论，最后每每是各自尝试直至一我的过了才能判断出题意到底想表达的是什么。而在使用JML后咱们只需仔细阅读JML描述，即可顺利理解题意，不会再出现题意不清的状况。能够说，JML这种契约式的编程将架构设计与具体实现分离，有助于实现更优秀的架构，同时底层实现也不受约束。

遗憾的是，JML虽然带来了不少帮助，可是JML自己使用并不容易。课上实验时咱们须要本身写JML，那时咱们所描述的不过是最简单的函数（好比说add等），但仍然感受比写代码自己要困难。另外本单元做业由老师和助教共同商议写出的JML也常出如今发布后经同窗反馈进行从新修改的状况，可见JML是真的很差写。另外在尝试使用JML应用工做链的过程我也发现JML的配套工具并非很是容易使用，即便有讨论区前人栽树，咱们仍然不容易乘凉。

虽然JML自己应用体验并非很是好，不过本单元对于JML的介绍确实给我了很大启发。写JML意味着撰写者本人须要对于本身的需求有着充分的理解，在这个过程当中撰写者进一步改进理解思考本身程序的写法，避免出现设计性问题。同时JML严苛的语法也意味着设计者须要通过缜密的思考才能完成，在这个过程当中撰写者本人的逻辑也会获得锻炼变得更严密。我认为这种契约式编程思惟自己是十分值得称道的，这帮助咱们极大程度避免了需求沟通的成本和难度。所以之后也许咱们能够考虑按照讲座课老师介绍的那样尝试使用更多的工具来完成设计描述从而帮助他人理解。