OO第三次博客作业——第三单元总结

JML语言理论基础

JML理论基础

Java建模语言是一种进行详细设计的符号语言，JML能够帮助我们进行代码的规范性设计和规格化设计，借助JML的符号可以清晰准确地表示出方法的功能和规格。通过JML及其支持工具，不仅可以基于规格自动构造测试用例，并整合了SMT Solver等工具以静态方式来检查代码实现对规格的满足情况。

一般而言，JML有两种主要的用法：
（1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。
（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。

方法规格

• 前置条件pre-condition

  一般形式：requires P1||P2;

  前置条件定义了对调用者的要求，规定了方法能够正确处理的输入范围。前置条件必须包含一个可判定的布尔表达式。如果调用者不能满足前置条件，方法就不能保证执行结果满足后置条件。因此，一个方法A在调用另外一个方法B之前需要满足B所要求的前置条件，否则方法B可以不对A输入的数据进行处理。相应的，如果满足了B所要求的前置条件，则B必须对A输入的数据进行正确处理。

• 后置条件post-condition

  一般形式：ensures P1||P2;

  后置条件对方法执行之后必须达到的效果进行描述。后置条件也必须包含一个可判定的布尔表达式。前置条件是一个方法对调用者的要求，后置条件则是对调用者的承诺。如果调用者满足了被调用者的前置条件，被调用者的执行就必须满足所承诺的后置条件，否则视为被调用者执行有错误。

• 副作用side-effects

  副作用（side-effects）指方法在执行过程中不可避免要修改this对象的属性数据或传递进来的对象。这些修改会改变相应对象的状态，一旦修改有误，会给相应对象后续方法的执行带来不可预料的错误。因此，方法规格应明确执行过程会对哪些数据进行修改，同时方法的实现体只能对所声明的变量属性进行修改。作为规格的组成部分，描述副作用不是简单记录实际执行修改了哪些数据，而是在实现之前，从设计角度就规定要修改哪些数据。JML语法通过在方法的行为规范中使用assignable语句来对方法的副作用加以描述，只有在该语句中列出的变量才能在一个方法的实现中修改。

• 异常抛出

  为了获得一个全局适用的过程，就需要定义异常输入情况下的规格。JML通过normal_behavior和exceptional_behavior来区分正常功能和异常功能对应的规格。其中在normal_behavior情况下，可以定义方法的前置条件、副作用和后置条件；而在exceptional_behavior情况下，可以定义方法的前置条件、副作用和异常抛出，但不能定义方法的后置条件。JML语言提供了signals和signals_only来定义异常抛出行为规格：

  signals (abcException e) P：表示当前P满足时，抛出类型为abcException的异常e

  signals_only abcException：表示无条件抛出异常，类型为abcException。

常用JML特性

• othing, everything：当前作用域下的变量范围
• sum, max, min：对给定范围的表达式进行运算。分别表示加和、最大值、最小值。
• esult：方法的返回值。
• exists、forall：分别表示存在后续表达式代表的情况、满足后续表达式的任意值都成立。
• old：表示在方法执行前的值。

JML工具链

JML可以利用JMLUnitNG 生成 TestNG 测试样例，也可以利用OpenJML进行规格正确性检查。

1. OpenJML

   OpenJML可以对JML注释的完整性进行检测。OpenJML的功能十分丰富，具有类型检查、变量可见性检查等功能。

   命令行下主要有以下三种使用途径：运行时检查、JML语法静态检查、程序代码静态检查。（此处将openjml.jar放在了代码同一路径下，在真实使用环境下应该将下面的相对路径换为绝对路径）

   • 运行时检查：在运行和单元测试时会发挥作用。

     java -jar openjml.jar -rac test.java

   • JML语法静态检查：仅检查JML是否具有语法错误。

     java -jar openjml.jar -check test.java

   • 程序代码静态检查：仅检查代码是否有错误。

     java -jar openjml.jar -esc test.java

   网页版OpenJML也可以很方便的进行静态检查：

   https://rise4fun.com/OpenJMLESC

   

2. JMLUnitNG

   JMLUnitNG可以根据规格的实现自动生成TestNG测试样例。可以用来进行自动化测试，十分方便。

   以下为使用方法：（此处将jmluniting.jar放在了代码同一路径下，在真实使用环境下应该将下面的相对路径换为绝对路径）

   • 基于JML生成测试文件：

     java -jar jmlunitng.jar test.java

   • 使用OpenJML进行运行时检查

     java -jar openjml.jar -rac test.java

   • 使用TestNG针对性测试

     java -cp jmlunitng.jar:bin test_JML_Test

部署JMLUnitNG,自动生成测试样例

参考上一部分JML工具链中JMLUnitNG部分，部署JMLUnitNG并自动生成测试样例可分为以下步骤：

1. 基于JML生成测试文件：

   java -jar jmlunitng.jar test.java

2. 使用OpenJML进行运行时检查

   java -jar openjml.jar -rac test.java

3. 使用TestNG针对性测试

   java -cp jmlunitng.jar test.Test_JML_Test

最后即可得到运行结果,

文件树如下：

