面向对象的程序设计-地铁路线计算程序的设计、优化与测试

面向对象的程序设计(2019)第三单元总结

I  JML 语言相关情况

　　在这次实验中，我们首次接触到了 JML 语言。初见，这个语言将设计时的架构设计和具体实现时的技术细节分离开，使得在不同阶段的任务更加明确，显著降低了出错的概率。

A JML 语言的理论基础

　　JML 是 Java 模块的一种行为接口规格语言(Behavior Interface Specification Language/ BISL)。JML 提供语义来规范描述 Java 模块的行为，防止模块设计出现歧义。JML 的目标是提供严格的形式语义，同时仍然可供任何 Java 程序员访问。由于规范可以作为 Java 程序文件中的注释编写，或者存储在单独的规范文件中，因此可以使用任何 Java 编译器编译具有 JML 规范的 Java 模块。JML 语言距其诞生已有20年的历史，是将 Leavens 的 Larch 项目和 BetrandMeyer, John Guttag 等人的 Design by Contract 理念相结合的成果，其坚实的理论基础为其应用铺平了道路。

B 应用工具链

　　规格描述方面，JMLdoc 工具类似于 Javadoc 工具，可以快速生成 JML 文档的相关文件。静态检查方面，有诸如 OpenJML 的项目用来对代码执行静态检查，其通过将 JML 规格转换成 SMT-LIB 格式的代码，调用成熟的 SMT Solver 进行检查。动态检查方面，Java 还有开源的集成 JML 检查的编译器，可以在运行期检查 JML 规范是否得到满足，对于不满足的规范进行报错处理。在自动测试方面，有 JMLUnitNG 一类的应用，可以根据规格自动生成测试文件，部分测试需要使用 JML 编译器编译集成，在运行期检查。生成的测试文件基于 TestNG 框架，可以很方便的根据模块开展测试。

II SMT Solver 部署

　　SMT Solver 是 OpenJML 的后端接口，用来分析语法树。以下部署尝试基于 macOS 10.14.4/OpenJDK 1.8.0 环境进行。

A Command Line 部署方案

　　命令行中尝试了很多方式都无法让 OpenJML 正确工作，但是 IntelliJ IDEA 的插件可以正常使用。疑惑之余，我研究了插件使用的 Java 版本，发现是 OpenJDK 版本的 Java。所以我通过以下命令安装了 1.8.0 版本的 OpenJDK，使得 OpenJML 可以在命令行正常使用。

B IntelliJ IDEA 部署方案

　　IntelliJ IDEA 工具有插件 OpenJML-ESC 插件较为成熟，可以调用本地的 OpenJML 工具执行静态检查。但是因为官方版本的插件过旧，而且功能有限，所以我新增了一些功能，更新了插件依赖的 IntelliJ IDEA Runtime Library 以支持最常见的 2018.3 版本。

　　在最初使用的时候，对于简单的文件依赖层次可以正确识别，经过检查发现插件并没有指定合适的 Classpath 和 Sourcepath 导致的问题，所以修改插件源码，在设置中添加依赖路径选项自动识别当前项目信息加入命令行，使得插件可以正确使用。

· 插件基本使用

1. 下载插件 Custom Build (仅适配 2018.3，其他版本需要自行编译)
2. 选择 IntelliJ IDEA -> Preferences -> Plugins => Install Plugin from Disk 选择下载的 .zip 文件
   
3. 重启 IDEA 并前往 IntelliJ IDEA -> Preferences -> Other Settings -> JML Checker 配置本地 OpenJML 解压路径，注意这里路径中不支持空格！
   
4. 按需求勾选 Add Sourcepath 和 Add Classpath 选项添加依赖
5. 选择需要检查的文件，执行菜单栏 Check -> Run Check 进行检查
   

C Eclipse 部署方案

　　Eclipse 拥有官方支持的插件，可以按官方教程添加源并安装即可。但是运行时会提示 NullPointerException 错误，和 A 中的错误相似。分析原因是因为使用的 Java 版本不对，但是 Eclipse 没有显式设置 IDE Java 版本的选项，也没有在互联网找到相关方法。简单试验后找到设置方式。

　　首先为设备安装可以运行的 OpenJDK 版本：

• macOS 用户　　

brew tap AdoptOpenJDK/openjdk
brew install adoptopenjdk-openjdk8

• Linux 用户

sudo apt-get install openjdk-8-jdk

　　安装好之后可以通过配置 ~/.bash_profile (用户) 或 /etc/profile (全局) 中加入  export JAVA_HOME=/Library/Java/JavaVirtualMachines/JAVA_VERSION.jdk/Contents/Home  来设置默认 Java 版本，也可以使用  alias JDK_8='export JAVA_HOME=$JAVA_8_HOME'  快捷切换 Java 版本。

