OO第三次博客作业——规格

(1)梳理JML语言的理论基础、应用工具链情况

概述：JML语言是一种为Java程序设计的规格语言，遵循契约式设计规则。

编译：规格是用Java注释的方式编写的，因此可以被任意Java编译器编译。

思想：JML继承了Eiffel，Larch和Refinement Calculus的思想，其目标是在保持可读性的同时，提供严格的形式语义。

作用：JML提供语义来严格描述Java模块的行为，防止模块设计者的设计错误。JML使用各种验证工具，例如运行时断言检查器和扩展静态检查器（ESC / Java），可帮助程序员进行开发。

语法：（略）需要注意的是，JML语言为了和代码本体区别开来，其语法和Java有较大不同。

工具链：基于JML的工具较为完善。Iowa State JML tools提供了断言检查编译器jmlc；jmldoc可以生成含有额外JML信息的Javadoc；jmlunit根据JML生成单元测试。此外还有ESC/Java2（拓展的静态检查工具）、OpenJML（ESC/Java2的继承者）等等。

 

(2)【改为选做，能较为完善地完成的将酌情加分】部署SMT Solver，至少选择3个主要方法来尝试进行验证，报告结果，有可能要补充JML规格

(3)部署JMLUnitNG / JMLUnit，针对Graph接口的实现自动生成测试用例（简单方法即可，如果依然存在困难的话尽力而为即可，具体见更新通告帖）， 并结合规格对生成的测试用例和数据进行简要分析

首先手写一个Test.java用于测试：

package test;

public class Test {

    public Test() {

    }

    //@ public normal_behavior
    //@ requires (((long)i + (long)j) <= Integer.MAX_VALUE && (long)i + (long)j >= Integer.MIN_VALUE);
    //@ ensures 
esult == (i + j);
    //@ public exceptional_behavior
    //@ requires !(((long)i + (long)j) <= Integer.MAX_VALUE && (long)i + (long)j >= Integer.MIN_VALUE);
    //@ signals (IllegalArgumentException e) true;
    public int sum(int i, int j) throws RuntimeException {
        if ((long)i + (long)j <= Integer.MAX_VALUE
                && (long)i + (long)j >= Integer.MIN_VALUE) {
            return i + j;
        }
        throw new IllegalArgumentException();
    }

    public static void main(String[] args) {
        
    }
}

初始文件结构:

├── test

│├── Test.java

Step 1.

 java -jar jmlunitng.jar test/Test.java

Step 2.

 javac -cp jmlunitng.jar test/*.java

Step 3.

 java -jar openjml.jar -rac test/Test.java

Step Final.

 java -cp jmlunitng.jar test.Test_JML_Test

Execution Result:

[TestNG] Running:
  Command line suite

Failed: racEnabled()
Passed: constructor Test()
Passed: static main(null)
Passed: static main({})
Passed: <<test.Test@6c629d6e>>.sum(-2147483648, -2147483648)
Passed: <<test.Test@5ecddf8f>>.sum(0, -2147483648)
Passed: <<test.Test@3f102e87>>.sum(2147483647, -2147483648)
Passed: <<test.Test@6fdb1f78>>.sum(-2147483648, 0)
Passed: <<test.Test@51016012>>.sum(0, 0)
Passed: <<test.Test@29444d75>>.sum(2147483647, 0)
Passed: <<test.Test@2280cdac>>.sum(-2147483648, 2147483647)
Passed: <<test.Test@1517365b>>.sum(0, 2147483647)
Passed: <<test.Test@4fccd51b>>.sum(2147483647, 2147483647)

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

PS：racEnabled Failed的问题暂未找到方法解决:(。

在自动生成的测试中，对多种特殊情况都进行了测试。0、-2147483648、2147483647三个值互相加减，来测试是否符合jml要求。可见，jml不仅用于辅助设计，还可用于验证代码正确性。

(4)按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构

首先生成类图：

 

两根蓝线清晰表明：三次作业，MyGraph继承MyPathContainer，MyRailSystem继承MyGraph。这样基于上次作业的正确性，避免机械的copy，最大限度保持程序的可维护性，呈现出清晰的数据结构。对于特殊的数据，建立独立类，单独维护。当然，继承不等于纯继承。为了添加新的功能，有必要维护旧的架构。例如：第二次作业MyGraph类需要实现求最小路径等。如何在继承的前提下实现新功能呢？我的解决方案是在MyPathContainer类的 addPath 方法中添加新的 addInGraph 方法，并在MyPathContainer中声明此方法，其内容为空。

    public void addInGraph(Path p) {

    }

在MyGraph中对方法进行重载。

    public void addInGraph(Path p) {
        for (int i = 0; i < p.size() - 1; i++) {
            int a = p.getNode(i);
            int b = p.getNode(i + 1);
            mirrorAdd(a);
            mirrorAdd(b);
            a = getMirrorId(a);
            b = getMirrorId(b);
            edgeMat[Math.min(a, b)][Math.max(a, b)]++;
        }
        linJieMat = genWholeLinJie();
        minDisMat = floyd(genWholeLinJie());
        addInSystem(p);
    }

　　

(5)按照作业分析代码实现的bug和修复情况

在三次强测与互测中无bug。

(6)阐述对规格撰写和理解上的心得体会

规格在团队协作和大型项目管理中，的确可以发挥非常重要的作用。基于“契约式编程”的思想，coders可以有一个清晰的架构理解，在编写代码时不会出现违反jml的bug。然而，美中不足的是，jml的编写是困难且耗时的。在工业化实用性上进行考虑，是否应该花费大量的时间编写jml然后再实现方法内容仍旧存疑。