OO面向对象编程:第三单元总结

JML语言的理论基础与工具链

理论基础

JML（Java Metadata Language）是一种用于对Java程序进行规格化设计的语言，是一种行为接口规格语言(Behavior Interface Specification Language，BISL)，基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。JML的主要目标是为严格的程序设计提供一套有效的方法，通过JML及其支持工具，不仅可以基于规格自动构造测试用例，并整合了SMT Solver等工具以静态方式检查代码实现对规格的满足情况。

JML主要有以下两种主要用法：

开展规格化设计。交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。

针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这种方法在遗留代码的维护方面具有特别重要的意义。

工具链情况

OpenJML：自动检查JML规格文档并生成报告。

Junit自动测试类：用于验证JML规格文档的正确性。

JMLUnit NG/JMLUnit的部署与应用

安装OpenJML

从OpenJML官方GitHub仓库获取源码。

解压后，将.jar文件和Solver-Windows（适用于Windows系统）放在同一文件夹内（例如放在F:\jmlunitng文件夹下）。

在该文件夹下使用命令：$ java -jar openjml.jar "$@" 完成安装。

安装JMLUnit NG

从官网获取.jar包，安装方法与OpenJML相同。

调用命令：$ java -jar jmlunitng.jar "$@" 完成安装。

创建源文件

以getNode和size()为例：

public class MyPath implements Path {    private ArrayList nodes = new ArrayList();    public MyPath(int[] nodeList) {        int i;        for (i = 0; i < nodeList.length; i++) {            nodes.add(nodeList[i]);        }    }}

该实现使用动态数组存储路径中的节点。

生成测试文件

示例目录结构：

demo/├── Demo_InstanceStrategy.java├── Demo.java├── Demo_JML_Data/│   ├── ClassStrategy_int.java│   ├── ClassStrategy_java_lang_String1DArray.java│   ├── ClassStrategy_java_lang_String.java│   ├── compare__int_lhs__int_rhs__0__lhs.java│   ├── compare__int_lhs__int_rhs__0__rhs.java│   └── main__String1DArray_args__10__args.java├── Demo_JML_Test.java├── PackageStrategy_int.java├── PackageStrategy_java_lang_String1DArray.java└── PackageStrategy_java_lang_String.java

编译运行

使用javac编译JMLUnit NG生成文件：

$ javac -cp jmlunitng.jar demo/**.java

使用jmlc编译自己的文件，生成带有运行时检查的类文件：

$ java -jar openjml.jar -rac demo/Demo.java

运行测试：

$ javac -cp jmlunitng.jar demo/**.java$ java -cp jmlunitng-1_4.jar demo.Demo_JML_Test

架构设计与迭代优化

第1次规格作业

public class MyPath implements Path {    private ArrayList nodes = new ArrayList();    public MyPath(int[] nodeList) {        int i;        for (i = 0; i < nodeList.length; i++) {            nodes.add(nodeList[i]);        }    }}

该实现使用动态数组存储路径中的节点。

第2次规格作业

Path类与相关方法相比上次并无较大变化。Graph类中：

public class MyGraph implements Graph {    private ArrayList pathList = new ArrayList();    private ArrayList pidList = new ArrayList();    private int[][] graph = new int[252][252];    private int[][] dist = new int[252][252];    private int tempid = 1;    private int distinctcount = 0;    private boolean change = false;    private boolean changec = false;}

plist和pidList使用相同的数据结构，haha数组用于映射节点标识。Floyd算法用于计算最短距离。

第3次规格作业

RailwaySystem类中新增了三个二维数组：

private int[][] temp1 = new int[150][150];private int[][] temp2 = new int[150][150];private int[][] temp3 = new int[150][150];

主要用于解决以下问题：最小换乘次数、最少票价、最少不满意度。Dijkstra算法用于计算最短路径。

通过以上内容可以看出，随着规格作业的进行，代码架构逐步优化，解决了路径计算中的性能问题，并针对实际需求增加了功能模块。

转载地址：http://wosfk.baihongyu.com/

你可能感兴趣的文章