　　Mac Eclipse 启动和运行插件所用的 JRE 版本在 Eclipse.app/Contents/info.plist 中定义 （ Windows 位于 eclipse.ini 中 ），添加 -vm 选项指定本地 Java 路径即可正确运行。

　　macOS 配置示例：

　　　　

　　Windows 配置示例：

　　

D 问题检查

　　受插件能力限制，部分错误是由于插件内部问题导致的，所以这里只贴出部分合理的报错结果供分析。

oo-codes-11/src/MyRailwaySystem.java:61: 警告: The prover cannot establish an assertion (InvariantExit: /Users/bxymartin/Documents/BUAA/oo-codes-11/src/com/oocourse/specs3/models/PathContainer.java:6: 注: ) in method MyRailwaySystem
    public MyRailwaySystem() {
           ^
oo-codes-11/src/com/oocourse/specs3/models/PathContainer.java:6: 警告: Associated declaration: /Users/bxymartin/Documents/BUAA/oo-codes-11/src/MyRailwaySystem.java:61: 注: 
    //@ public invariant pList.length == pidList.length;
               ^
/Users/bxymartin/Documents/openjml-0.8.42/openjml.jar(specs/java/util/Map.jml):76: 警告: The prover cannot establish an assertion (Invariant) in method MyRailwaySystem
        public invariant content.owner == this;
               ^
/Users/bxymartin/Documents/openjml-0.8.42/openjml.jar(specs/java/util/Map.jml):76: 警告: The prover cannot establish an assertion (Invariant) in method MyRailwaySystem
        public invariant content.owner == this;
               ^
/Users/bxymartin/Documents/openjml-0.8.42/openjml.jar(specs/java/util/Map.jml):76: 警告: The prover cannot establish an assertion (Invariant) in method MyRailwaySystem
        public invariant content.owner == this;
               ^
/Users/bxymartin/Documents/openjml-0.8.42/openjml.jar(specs/java/util/Map.jml):76: 警告: The prover cannot establish an assertion (Invariant) in method MyRailwaySystem
        public invariant content.owner == this;
               ^

　　上述错误是因为我使用了双 Map 映射的数据结构，导致并不能很好的满足不变式导致报错。

/Users/bxymartin/Documents/BUAA/oo-codes-11/src/MyRailwaySystem.java:301: 警告: The prover cannot establish an assertion (ArithmeticOperationRange) in method addHash:  overflow in int sum
                    loops.put(path.getNode(i), loops.get(path.getNode(i)) + 1);
                                                                          ^
错误: ESC could not be attempted because of a failure in typechecking or AST transformation: addPath

　　上述错误是因为自己的变量加没有判断是否上溢出的问题，因为实验时我们规定了范围，所以此处没有问题。此处仅举两例错误讨论，其他错误也均正常汇报出来了。

III JML Unit 使用

A 安装配置和生成样例

　　工作环境为 MacOS 10.14.4 OpenJDK 1.7.0，经试验 Java HotSpot 1.8.0 运行时会提示 “主版本 52 比 51 新, 此编译器支持最新的主版本。建议升级此编译器。” 导致不能正确运行，尝试编译 JMLUnitNG 发现是 OpenJML 不支持 1.8.0 导致的问题。官网推荐使用 OpenJDK 1.7.0，但是因为 Java 1.8.0 的许多新特性诸如 Lambda 表达式等不能被兼容，所以被迫改写。

/src/MyRailwaySystem.java:266: 错误: 找不到符号
                loops.merge(path.getNode(i), 1, Integer::sum);
                                                ^
  符号:   变量 Integer
  位置: 类 MyRailwaySystem

/src/MyRailwaySystem.java:39: 错误: 类型变量数目错误; 需要2
        sum = new HashMap<>();

　　改写之后问题减少到了一个

JMLUnitNG exited because of an irrecoverable error: 
org.jmlspecs.jmlunitng.JMLUnitNGError: Encountered 1 compilation errors: 
/Users/bxymartin/Documents/BUAA/specs-homework-3-opensource/src/main/java/com/oocourse/specs3/models/RailwaySystem.java:46: 错误: 需要']'
    /*@ ensures (exists int[
esult][] blocks; (forall int i, j; 0 <= i && i< 
esult && 0 <= j && j < blocks[i].length; containsNode(blocks[i][j]));
                             ^
    at org.jmlspecs.jmlunitng.JMLUnitNG.processAllCompilationUnits(JMLUnitNG.java:527)
    at org.jmlspecs.jmlunitng.JMLUnitNG.run(JMLUnitNG.java:414)
    at org.jmlspecs.jmlunitng.JMLUnitNG.main(JMLUnitNG.java:177)

 　　修正出错点的 JML 写法为

-    /*@ ensures (exists int[
esult][] blocks; (forall int i, j; 0 <= i && i<
 
esult && 0 <= j && j < blocks[i].length; containsNode(blocks[i][j]));
-      @          (forall int i; 0 <= i && i < 
esult; (forall int j, k; 0 <=
 j && j < k && k < blocks[i].length; blocks[i][j] != blocks[i][k] && isConnected
(blocks[i][j], blocks[i][k]))) &&
-      @          (forall int i, j; 0 <= i && i < j && j < 
esult; !(exists int k,m; 0 <= k && k < blocks[i].length && 0 <= m && m < blocks[j].length; isConnected(blocks[i][k], blocks[j][m])))&&
-      @          (sum int i; 0 <= i && i < 
esult; blocks[i].length) == getDistinctNodeCount());
+    
+    /*@ ensures (exists int[][] blocks; (forall int i, j; 0 <= i && i < blocks.length && 0 <= j && j < blocks[i].length; containsNode(blocks[i][j]));
+      @          (forall int i; 0 <= i && i < blocks.length; (forall int j, k; 0 <= j && j < k && k < blocks[i].length; blocks[i][j] != blocks[i][k] && isConnected(blocks[i][j], blocks[i][k]))) &&
+      @          (forall int i, j; 0 <= i && i < j && j < blocks.length; !(exists int k,m; 0 <= k && k < blocks[i].length && 0 <= m && m < blocks[j].length; isConnected(blocks[i][k], blocks[j][m])))&&
+      @          (sum int i; 0 <= i && i < blocks.length; blocks[i].length) == getDistinctNodeCount() && 
esult == blocks.length);

　　之后运行  java -jar /PATH/TO/JMLUNITNG.JAR -v -cp /PATH/TO/SPEC:. -d /OUTPUT/DIR MyRailwaySystem.java 即可正确输出测试文件。

B 运行测试用例

　　将生成的测试用例添加进 IDEA 工程中，添加 JMLUnitNG.jar 进入 Project Structure 中后运行，结果导出为 HTML （部分）结果如下。

 

　　可以看到，racEnabled 提示 java.lang.AssertionError: JMLUnitNG tests can only run on RAC-compiled code. 所以如果想要动态检查需要编译一下代码。

　　运行  java -jar /PATH/TO/OPENJML.JAR -rac -cp /PATH/TO/SPECS:. -d /OUTPUT/DIR *.java 发现受 OpenJML 局限性的影响，无法完成动态编译。

错误: A catastrophic JML internal error occurred.  Please report the bug with as much information as you can.
  Reason: MISMATCHED BLOCKS

MyRailwaySystem.java:6: 注: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
import com.oocourse.specs3.models.RailwaySystem;

Graph.java:18: 注: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
      @          (exists Path path; path.isValid() && containsPath(path); path.containsNode(toNodeId));

The operation symbol ++ for type java.lang.Object could not be resolved
org.jmlspecs.openjml.JmlInternalError: The operation symbol ++ for type java.lang.Object could not be resolved
    at org.jmlspecs.openjml.JmlTreeUtils.findOpSymbol(JmlTreeUtils.java:286)
    at org.jmlspecs.openjml.JmlTreeUtils.findOpSymbol(JmlTreeUtils.java:277)
    at org.jmlspecs.openjml.JmlTreeUtils.makeUnary(JmlTreeUtils.java:723)

　　在自动生成的测试中可以看出，由于没有成功启用 RAC，所以通过的测试都是因为随机生成的数据不符合前置条件导致的，而没能通过的测试是因为没有使用 RAC 编译程序导致的。判定测试是否成功的代码段如下：

    try {
      the_test_object.containsNode(nodeId);
    }
    catch (final JmlAssertionError $e) {
      if ($e.jmlAssertionType.equals("Precondition") &&
          $e.getStackTrace().length >= 4 &&
          "test_containsNode__int_nodeId__0".equals($e.getStackTrace()[3].getMethodName())) {
        // meaningless test because precondition failed
        throw new PreconditionSkipException($e.getMessage());
      } else {
        // test failure because something else failed
        throw new TestException($e.getMessage());
      }
    } catch (final Throwable $e) {
      // test failure for some reason other than assertion violation
      throw new TestException($e.getMessage());
    }

　　可以看到，不满足前置条件的输入会被判定为成功，以及未抛出异常的部分，所以这个测试没有起到作用，所以转而分析较简单的样例分析。

C 简单样例分析

　　这里转而分析一个和 Path 类较为相似的类，经过多次尝试终于可以成功应用工具链，必须将文件定义在一个包里才能正确生成，否则会产生奇怪的错误。

　　具体文件结构与测试文件如下：

.
├── demo
│   └── MyPath.java
└── run.sh

1 directory, 2 files

　　在根目录运行  bash run.sh  得到的文件目录如下：

.
├── demo
│   ├── MyPath.class
│   ├── MyPath.java
│   ├── MyPath_InstanceStrategy.class
│   ├── MyPath_InstanceStrategy.java
│   ├── MyPath_JML_Data
│   │   ├── ClassStrategy_int.class
│   │   ├── ClassStrategy_int.java
│   │   ├── ClassStrategy_java_lang_String.class
│   │   ├── ClassStrategy_java_lang_String.java
│   │   ├── ClassStrategy_java_lang_String1DArray.class
│   │   ├── ClassStrategy_java_lang_String1DArray.java
│   │   ├── containsNode__int_node__0__node.class
│   │   ├── containsNode__int_node__0__node.java
│   │   ├── getNode__int_index__0__index.class
│   │   ├── getNode__int_index__0__index.java
│   │   ├── main__String1DArray_args__10__args.class
│   │   └── main__String1DArray_args__10__args.java
│   ├── MyPath_JML_Test.class
│   ├── MyPath_JML_Test.java
│   ├── PackageStrategy_int.class
│   ├── PackageStrategy_int.java
│   ├── PackageStrategy_java_lang_String.class
│   ├── PackageStrategy_java_lang_String.java
│   ├── PackageStrategy_java_lang_String1DArray.class
│   └── PackageStrategy_java_lang_String1DArray.java
└── run.sh

2 directories, 25 files

　　脚本文件的执行顺序为，首先使用 JMLUnitNG 生成测试文件(如果同名不会覆盖!!!)，之后使用 Java 编译工具为每个文件生成 .class 文件，最后使用 OpenJML 工具生成带有 RAC 功能的 .class 文件。最后执行测试函数，内容如下：

java -jar ~/Downloads/jmlunitng.jar demo/MyPath.java
javac -cp ~/Downloads/jmlunitng.jar demo/**/*.java demo/*.java
java -jar ~/Documents/openjml-0.8.42/openjml.jar -rac demo/MyPath.java
java -cp ~/Downloads/jmlunitng.jar: demo.MyPath_JML_Test

　　注意，如果上述脚本的生成文件存在，则不会再次生成，运行  java -jar ~/Downloads/jmlunitng.jar -v demo/MyPath.java  可以看到如下输出：

Generating test class for class demo.MyPath
Not overwriting existing strategy for parameter node of boolean containsNode(int)
Not overwriting existing strategy for parameter args of void main(String[])
Not overwriting existing strategy for parameter index of int getNode(int)
Not overwriting existing global strategy for type int
Not overwriting existing global strategy for type java.lang.String
Not overwriting existing global strategy for type java.lang.String[]
Not overwriting existing package strategy for type int in package demo
Not overwriting existing package strategy for type java.lang.String in package demo
Not overwriting existing package strategy for type java.lang.String[] in package demo
Not overwriting existing instance strategy for class demo.MyPath

　　运行脚本结果为：

[TestNG] Running:
  Command line suite

Passed: racEnabled()
Passed: constructor MyPath()
Passed: <<demo.MyPath@64cee07>>.containsNode(-2147483648)
Passed: <<demo.MyPath@1761e840>>.containsNode(0)
Passed: <<demo.MyPath@6c629d6e>>.containsNode(2147483647)
Passed: <<demo.MyPath@27abe2cd>>.getNode(-2147483648)
Passed: <<demo.MyPath@5f5a92bb>>.getNode(0)
Passed: <<demo.MyPath@6fdb1f78>>.getNode(2147483647)
Passed: <<demo.MyPath@51016012>>.isValid()
Passed: <<demo.MyPath@29444d75>>.size()
Passed: static main(null)
Passed: static main({})

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

　　待测试文件内容为精简版的 MyPath.java ：

// demo/MyPath.java
package demo;

public class MyPath {
    private /*@ spec_public @*/ int[] nodes;

    public MyPath() {
        nodes = new int[10];
    }

    //@ ensures 
esult == nodes.length;
    public /*@ pure @*/ int size() {
        return nodes.length;
    }

    /*@ requires index >= 0 && index < size();
      @ assignable 
othing;
      @ ensures 
esult == nodes[index];
      @*/
    public int getNode(int index) {
        if (index < 0 || index >= nodes.length) {
            return -1;
        } else {
            return nodes[index];
        }
    }

    //@ ensures 
esult == (exists int i; 0 <= i && i < nodes.length; nodes[i] == node);
    public boolean containsNode(int node) {
        for (int i = 0; i < nodes.length; i++) {
            if (nodes[i] == node) {
                return true;
            }
        }
        return false;
    }

    //@ ensures 
esult == (nodes.length >= 2);
    public boolean isValid() {
        if (size() >= 2) {
            return true;
        }
        else {
            return false;
        }
    }

    public static void main(String[] args) {

    }
}

