OO第三单元小结

一.JML语言理论基础及工具链梳理

在本单元我们学习了JML语言的一些基础知识，能够让我们看懂简单的JML规格并写出对应代码，

　　 主要用到的知识点有：

　　  1.requires 该子句定义了方法的前置条件

　　  2.\old(exp)，表示执行相应方法前表达式exp的取值

　　  3.assignable子句，列出方法修改的类成员属性。

　　  4.ensure子句，定义了后置条件，如返回的结果或者该方法运行后的逻辑结果等等

　　  5.\result表达式，表示方法返回的逻辑上的正确的结果

　　  主要用的工具有：

　　  Openjml，junit等，主要作用是测试jml的正确性以及代码实现的正确性。

二.JUNIT的使用

import com.oocourse.specs1.models.Path;
import com.oocourse.specs1.models.PathContainer;
import org.junit.After;
import org.junit.Assert;
import org.junit.Before;
import org.junit.Test;

public class MyPathContainerTest {
private final PathContainer pathContainer = new MyPathContainer();
private Path path1, path2, path3;

@Before  
public void before() {  
    path1 = new MyPath(1, 2, 3, 4);  
    path2 = new MyPath(1, 2, 3, 4);  
    path3 = new MyPath(1, 2, 3, 4, 5);  
}

@After  
public void after() {  
    // do something here  
}

@Test  
public void testAddPath() throws Exception {  
    Assert.assertEquals(1, pathContainer.addPath(path1), 1);  
    Assert.assertTrue(pathContainer.containsPathId(1));  
    Assert.assertEquals(path1, pathContainer.getPathById(1));  
    Assert.assertEquals(1, pathContainer.size());

    Assert.assertEquals(1, pathContainer.addPath(path2));  
    Assert.assertTrue(pathContainer.containsPathId(1));  
    Assert.assertEquals(path2, pathContainer.getPathById(1));  
    Assert.assertEquals(1, pathContainer.size());

    Assert.assertEquals(2, pathContainer.addPath(path3));  
    Assert.assertTrue(pathContainer.containsPathId(2));  
    Assert.assertEquals(path3, pathContainer.getPathById(2));  
    Assert.assertEquals(2, pathContainer.size());

}  

}

　　这一段测试代码简单地测试了addPath的基本功能，测试结果符合预期。

三.架构梳理

第一次作业：

第一次作业中简单的使用了一个由id到PATH，一个由PATH到id的Hashmap来存储PATH，

又使用了另一个由id到出现次数的hashmap来统计不同的点个数。

第二次作业：

第二次作业中创建了一个Node类来存储有关节点的相关信息，又建立了一个类来存储

dijistra算法的实现，类方法的主要实现依托于将大数转化成小数，并且利用数组来

存储node。

第三次作业：

第三次作业中四种不同的需求其实都可以抽象成求一个图中的最短距离，唯一不同的

只是每种需求对应的图不一样，因此此次作业中使用了一个Map类来存储这4个不一样

的图，并且对每个图应用dijistra算法即可得到答案。

四.bug分析

第一次作业中没有出现bug。

第二次作业在删除点的邻接点时出现了逻辑错误，修复逻辑即成功。

第三次作业中没有出现bug。

五.总结

　　在本单元的学习中，在jml的学习这一部分，入门的难度其实不是很高，因为只要

细细研读了学习手册，对于基本的jml用法就都能够掌握。看懂jml是没有问题的，但是

如果说要让我们自己去写一段jml规格，那难度就不小了，首先是对于它的一些语法书写

很生疏，其次是我们很难去保证我们书写的正确性。

　　但幸好本单元的作业还是基于jml写代码，那么就没有给我们带来太多的书写jml的

困扰。总而言之，jml语言设计出来对代码的书写者是比较友好的，但是由于我们的学习中

对jml没有一套完整的学习流程，因此它对于我们初学者又非常的不友好。但最重要的其实

也不是对jml的学习，而是学习它规范代码的思维。

　　相信jml的学习体系会越来越好。