OO-JML总结

JML语言理论基础

JML是对java代码进行规格抽象的一种表达手段。

面向对象的重要原则就是过程性的思考应该尽量地推迟。而JML能够帮助咱们去靠近这个原则。其经过一些逻辑符号等表示一个方法是干什么的，却并不关心它的实现，帮助你更好的用面向对象的思想去实现代码。

 

JML应用工具链

使用JML编译器 能够编译含有JML标记的代码，所生成的类文件会检查JML规范。

若是程序没有遵循规范，则会抛出unchecked exception来讲明程序违背哪一条规范。

JML工具备JML运行期断言检查编译器、Jmldoc、jmlunnit等，其中jmlunit能够生成一个java类文件测试的框架，能够方便得使用Junit工具测试含有JML标记的java代码。

 

部署SMT Solver

由于windows下用命令行真是太不方便了，我直接在IDEA中部署了openJML，官方github下载openjml，解 压，而后导入IDEA

Check-->Run Check便可运行

以MyPath为例：

 

/*D:\Mine\hw10\src\MyPath.java:12: 警告: The prover cannot establish an assertion (PossiblyNegativeIndex) in method MyPath nodes.add(nodeList[i]);*/
public MyPath(int... nodeList) { for (int i = 0; i < nodeList.length; i++) { nodes.add(nodeList[i]); //error! 
            /* 这是典型的下标可能为负的错误 * 须要增长 i >= 0 的判断 */ nodesset.add(nodeList[i]); } } /*D:\Mine\hw10\src\MyPath.java:49: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: D:\Mine\openjml\openjml.jar(specs/java/lang/Object.jml):76: 注: ) in method equals if (nodes.size() == ((Path) obj).size()) {*/
if (nodes.size() == ((Path) obj).size()) {  //error!
    /* 这是一种无异常判断的错误 * 这里须要增长异常判断 */
                return true; } else { return false; }/*D:\Mine\hw10\src\MyGraph.java:15: 警告: The prover cannot establish an assertion (NullField) in method MyGraph

 

以MyGraph为例

/*D:\Mine\hw10\src\MyGraph.java:15: 警告: The prover cannot establish an assertion (NullField) in method MyGraph private HashMap<Integer, Path> idToPath = new HashMap<>();*/
private HashMap<Integer, Path> idToPath = new HashMap<>(); //new HashMap<>()中<>补全 /*D:\Mine\hw10\src\MyGraph.java:301: 警告: The prover cannot establish an assertion (ArithmeticOperationRange) in method addEdge: overflow in int sum count++;*/ count++; //加法溢出 /*D:\Mine\hw10\src\MyGraph.java:91: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: D:\Mine\hw10\src\com\oocourse\specs2\models\PathContainer.java:57: 注: ) in method addPath if (path == null || !path.isValid()) {*/
 if (path == null || !path.isValid()) { //error //增长异常处理
            return 0; }

部署JMLUnitNG/JMLUnit

一样，我没有成功尝试命令行，仍然选择在IDEA中导入jmluniting.jar

(1) 在IDEA中下载TestMe

(2) project structure-->modules-->导入jmluniting.jar

(3) 对应类上alt+Ins --> test --> testme --> testNG

(4) 自动生成测试代码，开始测试

因为使用MyGraph存在许多问题，所以这里以一个简单的class为例

public class test {
    private int a;
    private int b;
    
    public test(int a1, int b1) {
        a = a1;
        b = b1;
    }
    
    public int add() {
        return a + b;
    }
    
    public int sub() {
        return a - b;
    }
    
    public int mul() {
        return a * b;
    }
    
}

生成测试代码

import org.testng.Assert;
import org.testng.annotations.Test;

public class testTest {
    test test = new test(0, 0);
    
    @Test
    public void testAdd() {
        int result = test.add();
        Assert.assertEquals( result, 0);
    }
    
    @Test
    public void testSub() {
        int result = test.sub();
        Assert.assertEquals(result, 0);
    }
    
    @Test
    public void testMul() {
        int result = test.mul();
        Assert.assertEquals(result, 0);
    }
}

//Generated with love by TestMe :) Please report issues and submit feature requests at: http://weirddev.com/forum#!/testme

运行

 

三次做业架构与迭代设计

第一次做业

主要是设计Path和 PathContainer

对于Path，观察JML发现：

一、Path中储存了可重复的nodes，所以能够采用可装入可重复元素容器：数组、arraylist等。

