规格化设计——OO第三单元总结

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

1.1 JML语言

? JML（java modeling language）是一种描述代码行为的语言，包括前置条件、副作用等等。JML是一种行为接口规格语言 （Behavior Interface Speci?cation Language，BISL），基于Larch方法构建。

? 通过使用JML，我们可以忽略一个类、一个方法内部的具体实现，专注于描述方法的预期功能，从而把过程性的思考延迟到方法设计中，扩展了面向对象设计的原则。

1.2 应用工具链

• OpenJML：根据JML语言描述对模块的功能实现进行验证，逻辑证明其正确性。
• JMLUnitNG：基于JML规格的自动化单元测试工具。

二、部署JMLUnitNG

public class Sub {
      /*@ public normal_behaviour
        @ requires a > 0 && b > 0;
        @ ensures \result == a - b;
        @*/
      public static int sub(int a, int b) {
          return a - b;
      }

    public static void main(String[] args) {
        sub(1, 1);
    }
}

在修改代码规格描述，使用OpenJML检验无误后可以生成和编译测试代码：

java -jar ../openjml/openjml.jar -check Sub.java > re.txt
java -jar jmlunitng-1_4.jar Sub.java
javac -cp jmlunitng-1_4.jar *.java
java -jar ../openjml/openjml.jar -rac Sub.java
java -cp jmlunitng-1_4.jar sub_JML_Test

之后即可测试代码，部分结果如下：

[TestNG] Running:
    Command line suite

Running:
Command line suite

Passed: racEnabled()
Passed: constructor sub()
Failed: static sub(-5464846548, -5464698148)
Passed: static sub(0, -9632483648)
Passed: static sub(2269875647, -2112489738)
Passed: static sub(-5963483648, 0)
Passed: static sub(0, 0)
Passed: static sub(5967483647, 0)
Passed: static sub(0, 2687483647)
Passed: static main(null)
Passed: static main({})

===============================================
Command line suite
Total tests run: 10, Failures: 1, Skips: 0
===============================================

三、作业架构分析

3.1 容器

? 第一次作业，只需要实现path和pathcontainer两个类。为了减少方法的时间复杂度，我选择了特定的数据结构，同时尽量把出现频率高的方法（查询）复杂度分担到出现较少的方法（增删）中：我实现了path的hashcode方法并使用了两个hashmap存储path和对应的id，保证查询path的复杂度接近o（n）。同时使用一个hashmap存储每个节点及其出现次数，计算node_count时直接返回size，复杂度小。Path中则采用ArrayList存储路径上的全部点。

3.2 扩展-图

? 第二次作业需要在PathContainer的基础上增加连通性判断、最短路径等图相关的方法，等同于要求扩展图的数据结构。
? 我使用了嵌套hashmap存储（节点-（相连的节点-连接次数））来记录图，每次增删路径时修改图。使用floyd算法求解两点最短路径：邻接矩阵original记录点之间的连接关系，每次增删时对应修改original并将新的original复制到二维矩阵routes，在routes中应用弗洛伊德算法可得到点与点之间的最短路径，最短路径不为MAX（代表点之间不连通）即是连通的，可求最短路径。
? 此外，为了将编号各异的点使用邻接矩阵管理起来，利用“同一时刻不超过250个点”这条数据限制，我将点的编号映射到0-249，代表在矩阵中的偏移。我使用了一个hashmap记录映射关系，使用了一个空闲点的堆栈来记录哪些点仍然可以提供映射。。

3.3 扩展-地铁换乘

? 由于低估了第三次作业的难度，这次作业的完成情况较为粗糙，设计和编码非常仓促：采用了同学之间普遍认同的算法计算最少换乘次数和最少票价；为了减少出错的可能，把上次作业中与图相关的部分全部封装到了一个类里。综上所述，并无多少自己深入的思考和独特的设计。

? 第三次作业的要求是扩展求联通块数量的功能和最小带权路径的功能（权值需要自己定义并计算）。

? 求联通块数量可以利用第二次作业中的图结构，采用单元点出发bfs搜索遍历所有到达点+依次将所有未标记节点作为起点的方式实现。

? 为了实现计算最少换乘、最小不满意度和最小票价，需要定义新的权。在设置好权值后，应用第二次作业的floyd算法即可，所以本次作业的关键是扩展新的数据结构存储权值。

? 求最少换乘时，应当把一条path上任意两点之间的边权值设为1；求最小票价时，应该把权值设置为两点之间的最短路径+2；求最小不满意度时则应该把权值设为最小不满意度+32。三种求解最后要相应地减去1, 2, 32以算出正确答案。归纳出三种方法的共性之后可以进行封装归类。

? 考虑到删除路径时对地铁结构影响较大，每次增删线路时，我都会重新扫描所有path建立新的邻接矩阵存储权值。

? 在扫描一条path计算权值时，我用到了spfa算法计算最短带权路径。

四、作业中的bug

? 第二次作业中修改邻接矩阵中自环的时机不对：自环应该在点被去除时消失，而不是在边被去除时消失。

? 第三次作业中，由于在上次作业中映射path中节点时没有判断该节点是否在图中存在，这个问题严重影响了第三次作业的评测：在强测中大量被包含“不存在于图中的节点”的样例攻击，出现大量nullpointer exception。归根结底，是在封装图的时候把规格和自认为冗余的代码删去了，导致出现了大量异常。（以惨痛的教训学习到规格和考虑重构后果的重要性）

五、单元心得体会

? 本单元的学习是一个较为完整的体会规格化设计和设计迭代的过程，虽说到了最后一次作业几乎已经无暇顾及阅读繁复的规格，但还是更深入地体会了继承的思想，学到了很多规格化设计的相关思想。

? 规格化设计一方面可以延迟过程性的思考，专注于描述算法的抽象实现和功能，从而方便了程序设计人员；另一方面，可以做到设计与实现分离，从而被广泛应用于对安全追求较高的大型软件开发中，在保证程序逻辑正确性的前提下分而治之，让不同的人根据规格编写不同的代码，并可以很方便地验证代码的正确性（JML工具链）。

原文地址：https://www.cnblogs.com/why34/p/10907680.html