面向对象第三单元总结

一、JML语言的理论基础和应用工具链

　　理论基础

　　JML是一种进行详细设计的符号语言，他鼓励你用一种全新的方式来看待Java的类和方法。

　　JML综合了Eiffel，Larch两者的优点，为Java提供了一个专门设计行为的接口语言。JML用来描述方法模块的动作行为，基于数学模型，其比自然语言更加精确。

　　JML编译器jmlc可以检查JML形式规范是否正确；JMLdoc与Javadoc工具相似，不同的是它在生成的HTML格式文档中包含JML规范；JMLunit可以成生一个Java类文件测试的框架，它可以让你很方便地使用JUnit工具测试含有JML标记的Java代码。

　　应用工具链

　　VSCode里面有JML高亮插件，这可以使我们更好的阅读JML语言。

　　OpenJML用于检查JML语法问题，是否如何规格。

　　JMLUnitNG主要是根据JML规格描述产生NG样例。

二、部署JMLUnitNG，自动生成测试样例

　　首先我们沿用讨论区的Demo.java作为入门例子来使用jmlunitng

　　Demo.java的具体内容为

public class Demo {
    /*@ public normal_behaviour
      @ ensures 
esult == lhs - rhs;
    */
    public static long compare(int lhs, int rhs) {
        return lhs - rhs;
    }

    public static void main(String[] args) {
        compare(114514,1919810);
    }
}

　　①建立jmlunitng的bash脚本

　　vim jmlunitng其具体内容为

#!/bin/bash
　　java –jar jmlunitng.jar “$@”

　　②建立openjml的bash脚本

　　vim openjml其具体内容为

#!/bin/bash
　　java –jar openjml.jar “$@”

　　③生成的test文件

　　. jmlunitng Demo.java

　　新增的文件为JMLUnitNG生成的测试文件

　　④将所有的.java文件编译出.class文件

　　Javac –cp jmlunitng.jar *.java

　　⑤用 openjml 自带的 jmlc编译自己的文件

　　. openjml –rac Demo.java

　　⑥开始测试

　　Java –cp jmlunitng.jar Demo_JML_Test

　　发现有三处地方出现了错误，打开代码发现该方法在比较大小时使用的减法，造成了减法的溢出，我们将int换乘long试试

public class Demo {
    /*@ public normal_behaviour
      @ ensures 
esult == lhs - rhs;
    */
    public static long compare(int lhs, int rhs) {
        return (long)lhs - (long)rhs;
    }

    public static void main(String[] args) {
        compare(114514,1919810);
    }
}

　　重复上述过程

　　发现已经全部通过

　　下面用path来尝试一下

　　发现constructor和getNode挂了，因为它的测试数据不符合requires的要求。。。

三、架构设计

　　这一系列的作业应该是这学期一个单元中重构最少的一次作业，几乎每次都能完美沿用之前的代码。第二次作业中有人说BFS块，但是BFS只能用于无项无权图，所以我还是果断选择了Dijkstra算法，在第三次作业中等于说算法是现成的，只用重新构造不同的邻接表即可。

　　第一次作业——pathContainer

　　这次作业比较简单，但是我还是经历了一次重构，最开始没有考虑到时间复杂度的问题，全部使用arrayList容器导致时间复杂度特别高。这也给我自己一个提醒，在后面的作业中格外注重时间复杂度的控制。

　　第二次作业——graph

　　这次作业加入了最短路径的查询，我没有像第一次那样在每次add和remove之后直接计算出所有需要查询的东西，而是在每次查最短路径时才进行查询，并将查询结果保存在cache中，每次在add和remove中清除cache。 

　　第三次作业——railwaySystem

　　第三次作业沿用第二次的策略，加到4个cache，采取重构图的方法，具体方法在另一篇博客中指出。

四、Bug分析

　　三次作业公测互测都没有出现bug，在自己测试的时候，对于dijkstra算法的查bug采用单步调试加断点的策略，将很多自己写的类重写了toString方法，方便在debug时使用。主要出错是在remove的时候总会出现空指针异常，因为add之后一些信息没有保存导致remove时因缺少信而出现空指针异常。

五、心得体会

　　学习规格这一块最大的感受就是，感觉通过规格来写代码时比较容易，而且出错的可能比较低，但是撰写规格的时候就比较困难，这个困难来自两方面，一方面是对jml语言还不够熟悉，另一方面是对架构的设计赫尔理解不够到位，我想这就是从码农到架构师的蜕变过程吧。有好的规格不一定能写出好的代码，但没有好的规格一定写不出好的代码，所以对规格的学习是十分重要而且必不可少的。

　　还有就是因为这次作业涉及到很多数据结构的知识，在复习数据结构课程的同时，我学会使用了很多容器，arrayList、hashMap、hashSet、priorityQueue等等，这些容器使我们的程序得到了最大程度的优化，即使在第三次作业中，我最大的cpu时间也没有超过20秒的。还有程序中看似有很多冗余的数据结构，但是正是因为这些数据结构的存在提高了程序的性能。