二、Path具备统计不一样nodes的功能，能够考虑使用HashSet来进行存储。

对于PathContainer，观察JML发现：

一、该类所操做的主要数据是id-->Path 的映射，且是一种双射。基于映射的特性，能够采用HashMap来存储。

二、对于双射：id-->Path，要求有双向查找功能，即须要实现函数和反函数的两种查找功能。又由于其是双射，两个HashMap来进行存储无疑是可行且高效的。

三、HashMap的key须要注意其compareTo接口，对于Path，须要咱们重写hashCode()。

注意：重写hashCode()要注重效率，毫不能采用直接return 1，必定要有所区分，尽量区别。

四、与Path相似，这里一样须要统计不一样Path的个数。简单的遍历必然会形成TLE。能够采用<path, count>的形式储存，直接统计其size()便可。把复杂度交给add和remove。

 

---

 

第二次做业：

主要是实现Graph。

对于图，无疑须要考虑两点：

一、数据结构

图须要考虑的是边和点。

对于点，

能够直接沿用上一次的存储方式。

对于边，

（1）大几率是个稀疏无向图，采用邻接矩阵不合适。

（2）回忆DS课关于稀疏矩阵的存储方式——邻接表。

（3）如何存邻接表？咱们须要尽量选择一种好的存储形式和容易来帮助咱们快速操做边（这里包括已知from，搜索to、便于增、删、查.....)

（4）基于（3）能够考虑构造映射起点-->全部终点+出现次数（便于删除）。

（5）基于（4），HashMap来作映射再好不过了。

二、图算法

主要涉及两种算法和一种机制

（1）图的连通性算法

不管是dfs、仍是bfs、仍是并查集，我的感受复杂度的差距不大。可是我更喜欢并查集+优化路径压缩，由于并查集维护起来我的感受比较方便，查找也比较快捷，缘由在于

**并查集是若干个集合（连通块），可以实现较快的合并和判断元素所在集合的操做。(听起来就很是适用本次的状况？？)

**查找复杂度O(1)，合并复杂度o(h)(h为合并后树的高度)

**union的复杂度能够分担给addPath

并查集学习连接http://www.javashuo.com/article/p-yytvowpn-hz.html

（2）最短路径算法

Dijsktra? or Flord?

我选择Dij，缘由在于Flord在个人认知里是有点浪费的。每次都求出全部点，最短路径，万一用不到呢？万一又被add、remove了呢？可是大量数据+少许图结构修改的前提下，选择Flord好像也不错。

（3）Cache机制

其实很简单，就是把已经算过的不管是最短路径仍是连通性，存储已经计算好的结果。（滚雪球）

下次调用时，先查询cache，后计算，防止重复计算。

修改图结构，须要清空cache。

 

---

 

第三次做业

这是一次让人头疼的做业。

与前面大有不一样的就是相似最短路径的算法增长了换乘的消耗。也就是weight(1-->1) == 0 || weight(1-->1) != 0

拆点是种好方法，但点太多容易炸内存，也容易炸时间。

所以，选择合适的拆点方法是重中之重。

直接强拆：

点抽象成<node, pathId>。增长node1 == node2 && pathId1 != pathId2 的边的权值

巧妙拆：

来自讨论区的想法。每一个点拆成站台+起点+终点

我的实现了这两种拆点方法。

先写了强拆的方法，发现1000+指令就有点受不了？？不知道是否是cache机制作的不够好？

后来临时补了巧妙拆的方法，时间上有了提高，但最后提交截至前出现bug没有解决，无奈交了初版。

最后果真被炸的体无完肤。

 

bug状况

第一次做业：

这是一次比较简单的做业，可是因为我考虑不周，出现了TLE的问题。

主要问题在于

(1)hashCode()重写过于简单，直接return1

(2)没有双HashMap配合，致使搜索复杂度太高

第二次做业：

本次做业没有发现bug

第三次做业：

本次做业因为巧妙拆点的方法在最后出现了bug，没有完成修复，最后提交了初版强拆点的，致使了TLE

 

心得体会

面向对象的思想要求咱们关注和设计每一个类和方法实现的效果，推迟中间过程化的思考。规则撰写很是有利于咱们去遵循这个原则，JML帮助咱们在设计层面更加规范化得思考每一个类和方法的状态，表达逻辑严谨，又能给后续编码带来好的指导。

规则撰写很是有助于理清思路，也有助于延展性的思考，对我的很是有帮助。