2019年北航OO第三次博客总结

1、JML语言理论基础及其工具链

1. JML语言理论基础

JML是用于对Java程序进行规格化设计的一种表示语言，是一种行为接口规格语言(Behavior Interface Specification Language，BISL),基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。JML主要由Leavens教授在Larch上的工做，并融入了BetrandMeyer， John Guttag等人关于Design by Contract的研究成果。近年来，JML持续受到关注，为严格的程序设计提供了一套行之有效的方法。经过JML及其支持工具，不只能够基于规格自动构造测试用例，并整合了SMT Solver等工具以静态方式来检查代码实现对规格的知足状况。通常而言，JML有两种主要的用法：

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

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

2. JML工具链

JML是一种语言，那必然须要一些测试工具来检验咱们用JML编写的规格的正确性。JML的测试可使用开源的JML编译器来编译含有JML标记的代码，所生成的类文件会在运行时自动检查JML规格，若程序未实现规格中的要求，JML运行期断言检查编译器会抛出一个uncheckedException来讲明程序违背了哪一条规格。JMLdoc工具与Javadoc工具相似，可在生成的HTML格式文档中包含JML规范。还有工具JMLUnitNG能够根据规格的实现自动生成TestNG测试样例。SMT在形式化方法、程序语言、软件工程、以及计算机安全、计算机系统等领域获得了普遍应用。SMT Solver工具能够以静态方式来检查代码实现对规格的知足状况。Openjml使用SMT Solver来对检查程序实现是否知足所设计的规格(specification)。目前openjml封装了四个主流的solver。z3由Microsoft开发的，并已在github上开源：https://github.com/Z3Prover/z3 其正式发布版可经过https://www.microsoft.com/en-us/download/details.aspx?id=52270得到。cvc4由Standford开发，能够经过http://cvc4.cs.stanford.edu/downloads/下载。 

2、JMLUnitNG测试流程

1. 实现文件树

test --> test.java

执行 jmlunitng test/Test.java

生成新的文件树

test
├── Test_InstanceStrategy.java
├── Test.java                                      
├── Test_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
├── Test_JML_Test.java
├── PackageStrategy_int.java
├── PackageStrategy_java_lang_String1DArray.java
└── PackageStrategy_java_lang_String.java2

2. 编译

1）javac 编译 JMLUnitNG的生成文件 java -cp jmlunitng-1_4.jar test.java

2）jmlc 编译咱们的java代码，生成class文件 openjml -rac test/Test.java

3. 测试

java -cp jmlunitng-1_4.jar test.Test_JML_Test 便可获得运行结果

3、三次做业架构设计与迭代

1. 第一次做业PathContainer

PathContainer主要是针对path的增删改查，指令都很简单也不涉及到算法，而又有运行时间的要求，所以主要为了锻炼咱们对JML的理解和对java中的各类容器的认识。我在MyPath类中采用的arraylist+hashset的方式，arraylist来计算路径长度，判相等，hashset用于计算distinctNodes.而MyPathContainer中，我采用了双hashmap，这样能保证根据path查pathid和根据pathid查path都有相同的复杂度O(1)。

2. 第二次做业Graph

Graph最重要的是出现了图这个概念，最重要的方法即是判连通和最短路径。我用了三个类：Vertex类，Edge类和Graph类三个类来存储图，每一个vertex有一个linkedlist的属性来储存邻接表，Graph中有一个hashmap来存储vertex和其对应的nodeId.算法上判连通我用的BFS，而最短路径因为边权值均为1所以也能够用BFS来作。因为图结构变化指令不多，所以distinctnodes是在每次加入删除path时计算，询问时直接返回便可。

3. 第三次做业RailwayStation