最终自动测试结果如下：

三次作业架构设计与迭代

综述

在这三次作业中，MyRailSystem - MyGraph - MyPathContainer这三个类存在明显的继承层级关系。利用继承的方法可以很大程度上减少代码量，并使得代码结构层次更加清晰、整洁。
在继承关系中进行迭代，有利于根据不同的需求进行针对性的优化，既可以在一定程度上降低思维难度，防止出错，又可以在一步步优化的过程中让这几个类更加鲁棒。

第一次作业PathContainer

这次作业主要包括Path类和PathContainer类的构建。主要需要考虑的问题是避免超时，设计中涉及到的算法难度不大，合理使用了HashMap、ArrayList等容器就可以完成本次作业。

HashMap查找和插入的时间复杂度都是O(1)，可以防止超时，所以利用HashMap实现索引功能。

ArrayList可以实现path中节点的存储。

由于本次作业中需要利用id索引path，也需要利用path索引id，又考虑到PathContainer中path的id与路径一一对应的特点，所以我将两个HashMap合并封装为了一个新的容器DuplexMap类，可以使用泛型，具有HashMap常用的一系列增删改查的功能。封装之后显得简洁、方便。

具体代码如下：

import javafx.util.Pair;
import java.util.HashMap;
import java.util.Set;

public class DuplexMap<K, V> {
    private HashMap<K, Pair<K, V>> kmap = new HashMap<>();
    private HashMap<V, Pair<K, V>> vmap = new HashMap<>();

    public boolean containsKey(K k) {
        return kmap.containsKey(k);
    }

    public boolean containsValue(V v) {
        return vmap.containsKey(v);
    }

    public V getByKey(K k) {
        Pair<K, V> e = kmap.get(k);
        if (e == null) {
            return null;
        }
        return e.getValue();
    }

    public K getbyValue(V v) {
        Pair<K, V> e = vmap.get(v);
        if (e == null) {
            return null;
        }
        return e.getKey();
    }

    public boolean put(K k, V v) {
        if (k == null || v == null) {
            return false;
        }
        Pair<K, V> e = new Pair<>(k, v);
        if (containsKey(k)) {
            removeByKey(k);
        }
        if (containsValue(v)) {
            removeByValue(v);
        }
        kmap.put(k, e);
        vmap.put(v, e);
        return true;
    }

    public V removeByKey(K k) {
        Pair<K, V> e = kmap.remove(k);
        if (e == null) {
            return null;
        }
        vmap.remove(e.getValue());
        return e.getValue();
    }

    public K removeByValue(V v) {
        Pair<K, V> e = vmap.remove(v);
        if (e == null) {
            return null;
        }
        kmap.remove(e.getKey());
        return e.getKey();
    }

    public int size() {
        return kmap.size();
    }

    public Set<K> keySet() {
        return kmap.keySet();
    }
}

第二次作业Graph

这一次作业沿用上一次作业的Path类。

另外还由PathContainer变为Graph类，最大的变化在于需要判断是否连通以及求最短路径。

由于边的权重全部为1，所以可以使用BFS遍历。

在遍历的过程在，还需要将中间结果在HashMap中存储下来，便于下一次查询时节约CPU的开销。

而本次作业改变图的指令很少，所以在添加和删除path时更新Graph并且清空缓存的中间结果后再在下次查询时重新计算即可。

第三次作业RailwayStation

个人感觉这次作业难度有点大，慢慢摸索，研究了讨论区中大佬的发言之后，明白了该如何解决作业中遇到的问题。

查询连通块个数可以利用BFS染色法解决，在遍历时每遇到一个没有经过的点的时候就将连通块的计数变量加1，因为每个没有经过的点都属于一个新的连通块。

最低票价、最短换乘、最少不满意度都是最短路的变体，但是需要考虑权重，所以使用dijkstra算法。

为了避免超时，我使用优先队列优化后的dijkstra算法。

涉及换乘的问题，我采用拆点的方法，将不同路径中id相同的点视为不同点，另外按照讨论区中的方法把不同路径中的相同点与起点终点连接起来，减少整个图中点的数目。

Bug分析与修复

bug：

第一次作业中犯了一个愚蠢的错误，comparePath函数没有使用Integer.compare()而是直接相减，导致了出错。

修复：

将相减换为Integer.compare()即可解决问题。

心得体会

JML规格化设计

JML规格的设计之间从未接触过，经过这几次作业的洗礼，我对于规格化设计有了初步的了解。

如果说类规格定义了与用户的契约，那么规格也定义了开发人员必须遵从的规约。

这种契约式的设计对于代码风格和代码正确性有极大裨益，JML利用简洁的规格语言将代码的架构描述了出来，将每一个函数的功能实现的十分透彻，更加清晰，没有二义性。

容器的使用

这几次作业使用了大量容器，我自己也搭建了一些容器。在整个代码架构中，容器帮助我讲各种数据有机的组织了起来，给了我很大的帮助。

合理利用这些容器可以极大的提升我们代码的质量和性能。在今后我也想对容器有更加深入的了解，从而将容器的威力真正发挥出来。