　　可以看到，JMLUnitNG 对输入的 int 参数进行了最大值，中值和最小值进行了测试，如果有多个输入，还会进行排列组合。

　　对于 Object 类的子类，会分别测试空和空对象两种情况。

IV 架构设计分析

A PathContainer 设计

　　PathContainer 作为容器包括基本的增删改查功能。在最初设计时，直觉的就想用规格里设计的单容器储存所有数据，在查询的时候正常查询即可。实现之后进行测试计时，发现如此实现会导致查找时的时间复杂度过高超时，所以需要优化查询过程为常数时间。所以最终确认使用双 Map 同时映射 ID -> Path / Path -> ID 以增加查询效率。同时对于统计独立节点数的操作，单独维护一个集合包括独立的节点，以优化多次查询时的效率。

B Graph 设计

　　这一次作业新增了 Graph 结构，需要应用图的知识检查节点之间的连通性和节点间的距离。和上次想法相似，为了加速边和节点的查询，在增删路径时维护两个集合以加快多次查询时的效率。对于连通性的检查，为了提高效率选择 Dijkstra 算法计算节点间路径连接是否合理。为了将业务逻辑分离，封装 Dijkstra 模块以加速相关内容的计算，同时由于 Dijkstra 算法的特性，一次单源点路径计算可以计算出到所有终点的所有路径长度，所以可以将结果保存下来，之后使用时可以提高速度。经压力测试计时后发现这种实现的时间满足需求。

