面向对象第三单元博客作业

2023-10-28 19:35:28

面向对象第三单元博客作业
- JML Language
  - Theory
  - Toolchain
- SMT Solver
  - 部署
  - 最简单的例子
- JMLUnitNG
  - 测试Graph
  - 测试Path
- 架构设计
  - 1
  - 2
  - 3
- bug和修复情况
  - 1
  - 2
  - 3
- 对规格撰写和理解上的心得体会

面向对象第三单元博客作业

针对第三单元的三次作业和课程内容，撰写技术博客

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

• (2)部署SMT Solver，至少选择3个主要方法来尝试进行验证，报告结果

• 有可能要补充JML规格

• (3)部署JMLUnitNG/JMLUnit，针对Graph接口的实现自动生成测试用例，并结合规格对生成的测试用例和数据进行简要分析

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

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

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

JML Language

JML是一种形式化的、面向JAVA的行为接口规格语言。其最重要的特点是契约式设计（Design by contract）

Theory

笔者个人的理解是，JML结合了契约式设计和规格，其理论基础是数理逻辑，可以由形式化推理工具验证正确性。

Toolchain

JML官方主页

http://www.eecs.ucf.edu/~leavens/JML//index.shtml

不幸的是，官方预先编译好的工具jmlc、jmlunit、jmldoc在Java 8无法正常工作。对于Java8，推荐使用openjml。

Users who want to work with Java 1.5, 1.6, 1.7, or later sources should consider using OpenJML first.

OPENJML包含了编译器，SMT Solver，命令行前端等。

另外，OPENJML提供了Eclipse插件，可以直接在IDE使用OPENJML的功能，包括但不仅限于JML规格的语法检查、ESC静态检查、RAC动态检查。

生成测试的工具有jmlunit，JMLUnitNG等。不过经过笔者测试，在使用Java 8的情况下，jmlunit无法正常工作，而JMLUnitNG可以生成测试代码。

SMT Solver

部署

SMT Solver使用Microsoft的Z3 4.3.1

最简单的例子

Student.java

public class Student {
    private /*@ spec_public @*/ String name;
    //@ public invariant credits >= 0;
    private /*@ spec_public @*/ int credits;
    /*@ public invariant credits < 180 ==> !master &&
      @ credits >= 180 ==> master;
      @*/
    private /*@ spec_public @*/    boolean master;
    /*@ requires sname != null;
      @ assignable \everything;
      @ ensures name == sname && credits == 0 && master == false;
      @*/
    public Student (String sname) {
        name = sname;
        credits = 0;
        master = false;
    }
    /*@ requires c >= 0;
      @ ensures credits == \old(credits) + c;
      @ assignable credits, master;
      @ ensures (credits > 180) ==> master;
      @*/
    public void addCredits(int c) {
        updateCredits(c);
        if (credits >= 180) {
            changeToMaster();
        }
    }
    /*@ requires c >= 0;
      @ ensures credits == \old(credits) + c;
      @ assignable credits;
      @*/
    private void updateCredits(int c) {
        credits += c;
    }
    /*@ requires credits >= 180;
      @ ensures master;
      @ assignable master;
      @*/
    private void changeToMaster() {
        master = true;
    }
    /*@ ensures this.name == name;
      @ assignable this.name;
      @*/
    public void setName(String name) {
        this.name = name;
    }
    /*@ ensures \result == name;
      @*/
    public /*@ pure @*/ String getName() {
        return name;
    }
}

运行ESC检查：

java -jar openjml.jar -encoding utf-8 -esc Student.java

得到如下输出

Student.java:34: 警告: The prover cannot establish an assertion (ArithmeticOperationRange)
in method updateCredits:  overflow in int sum
        credits += c;
                ^

显然，当credits==2147483467且c>0时，credits会发生溢出。

JMLUnitNG

测试Graph

