梳理JML语言相关内容
1. JML语言理论基础
JML(Java modeling language)是一种行为接口规范语言(BISL)，可用于指定Java模块的行为。JML可以表达的约束包括类和接口的不变量，方法的前置条件和后置条件。JML具备基于Java表达式的断言语言(assertion language)，并提供模型类型库（集合、包等）用于定义为pure的Java类规范中。这些特质都为操作和检查JML规范的工具开发提供了切入点。
如何保障程序质量在信息时代已经成为一个具有重要意义的问题。基于契约的程序设计是一种提高程序质量的重要且有效的技术，但是形式化契约的制定是一件十分困难的工作，而程序不变量动态发现与生成是解决大中型程序契约制定困难的一种有效的方法。JML为详细的体现程序规范具体内容提供了详尽的语法支持，也对验证提供了一定的依据支持。
至于具体的使用规范以及示范样例，推荐浏览JML手册([4])。
可参考
[1] A. Hamie, "On the Relationship between the Object Constraint Language (OCL) and the Java Modeling Language (JML)," 2006 Seventh International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT'06), Taipei, 2006, pp. 411-414.
[2] Søndergaard, H., Korsholm, S. E., and Ravn, A. P. ( 2017) Conformance test development with the Java modeling language. Concurrency Computat: Pract Exper, 29: e4071. doi: 10.1002/cpe.4071.
[3]
[4]
[5]刘树锟,阳小华,刘杰.Java建模语言在程序不变量动态发现过程中的应用[J].计算机工程与设计,2007(18):4536-4538+4545.
2.应用工具链情况
[来源JML官网，瞎翻译一下……准确描述请看括号中的英文]
-
图形化用户界面应用 (the launcher for the graphical user interface tools)
-
JML检查器 (the checker)
-
编译运行时断言检查 (compile for runtime assertion checking)
-
包含JML规范信息的javadoc版本 (a version of javadoc that includes JML specification information)
-
针对执行或开发规范的编译 (compile for executing or prototyping specifications)
-
包含了在CLASSPATH中部署bin/jmlruntime.jar文件的java、VM版本，可运行使用jmlc编译的文件
(a version of java, the VM, that includes the bin/jmlruntime.jar file in the CLASSPATH, for running files compiled with jmlc)
-
包含了在执行规范时所需的运行时支持条件的java、VM版本，可运行使用jmle编译的文件
(a version of java, the VM, that includes the runtime support needed for executing specifications, for running files compiled with jmle)
-
从Java源文件生成框架规范文件 (generate skeleton specification files from Java source files)
-
生成用于JUnit单元测试的代码存根 (produce unit testing code stubs for use with JUnit)
-
结合了jmlc和 jmlunit的工作 (combines the work of jmlc and jmlunit)
-
JUnit用户界面的一个版本，包括CLASSPATH中的bin / jmlruntime.jar和bin / jmljunitruntime.jar文件，用于对使用jmlc编译的文件和jmlunit生成的测试用例运行基于JML和Junit的测试
(a version of JUnit's swing user interface that includes the bin/jmlruntime.jar and bin/jmljunitruntime.jar files in the CLASSPATH, for running JML and JUnit based tests on files compiled with jmlc and test cases generated by jmlunit)
-
Java程序验证工具，检查JML中注释的规范性，支持静态检查和运行时检查
-
基于Eclipse的JML编译器，提供运行时检查，提高编译速度，支持Java5和嵌套类等特性
-
用于JML的Java代码自动化单元测试生成工具，支持Java1.5+特性代码，使用Java反射自动生成非基本类型的测试数据
JMLUnit测试Graph接口
我感觉我对JMLUnit的理解还不太深，使用过程也非常迷惑，以下内容应该存在很多错误，之后得去阅读一下其它同学的优秀博客增长一下知识，再练习练习QWQ。
package com.oocourse.specs2;import com.oocourse.specs2.models.NodeIdNotFoundException;import com.oocourse.specs2.models.NodeNotConnectedException;import org.junit.Before;import org.testng.Assert;import org.testng.annotations.Test;public class MyGraphTest { private MyPath path1, path2, path3, path4; private MyGraph graph = new MyGraph(); @Before public void Before() { path1 = new MyPath(1, 2, 4); path2 = new MyPath(2, 3, 4, 5); path3 = new MyPath(5, 6, 7, 7, 8); path4 = new MyPath(9, 10); graph.addPath(path1); graph.addPath(path2); graph.addPath(path3); graph.addPath(path4); } @Test public void testIsConnected() throws NodeIdNotFoundException { Before(); Assert.assertTrue(graph.isConnected(1, 4)); Assert.assertTrue(graph.isConnected(1, 8)); Assert.assertFalse(graph.isConnected(2, 10)); } @Test public void testGetShortestPathLength() throws NodeIdNotFoundException, NodeNotConnectedException { Before(); Assert.assertEquals(graph.getShortestPathLength(1, 4), 2); Assert.assertEquals(graph.getShortestPathLength(1, 5), 3); Assert.assertEquals(graph.getShortestPathLength(8, 4), 4); }} 运行结果
单元框架设计
1.myPathContainer
- 需求：实现路径管理系统，实现容器内的增删改查以及统计不同结点数等操作。
- 分析：实现基础功能，按照JML提示以及对需求的理解完成函数。可以使用HashMap等数据结构优化程序效率，也可以在实现某些功能的时候顺带完成别的功能的实现，比如在添加路径进入容器的时候，顺带统计不同结点数。
- 实现：完成基础Path类->调用Path完成PathContainer容器类（将功能拆分成易复用且简洁的函数组合）
2.myGraph
- 需求：基于路径管理系统构建无向图系统。保持原有的路径增删改查功能，增加基于无向图特殊性质的查询操作。
- 分析：开始出现拓展需求，对基础功能的继承与拓展是必然的。而开放封闭原则（OCP/Open Closed Principle）是所有面向对象原则的核心。软件设计本身所追求的目标就是封装变化、降低耦合，而开放封闭原则正是对这一目标的最直接体现。实现最优的、正确的继承层次，就能保证不会违反开放封闭原则。[摘自网络] 在不改变基础代码的原则下，针对不断变化的需求进行灵活的扩展，这是我们构架软件的原则，也是这个单元的训练目的。因此，利用继承PathContainer这一点，调用已实现功能来扩展新功能以实现图结构。
- 实现：继承PathContainer->扩写相应函数构建无向图结构实现Graph->二维数组存储邻接矩阵，HashMap优化效率，使用Floyd计算最短路径
3.myRailwaySystem
- 需求：基于无向图系统，复合实现复杂需求，如换乘、乘车票价及不满意度等新需求。同时之前实现的对路径容器基本操作仍然需要保持正常运作。
- 分析：新需求的多样性与复杂性很好的体现了需求从抽象到具体的过程。分析多个需求的共性与特性，向下追溯至基础功能如何组合实现这些复杂需求。首先实际上最短路径问题、最少换乘次数问题、最低票价问题与最低不满意度问题都是相似的，本质上都是对无向图进行最短路径的求解，区别在与对结点和边的有不同的权重处理。因此可以按要求改变相应的权值，再通过使用封装好的基础Floyd算法通用的完成需求。
- 实现：继承Graph->扩写无向图实现RailwaySystem地铁系统->实现基于Floyd的相关算法，对权重进行区分的处理就能解决所有需求 [具体可参考大佬们的发言]
总览
纵观整单元，可以看见模块化与层次化对逐步解决复杂问题的重要性。使用基础模块进行组合拳攻击，减少了代码量，提高了复用率。遵守开放封闭原则，对问题逐层拆分，在简化问题的同时也能减少编码压力。学习工程化的思维与开发方法是相当必要的。
BUG分析
1. myPathContainer
- 问题：由于之前贪图简单实现，使用了ArrayList作为Path容器类的基础，没有深究ArrayList简单的查询访问操作背后的时间代价，以及在大数据集下运行的复杂度与不稳定性。主要问题都是出在程序效率低，运行过慢，鲁棒性较差等方面。
- 解决：将部分ArrayList结构替换成了HashMap结构，并且将部分ArrayList相关操作适当替换成了HashMap操作，极大的提高了程序效率。
2.myGraph
- 问题：增删操作对最短路径相关计算带来的影响考虑不全。首先是删除路径时的错误，边删除显然不易出错，但结点的删除需要考虑结点是否在别的路径出现、能不能完全删除的问题。其次是在新增路径以及删除路径后，对邻接矩阵的更新策略需要考虑全面，或者说更新策略需要有一定的鲁棒性。因此，多数的错误都出在频繁增删操作与查询操作交错时诱发的细节bug。
- 解决：改变矩阵更新策略。Floyd运行代价是相同的，因此可以操作基础矩阵，每次都进行简单但有效的覆盖刷新。
3.myRailwaySystem
问题：对复杂操作的策略考虑不全导致了程序出现了较多问题。
解决：重新梳理复杂操作的共性与特性，重构代码相应的实现。
规格撰写与理解的心得体会
反思回顾解决JML问题的一周，最大的体会就是思考比具体实现代码更重要。在对问题理解透彻思路清晰的情况下，编写代码进行具体实现的过程会更加条理更加简单。相反，在思路混乱理解迷糊的情况下，写出的代码就是一个马蜂窝……问题源源不断理还乱，鲁莽的编程得不偿失。
其次就是认识到规格对于软件设计与开发的重要性。规范编写规格的过程也是抽象问题、梳理思路、构建框架的过程。不必拘泥于具体的代码实现，而是宏观地抽象地思考如何解决问题，面向对象地思考对象的功能，考虑对象之间的关联，完善整个框架的构造。程序是具象化实现规格的实例，而规格本身也是形式化验证程序的依据，基于规格的测试方法能相对独立的完备的测试程序的正确性。这些都是花时间撰写规格、理解规格的意义所在。