C RailwayStation 设计

　　最后一次作业增加了很多相似的功能，其特征是变化边权重和换乘权重，求不同的数值。这次作业我的版本历经多次改版，反复迭代最终达到完美，深刻体会到面向对象设计的优势。

　　第一次实现，我鲁莽的在之前实现的基础上为每个节点添加了一个可达路线集合，如果当前路线在可达路线集合中，则说明不需要换乘，可以直接乘坐；如果当前线路不在换乘集合中，则需要额外附加换乘开销。在实现了之后自我反思和测试，发现这个实现有很严重的逻辑漏洞，因为换乘权重数值的不确定性，这个问题不存在最优子结构，所以不能通过这样来获得最小的路线权重。

　　

　　第二版的迭代采用了拆点加边的方法，对于每个换乘节点，设置两个总站点，一个作为起点，另一个作为终点，对每一个线路到达这个站的节点，分别连接这个站台的总起点与线路站点，线路站点和这个站台的总终点与站台总终点和总起点，这样在换乘的时候就可以应用普通的 Dijkstra 算法计算每一条路的权重。在实现了之后发现这个方法会增加大量的边，导致 Dijkstra 算法的时间会增加的特别多，压力测试甚至在 40 秒内都不能输出结束，所以只能再一次重构。

　　