java -jar $HOME/jmlunitng-1_4.jar -cp src:$HOME/specs-homework-2-1.2-raw-jar-with-dependencies.jar -sp $HOME/specs-homework-2-opensource/src/main/java -d test src/MyGraph.java
javac -cp src:$HOME/specs-homework-2-1.2-raw-jar-with-dependencies.jar -d test src/**/*.java
java -jar $HOME/openjml.jar -cp src:$HOME/specs-homework-2-1.2-raw-jar-with-dependencies.jar -d test -rac -racShowSource src/MyGraph.java
javac -cp test:$HOME/jmlunitng-1_4.jar:$HOME/specs-homework-2-1.2-raw-jar-with-dependencies.jar -d test test/*.java
java -cp test:$HOME/jmlunitng-1_4.jar:$HOME/specs-homework-2-1.2-raw-jar-with-dependencies.jar MyGraph_JML_Test

注意：这里的OPENJML没有指定规格路径，是由于Graph的规格导致OPENJML出现以下错误：

error: A catastrophic JML internal error occurred.  Please report the bug with as much information as you can.
  Reason: Unexpected call of JmlFlow.visitJmlTypeClauseConstraint
1 error

不指定Graph规格，也能生成测试，但是只盲目测试了边界。

[TestNG] Running:
  Command line suite

Passed: racEnabled()
Passed: constructor MyGraph()
Passed: <<MyGraph@18ef96>>.addPath(null)
Passed: <<MyGraph@ba4d54>>.containsEdge(-2147483648, -2147483648)
Passed: <<MyGraph@de0a01f>>.containsEdge(0, -2147483648)
Passed: <<MyGraph@4c75cab9>>.containsEdge(2147483647, -2147483648)
Passed: <<MyGraph@1ef7fe8e>>.containsEdge(-2147483648, 0)
Passed: <<MyGraph@6f79caec>>.containsEdge(0, 0)
Passed: <<MyGraph@67117f44>>.containsEdge(2147483647, 0)
Passed: <<MyGraph@5d3411d>>.containsEdge(-2147483648, 2147483647)
Passed: <<MyGraph@2471cca7>>.containsEdge(0, 2147483647)
Passed: <<MyGraph@5fe5c6f>>.containsEdge(2147483647, 2147483647)
Passed: <<MyGraph@6979e8cb>>.containsNode(-2147483648)
Passed: <<MyGraph@763d9750>>.containsNode(0)
Passed: <<MyGraph@2be94b0f>>.containsNode(2147483647)
Passed: <<MyGraph@d70c109>>.containsPathId(-2147483648)
Passed: <<MyGraph@17ed40e0>>.containsPathId(0)
Passed: <<MyGraph@50675690>>.containsPathId(2147483647)
Skipped: <<MyGraph@31b7dea0>>.containsPath(null)
Passed: <<MyGraph@3ac42916>>.getDistinctNodeCount()
Failed: <<MyGraph@47d384ee>>.getPathById(-2147483648)
Failed: <<MyGraph@2d6a9952>>.getPathById(0)
Failed: <<MyGraph@22a71081>>.getPathById(2147483647)
Failed: <<MyGraph@3930015a>>.getPathId(null)
Failed: <<MyGraph@629f0666>>.getShortestPathLength(-2147483648, -2147483648)
Failed: <<MyGraph@1bc6a36e>>.getShortestPathLength(0, -2147483648)
Failed: <<MyGraph@1ff8b8f>>.getShortestPathLength(2147483647, -2147483648)
Failed: <<MyGraph@387c703b>>.getShortestPathLength(-2147483648, 0)
Failed: <<MyGraph@224aed64>>.getShortestPathLength(0, 0)
Failed: <<MyGraph@c39f790>>.getShortestPathLength(2147483647, 0)
Failed: <<MyGraph@71e7a66b>>.getShortestPathLength(-2147483648, 2147483647)
Failed: <<MyGraph@2ac1fdc4>>.getShortestPathLength(0, 2147483647)
Failed: <<MyGraph@5f150435>>.getShortestPathLength(2147483647, 2147483647)
Failed: <<MyGraph@1c53fd30>>.isConnected(-2147483648, -2147483648)
Failed: <<MyGraph@50cbc42f>>.isConnected(0, -2147483648)
Failed: <<MyGraph@75412c2f>>.isConnected(2147483647, -2147483648)
Failed: <<MyGraph@282ba1e>>.isConnected(-2147483648, 0)
Failed: <<MyGraph@13b6d03>>.isConnected(0, 0)
Failed: <<MyGraph@f5f2bb7>>.isConnected(2147483647, 0)
Failed: <<MyGraph@73035e27>>.isConnected(-2147483648, 2147483647)
Failed: <<MyGraph@64c64813>>.isConnected(0, 2147483647)
Failed: <<MyGraph@3ecf72fd>>.isConnected(2147483647, 2147483647)
Failed: <<MyGraph@483bf400>>.removePathById(-2147483648)
Failed: <<MyGraph@21a06946>>.removePathById(0)
Failed: <<MyGraph@77f03bb1>>.removePathById(2147483647)
Failed: <<MyGraph@326de728>>.removePath(null)
Passed: <<MyGraph@25618e91>>.size()

===============================================
Command line suite
Total tests run: 47, Failures: 26, Skips: 1
===============================================

测试Path

这里的OPENJML依然无法指定规格路径，否则会抛出Internal JML bug - please report. 。jmlunitng可以指定规格，但是不支持Java 8的新语法。

jmlunitng_jar=$HOME/openjml/jmlunitng-1_4.jar

java -jar $jmlunitng_jar -cp src:$HOME/specs-homework-2-1.2-raw-jar-with-dependencies.jar -sp $HOME/specs-homework-2-opensource/src/main/java -d test src/MyPath.java
javac -cp src:$HOME/specs-homework-2-1.2-raw-jar-with-dependencies.jar -d test src/**/*.java
openjml -cp src:$HOME/specs-homework-2-1.2-raw-jar-with-dependencies.jar -d test -rac -racShowSource src/MyPath.java
javac -cp test:$jmlunitng_jar:$HOME/specs-homework-2-1.2-raw-jar-with-dependencies.jar -d test test/*.java
java -cp test:$jmlunitng_jar:$HOME/specs-homework-2-1.2-raw-jar-with-dependencies.jar MyPath_JML_Test

结果即使指定了规格，自动生成的测试仍然存在一定程度的盲目，甚至出现忽视前置条件的情况

[TestNG] Running:
  Command line suite

Passed: racEnabled()
Failed: constructor MyPath(null)
Passed: constructor MyPath({})
Failed: <<MyPath@1>>.compareTo(null)
Passed: <<MyPath@1>>.containsNode(-2147483648)
Passed: <<MyPath@1>>.containsNode(0)
Passed: <<MyPath@1>>.containsNode(2147483647)
Passed: <<MyPath@1>>.equals(null)
Passed: <<MyPath@1>>.equals(java.lang.Object@1c2c22f3)
Passed: <<MyPath@1>>.getDistinctNodeCount()
Failed: <<MyPath@1>>.getNode(-2147483648)
Failed: <<MyPath@1>>.getNode(0)
Failed: <<MyPath@1>>.getNode(2147483647)
Passed: <<MyPath@1>>.hashCode()
Passed: <<MyPath@1>>.isValid()
Passed: <<MyPath@1>>.iterator()
Passed: <<MyPath@1>>.size()

===============================================
Command line suite
Total tests run: 17, Failures: 5, Skips: 0
===============================================

从以上例子可以看出，OPENJML以及JML自动生成测试的工具仍然有很大的改进空间。

架构设计

1

这次作业要求实现Path和PathContainer接口，直接按照题目要求实现对应的类。

2

这次作业新加了一个Graph接口，由于在增加、删除路径需要对已经建立的图进行重构，为了方便笔者直接将PathContainer合并到Graph的实现代码。实际上这严重违背了单一功能的原则。

3

这次作业笔者放弃了之前把PathContainer、Graph的实现写在一起的方法，将Graph和PathContainer的实现代码分离，MyRailwaySystem继承MyGraph实现RailwaySystem接口。

对Graph的实现中并没有包含图的存储和算法，而是新建一个类，存储图的数据结构和封装最短路算法（Floyd算法），对外提供求任意两点最短路径、求连通块等方法。

对RailwaySystem也同理，构造函数传入PathContainer、问题类型，建立不同的图，内部用Dijkstra或SPFA算法求最短路，实现缓存机制存储已经计算过的最短路长度。（不推荐笔者将问题类型传入构造函数的这种方式。这里应该实现一个Factory，根据问题类型构图）

bug和修复情况

1

这次作业代码在Path类的compareTo存在1个bug：

return getNode(i) - b.getNode(i);

显然这样直接相减，会出现整数运算溢出，导致原本大于关系应该返回正数，实际上返回负数。事实上，运行ESC检查很容易发现。

src/MyPath.java:84: warning: The prover cannot establish an assertion (ArithmeticOperationRange) in method compareTo:  underflow in int difference
            return getNode(i) - b.getNode(i);
                              ^
src/MyPath.java:84: warning: The prover cannot establish an assertion (ArithmeticOperationRange) in method compareTo:  overflow in int difference
            return getNode(i) - b.getNode(i);

由于compare方法溢出，强测只剩60分。令人遗憾的是，互测中没有人发现我的这个bug。

修复：改成使用Integer类的compare

return Integer.compare(getNode(i), b.getNode(i));

2

强测100分，互测也未发现bug。

3

由于拆点后添加的边数过多（最坏情况下，边数为\(120^3\)），而笔者使用的Dijkstra算法复杂度为\(O(m \log n)\) ，强测中有1个测试点超时。互测中，拆点后的构建的图出现最坏情况（形成稠密图）出现超时。

修复方法是：在仍然采用拆点的前提下，调整了构图策略，由原来换乘站拆出来的点之间相互连接(A_i---A_j)修改为连接到对应的中间节点(A_i---M_A)，减少边数。同时，由于拆出的点之间增加了中间节点，边(A_i--M_A)权重相应变为原来(A_i---A_j)的一半。

修复后，最坏情况下边数为\(120^2\)，比修复之前减少很多，成功解决了超时的问题。

对规格撰写和理解上的心得体会

规格的作用是约束，只关心状态变化，而不关心实现细节。

在第1次JML作业中，笔者尚未充分理解JML，对PathContainer的规格困惑了很久。后来才认识到JML规格中//@ public instance model non_null Path[] pList;只是一种形式，用来描述对结果的约束。
对于方法规格的撰写必须跳出面向过程的思维，不考虑实现细节，而是用JML描述函数的作用，包括结果必须满足的条件、修改的变量、参数的要求、异常等。
数据规格的编写主要是不变式invariant 和状态变化约束constraint ，同时注意到这些约束只针对可见状态，而不是任意时刻。

码农公寓

面向对象第三单元博客作业

JML Language

Theory

Toolchain

SMT Solver

部署

最简单的例子

JMLUnitNG

测试Graph

测试Path

架构设计

1

2

3

bug和修复情况

1

2

3

对规格撰写和理解上的心得体会

相关文章