RailwayStation是一个实际应用的场景，包括此次做业实现的方法也是与实际生活息息相关的。这让咱们体会到了从简单的底层抽象到复杂的实际问题的分析流程。查连通块个数能够用多个BFS或者冰茶几，另外三个最低票价，最短换乘，最少不满意度其实都是虽短路径问题的变体。最短路径算法我采用的是时间复杂度为O(n^2)的dijkstra算法。对于最短换乘，我把每一个Path看做一个节点，若是两个Path中有相同的PathId则这两个Path有一条边相连，而后用BFS便可。而最低票价和最少不满意度，都是涉及到一个换乘的问题。我采用的是拆点的解决方案，权值赋值成换乘须要增长的便可。

4、Bug分析与修复

1. WA

第9次做业，也是我认为OO做业有史以来最简单的一次做业，然而个人强测却惨遭爆炸，缘由就是个人偏序比较comparable接口的实现错误。我对字典序的理解出现了误差，致使全部不是相同长度的路径的比较都会产生相反的结果。分析缘由，一是我C语言功底的薄弱，更重要的是我没有进行充足的测试，没有用Junit进行单元测试或者与自动生成测试样例与人对拍。在以后两次做业我加强了自个人测试于是以后没有出现正确性的问题。

2. CTLE

第11次做业个人strong15发生了CPU超时的状况，缘由是忘了写cache。在用dijkstra算法求解最短路径的过程当中，其实不止能够算出要求的最短路径，还有包含好多的中间结果(好比起点到好多点的最短路径)。而后，咱们须要作的，就是充分利用好这些本次暂时用不上的中间结果，使得之后的最短路运算被不断加速（准确的说，这样的架构下，求解次数越多，后期速度越快）。对于已经求出来的所有最短路结果(不管本次是否用得上)，都做为边加入到构建的图中(后续通过此段的时候，再也不须要一步步算)，并作好标记(对于访问已有结果的状况，能够直接出解)，使得这张图不断滚雪球，运算速度愈来愈快,这样能够极大的提升程序性能，下降CPU时间。

5、心得体会

1. 规格撰写与理解

经过这一单元三次做业还有课上的两次实验写下来，对规格也算是有了更深的理解。规格是对开发人员的规范，为严格的程序设计提供了一套行之有效的方法。咱们第三单元经过三节课的学习，了解了类规格，方法规格，数据规格的写法，最重要的是为何要写规格。总结来讲，类规格定义了与用户的契约，也定义了开发人员必须听从的规约。方法规格则由前置条件，后置条件和反作用组成，这是一个方法对实现者的规约。而数据规格则是类有效性的控制条件，constraint和invariant分别定义了数据状态须要知足的条件和数据修改须要知足的条件。

规格化设计是一种致力于保证程序正确性的设计方法，它本质上是一种设计方法。咱们能够利用WARRANTY方法来看待规格化设计。

Step1(Why): 为何须要这个方法？
Step2(Acceptance criteria): 这个方法所提供结果正确的断定条件是什么？
Step3(cleaR Requirement): 这个方法是否须要对调用者作出一些要求，从而确保可以产生正确结果？
Step4(ANticipated changes): 这个方法执行期间是否须要修改输入数据或者所在对象数据？
Step5(TrustY): 无需代码便可确认其语义

契约式设计是一种基于信任机制+权利义务均衡机制的设计方法学，JML的诞生正是源自于契约式设计的须要。经过本单元的学习，我感觉到了经过规格设计，能够更容易得到简洁和职责单一的设计和实现（复杂方法会致使直接写不清楚相应的规格）。另外一方面，通过实验和做业训练会发现，在不少状况下设计和撰写规格要比编写代码难。一旦规格肯定了，其实实现代码就变成了一个相对简单的事情，除非涉及复杂的算法要求。所以，多理解规格使用规格化设计，对咱们从此的软件开发大有裨益。

2. 想说的话

随着第三单元的结果，12周OO生涯已通过去了。本学期的OO课程也接近尾声，本学期OO课程作了很是大的改革，目前看来都是很是成功的，再次感谢老师助教们的付出。最后一单元是UML相关，但愿本身继续加油，给本学期的OO课程画上一个圆满的句号。