　　第三版实现采用了拆点的方法，对于每一个可用的节点，在到达时不仅要访问当前节点的可达节点，还要访问其他路径中的相同编号的节点，同时添加换乘权重，这样在不加边的情况下访问了所有情况，显著降低了时间。同时，第三次作业对于权重有这不同的数值，所以我采用了继承的方法，重载获取权重的函数，使用一个类解决不同的功能。这样实现简单快捷，逻辑清晰，充分体现了面向对象设计的优势。

　　

　　最终的实现十分清晰，通过继承的方法实现了不同的计算需求，最顶层由 Dijkstra 类执行计算操作，使用 Distance 类保存和维护计算结果。其类图如下：

V 代码问题和修复 

A 运行超时

　　PathContainer 和 RailwayStation 在测试时都出现了超时的情况。通过优化数据结构和缓存结构，以及修正潜在的问题，可以解决问题。

　　其中最难发现的问题是计算更新 Dijkstra 图时候的逻辑问题。移除待遍历队列中的节点时，我在搜索时引用了新的值，而非队列中的旧值，使得虽然程序的运行结果正确，但是时间复杂度是平方的，并没有体现出算法的优越性。这个问题的发现起源于自己构造的强侧数据集会出现超时的情况，但是输出结果都是一样的，而且问题在于运行时间缓慢，所以很难找到问题所在。调试时首先需要找准可能运行缓慢的点，甚至考虑了类变量的声明位置对速度的影响。最后，在定位 Dijkstra 模块时发现了速度缓慢的异常函数，最终解决了问题。

