OO第三次作业总结

一、JML

（一）JML语言理论基础

（1）JML表达式：

  JML表达式包括以下几种：

  原子表达式如\result（方法执行后的返回值）、\old（表达式在相应方法执行前的取值）；

  量化表达式如\forall（表示每个元素都满足相应的约束）、\exists（表示存在一个元素满足相应的约束）；

  集合表达式；

  操作符如推理操作符==>（表示充分条件）和价关系操作符<==>（充分必要条件）。

（2）方法规格

  前置条件：用require语句表示，表示方法执行所必须满足的条件。

  后置条件：用ensures语句表示; 表示方法执行后所必须满足的条件。

  副作用范围限定：用assignable表示可赋值的变量，用modifiable表示可修改的变量

  方法的异常行为：normal_behavior, also, exceptional_behavior

（3）类型规格

  不变式invariant，要求在所有可见状态下都必须满足的特性。

  状态变化约束constraint，来对前序可见状态和当前可见状态的关系进行约束。

（二）JML应用工具链

工具链主要包括以下几种

JMLUnitNG：可以自动生成测试数据来检验代码的正确性。

SMT Solver：用于验证代码和规格的等价性。

OpenJml：检查JML的规范性。

二、JMLUnitNG

 

public class Test {

    /*@ public normal_behavior

     @ requires c >= 0 && d >= 0;

     @ ensures \result == c + d;

     @*/

    public static int sum(int c, int d) {

        return c + d;

    }

}

在执行过程中，会发现这个写法会有溢出的错误。

三、架构设计

（一）第一次作业

在第一次作业的时候我就按照JML所写，一个一个的完成它所要求的方法。值得注意的一点是，对于删除指令和增添指令来说，由于他们所占的比例不大，因此，最好将复杂度高的算法放在这些方法里，可以节约时间，比如算不同节点数目这个方法。甚至也没有考虑数据结构，时间这些事情。导致的结果就是，我并没有用HashMap完成PathContainer中Path的存储，而是用ArrayList。这样即使我已经提前把getDistinctNode算出，但依然复杂度很高。而且这样做也容易出错，有一个方法中，我对Pathid返回出错。这样的结果就是我并没有进入互测。

作业完成之后，我对我的程序中数据结构重新写了一遍，将PathContainer中Path的存储改成HashMap，并且由id和path双索引的HashMap，顺利修复了强侧中的bug。

（二）第二次作业

第二次作业中把所有的path构成了一张无向图，这样就新添了对边，两个点是否连通，两个点之间的最短路径的问题。相较于第一次作业而言，首先，我要构造出一张图，然后才能根据这张图来进行一些操作。我对图的存储是这样的：我是用的两层HashMap来存储，存的值呢为边的数量，这么做的原因是因为可能有多条路包含同一条边，因此，在删除路径的时候，就能确定这条边到底删不删除。

我这次作业也出了很大的问题。其实我在时间截止之前就已经发现了，但我没有来的级改。我用的是floyd算法，但在大强度下，时间特别慢。我推测的原因是我对于存储最短路径的HashMap有问题，由于HashCode设计的不好，导致效率十分的低。因此在强侧中只的了65分。在之后的bug修复中，我重新更改了数据结构，用了两层HashMap来存储最短路算法，并且把算法换成了spfa算法，顺利的修复了bug。

我自己设计的GraphAm类，这个类我主要是用来完成与图有关的一些操作。这次设计的不是很好，里面只有一个spfa算法。但在第三次作业中，我将其完善了许多。

这次没有找到别人的bug

（三）第三次作业

 

这次作业中对图这个数据结构进行了进一步的升级，变成了一个地铁结构。跟图数据结构相比，地铁数据结构当然多了换乘，票价。当然助教还编了一个满意度。其实本质这三个是一样的，都是同一个解决办法。当开始拿到这个题时，我是没有任何思路的。但是多亏了大佬提供了拆点的思路后，我变豁然开朗。就拿计算两个点最少换成次数来举例，我们刚开始的思路还是想用与最短路相关的算法来解决问题，但是如何转化成这种问题呢？由于换乘是不同路径上的相同点的转移。因此我们不妨在这些点直接加一条边，经过这些边一次就代表换乘一次，即这些边的权重为1。这样就转化为了最短路径问题。

对于架构而言，我将所有对图的修改，计算的部分全部放入了GraphAm里面，这样在容器中只需调用里面的方法即可。

这次也犯了一个低级错误，在Integer对象比较时，没有用equal。（其实我不明白为什么前两次没有这个问题），改完就修复了这个bug

这次我重点测试了同room中新增的对于换乘，票价，满意度的测试，找到了大量的bug。

四、心得与体会

这一次大的主题让我们对JML规格有了一定的了解。同时也对数据结构有了深刻的认识。

JML在整体思路设计的时候能发挥很好的作用。特别是一份写得很清晰的JML，可以很很轻松的翻译成成行的代码，他没有二义性。

可能在工业界，尤其是那些不容许任何程序错误的场景下（如航空航天、军事领域），使用JML是一种较好的易于沟通和协作的编程方式，且能在最大程度上避免错误的产生。但在小团队的常规开发中，自然语言会是相对更好的选择。

总之我还是学到了许多的。