B 连通区域发现错误

　　在编写 BFS 的时候因为忘记了调整节点映射所以在大规模测试时有一个点的映射有误，最终找出了问题。

C Unpleasant Value 计算出错

　　当两个节点相同时，通过规格没有看出具体数值应该为多少，所以误给了两个节点正常计算的数值，在线上评测发现应该为0，但是 JML 规格中并未找到相关描述。

VI 规格撰写的心得体会

　　规格的撰写需要一种模式化的抽象思维。规格概括了一系列对象共性特征后形成的类型，概括了一系列对象的行为能力以及概括了一系列对象的状态空间，弥补了面向对象除了结构抽象和行为抽象之外的规格抽象。撰写过程规格时按照输入-处理-输出的模式进行思考，首先考虑前置条件，即针对不同的输入类型需要采取什么样的条件；之后针对每一种条件撰写副作用，即会修改什么变量和结构，以及撰写可赋值的范围；最后撰写后置条件，即满足输入前置条件的情况下应该满足什么样的条件。除了描述函数功能之外，数据抽象规格还可以描述过程中的约束和不变量等方式规定始终满足的条件。撰写之后的规格可以用各种工具检查正确性，降低出错概率。

VII 自动测试系统

　　三次作业中均使用了相似结构的测试结构，实现了批量运行测试，统计运行时间与内存占用等功能，对于异常运行的数据集储存并报错。文件目录结构如下：

.
├── README.md
├── comm.py
├── compare.sh
├── start.sh
└── test_path
    ├── Railway.jar
    ├── clean.sh
    ├── comm.py
    ├── gen.py
    ├── specs-homework-3-1.3-raw-jar-with-dependencies.jar
    ├── test.sh
    └── test_case

2 directories, 10 files

　　主要逻辑函数为 comm.py，其中实现了对子进程运行时间的统计以及内存的统计，同时通过轮询的方式对超时的程序执行退出操作。

from subprocess import Popen, PIPE
import os, sys, time, resource
import signal
import time
import re

write_content=""
while True:
    line = sys.stdin.readline()
    if line:
        write_content=write_content+line
    else:
        break
with open("project.cache","r") as file:
    project = str(file.readline().strip('
'))
with open("package.cache","r") as file:
    package = str(file.readline().strip('
'))
with open("run.res","wb") as out, open("run.err","wb") as err:
    path_runner = Popen(['java', '-classpath', project + ':specs-homework-3-1.3-raw-jar-with-dependencies.jar', package], stdin=PIPE, stdout=out, stderr=err, shell=False)
start = time.time()
check_content=""
try:
    path_runner.stdin.write(write_content.encode())
    path_runner.stdin.flush()
    path_runner.stdin.close()
except KeyboardInterrupt:
    print("[!] ERROR:	 Terminating...")
    os.kill(path_runner.pid, signal.SIGTERM)
cut = resource.getrusage(resource.RUSAGE_CHILDREN)
try:
    timeout = 40
    t_beginning = time.time()
    seconds_passed = 0
    while True:
        if path_runner.poll() is not None:
            break
        seconds_passed = time.time() - t_beginning
        if timeout and seconds_passed > timeout:
            path_runner.terminate()
            print("[!] ERROR:	 Path Running Timeout!")
            raise TimeoutError("Elapsed For " + str(timeout) + " Seconds")
        time.sleep(0.5)
    ef = resource.getrusage(resource.RUSAGE_CHILDREN)
    elapsed = time.time() - start
except ChildProcessError:
    print("[!] WARNING:	 Real Time Limit Exceeded!")
    os._exit(0)
except KeyboardInterrupt:
    print("[!] ERROR:	 Terminating...")
    os.kill(path_runner.pid, signal.SIGTERM)
if path_runner.poll() != 0:
    print("[!] ERROR:	 Error Status On Exit!")

with open("run.tst","a+") as test:
    test.write(check_content)
with open("run.check","a+") as check:
    check.write(check_content)
print("[i] Baseline Refer:	 Base :{0:>7.3f}s | Upper:{1:>7.3f}MB".format(35.000, 768.000))
print("[i] Path Processor:	 Real :{0:>7.3f}s | Total:{1:>7.3f}s | Memory:{2:>7.3f}MB".format(elapsed, ef.ru_utime - cut.ru_utime + ef.ru_stime - cut.ru_stime, ef.ru_maxrss / 1024 / 1024))

with open("summary.log","a+") as log:
    log.write(str(ef.ru_utime + ef.ru_stime) + "
")
if ef.ru_utime+ef.ru_stime-cut.ru_utime-cut.ru_stime > 35.000 or ef.ru_maxrss >= 768 * 1024 * 1024:
    name=time.strftime("%Y-%m-%d~%H:%M:%S.log", time.localtime())
    with open("run.check","r") as test, open(name, "w+") as log:
        print("[-] Bad Result Found in " + name + "!")
        for line in test.readlines():
            log.write(line)

　　测试使用的数据集则由一个 Java 程序生成，有目的性的进行压力测试和随机测试。

import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.io.Writer;

public class Main {


    public static void main(String[] args) {
        // write your code here
        Generator gen = new Generator();
        for (int i = 0; i < 100; i++) {
            File file = new File("ins_stress_" + i + ".txt");
            try{
                Writer out = new FileWriter(file);
                out.write(gen.stress());
                out.close();
            } catch (IOException e) {
                System.out.println("IO Error!");
            }
            System.out.println(i);
        }
    }
}

import java.util.*;

public class Generator {
    double correct = 0.99;
    double rate = 0.8;
    int sum_50 = 0;
    int sum_1000 = 0;
    int number = 0;

    Map<Integer, Integer> nodeSet = new LinkedHashMap<>();
    HashMap<Integer, LinkedList<Integer>> pathSet = new HashMap<>();

    public Generator() {}

    HashSet<String> core_50 = new HashSet<String>() {{
        add("PATH_ADD");
        add("PATH_REMOVE");
        add("PATH_REMOVE_BY_ID");
    }};
    HashSet<String> core_1000 = new HashSet<String>() {{
        add("PATH_ADD");
        add("PATH_REMOVE");
        add("PATH_REMOVE_BY_ID");
        add("PATH_GET_ID");
        add("PATH_GET_BY_ID");
        add("CONTAINS_PATH");
        add("COMPARE_PATHS");
    }};
    HashSet<String> path = new HashSet<String>() {{
        add("PATH_ADD");
        add("PATH_REMOVE");
        add("PATH_GET_ID");
        add("CONTAINS_PATH");
    }};
    HashSet<String> id = new HashSet<String>() {{
        add("PATH_REMOVE_BY_ID");
        add("PATH_GET_BY_ID");
        add("CONTAINS_PATH_ID");
        add("PATH_SIZE");
        add("PATH_DISTINCT_NODE_COUNT");
    }};
    HashSet<String> none = new HashSet<String>() {{
        add("PATH_COUNT");
        add("DISTINCT_NODE_COUNT");
        add("CONNECTED_BLOCK_COUNT");
    }};
    HashSet<String> ids = new HashSet<String>() {{
        add("COMPARE_PATHS");
    }};
    HashSet<String> idnode = new HashSet<String>() {{
        add("PATH_CONTAINS_NODE");
    }};
    HashSet<String> node = new HashSet<String>() {{
        add("CONTAINS_NODE");
    }};
    HashSet<String> nodes = new HashSet<String>() {{
        add("CONTAINS_EDGE");
        add("IS_NODE_CONNECTED");
        add("SHORTEST_PATH_LENGTH");
        add("LEAST_TICKET_PRICE");
        add("LEAST_TRANSFER_COUNT");
        add("LEAST_UNPLEASANT_VALUE");
    }};

    ArrayList<String> all = new ArrayList<String>() {{
        addAll(path);
        addAll(id);
        addAll(none);
        addAll(ids);
        addAll(idnode);
        addAll(node);
        addAll(nodes);
    }};

    ArrayList<HashSet<String>> choice = new ArrayList<HashSet<String>>() {{
        add(path);
        add(id);
        add(none);
        add(ids);
        add(idnode);
        add(node);
        add(nodes);
    }};

    Random random = new Random();

    private String getCommand() {
        while (true) {
            HashSet<String> select = choice.get(random.nextInt(choice.size()));
            String target = shuffle(select, random.nextInt(select.size()));
            if (core_50.contains(target)) {
                if (sum_50 >= 50) {
                    continue;
                }
                sum_50++;
            }
            if (core_1000.contains(target)) {
                if (sum_1000 >= 1000) {
                    continue;
                }
                sum_1000++;
            }

            // Append Parameters
            String para =  parameter(select);
            String[] list = para.split("[-0-9]+");
            if (target.equals("PATH_REMOVE")) {
                LinkedList<Integer> p = link();
                for (String s:list) {
                    if (s.equals(" ") || s.equals(""))
                        continue;
                    p.add(Integer.valueOf(s));
                }
                for (int id:pathSet.keySet()) {
                    if (pathSet.get(id).equals(p)) {
                        remove(id);
                        break;
                    }
                }
            }
            else if (target.equals("PATH_REMOVE_BY_ID")) {
                if (list.length == 1 && !list[0].equals(" ") && !list[0].equals("") && Integer.valueOf(list[0]) <= number) {
                    remove(Integer.valueOf(list[0]));
                }
            }

            return target + para;
        }
    }

    private String parameter(HashSet<String> set) {
        while (true) {
            try {
                if (random.nextDouble() <= correct) {
                    if (set.equals(path)) {
                        if (random.nextDouble() <= rate) {
                            return path(random.nextInt(80)).toString();
                        }
                        return get().toString();
                    }
                    if (set.equals(id)) {
                        return " " + random.nextInt(number);
                    }
                    if (set.equals(ids)) {
                        return " " + random.nextInt(number) + " " + random.nextInt(number);
                    }
                    if (set.equals(none)) {
                        return "";
                    }
                    if (set.equals(idnode)) {
                        return " " + random.nextInt(number) + " " + shuffle(random.nextInt(nodeSet.size()));
                    }
                    if (set.equals(node)) {
                        return " " + shuffle(random.nextInt(nodeSet.size()));
                    }
                    if (set.equals(nodes)) {
                        return " " + shuffle(random.nextInt(nodeSet.size())) + " " + shuffle(random.nextInt(nodeSet.size()));
                    }
                }
                return parameter(choice.get(random.nextInt(choice.size())));
            }
            catch (Exception e) {
                continue;
            }
        }
    }


    private LinkedList<Integer> get() {
        return pathSet.get(random.nextInt(pathSet.size()));
    }

    private LinkedList<Integer> link() {
         return new LinkedList<Integer>() {
            @Override
            public String toString() {
                String r = "";
                for (int i = 0; i < this.size(); i++) {
                    r += " " + this.get(i);
                }
                return r;
            }

            @Override
            public boolean equals(Object o) {
                if (o instanceof LinkedList) {
                    if (this.size() == ((LinkedList) o).size()) {
                        for (int i = 0; i < this.size(); i++) {
                            if (this.get(i) != ((LinkedList) o).get(i)) {
                                return false;
                            }
                        }
                        return true;
                    }
                }
                return false;
            }
        };
    }

    private LinkedList<Integer> path(int len) {
        len = (len > 80) ? 80 : len;
        LinkedList<Integer> p = link();

            number++;
            for (int i = 0; i < len; i++) {
                int m;
                if (nodeSet.size() >= 120) {
                    m = shuffle(random.nextInt(nodeSet.size()));
                    p.add(m);
                }
                else {
                    m = random.nextInt();
                    p.add(m);
                }
                nodeSet.merge(m, 1, Integer::sum);
            }

            pathSet.put(number, p);

        return p;
    }

    private void remove(int id) {
        for(int i:pathSet.get(id)) {
            nodeSet.merge(i, -1, Integer::sum);
        }
        pathSet.remove(id);
    }

    private int shuffle(int i) {
        int res = 0;
        Iterator itr = nodeSet.keySet().iterator();
        while (itr.hasNext() && i-- >= 0) {
            res = (int) itr.next();
        }
        return res;
    }

    private String shuffle(HashSet<String> set, int i) {
        String res = "";
        Iterator itr = set.iterator();
        while (itr.hasNext() && i-- >= 0) {
            res = (String) itr.next();
        }
        return res;
    }

    private void init() {
        number = 0;
        nodeSet.clear();
        pathSet.clear();
        sum_50 = 0;
        sum_1000 = 0;
    }


    public String stress() {
        String s = "";
        init();
        for (int j = 0; j < 50; j++) {
            s += "PATH_ADD" + path(80) + "
";
        }
            for (int i = 0; i < 6000 - 50; i++) {
                s += shuffle(nodes, random.nextInt(nodes.size())) + " "
                        + shuffle(random.nextInt(nodeSet.size()))
                        + " "
                        + shuffle(random.nextInt(nodeSet.size()))
                        + "
";
            }
        return s;
    }

    public String generate(int min, int max) {
        String s = "";
        init();
        int len = random.nextInt(max - min + 1) + min - 1;
        for (int i = 0; i < len; i++) {
            s += getCommand();
            if (i < len - 1) {
                s += "
";
            }
        }
        return s;
    }
}

　　这样就形成了自动测试的完善体系，可以自由进行不同针对性的检测，是除了 JML 规格约束检查之外的另一个有效的验证手段。