oo第三单元总结

一.梳理JML语言的理论基础、应用工具链状况

(1)JML语言的理论基础

 JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言（Behavior Interface Specification Language，BISL），基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。JML主要由Leavens教授在Larch上的工做，并融入了BetrandMeyer， John Guttag等人关于Design by Contract的研究成果。
 JML以javadoc注释的方式来表示规格，每行都以@起头。有两种注释方式，行注释和块注释。其中行注释的表示方式为 //@annotation ，块注释的方式为 /* @ annotation @*/ 。
 JML的表达式是对Java表达式的扩展，新增了一些操做符和原子表达式。一样JML表达式中的操做符也有优先级的概念。特别须要提醒，在JML断言中，不可使用带有赋值语义的操做符，如 ++，--，+= 等操做符，由于这样的操做符会对被限制的相关变量的状态进行修改，产生反作用。
 方法规格是JML的重要内容。方法规格的核心内容包括三个方面，前置条件、后置条件和反作用约定。其中前置条件是对方法输入参数的限制，若是不知足前置条件，方法执行结果不可预测，或者说不保证方法执行结果的正确性；后置条件是对方法执行结果的限制，若是执行结果知足后置条件，则表示方法执行正确，不然执行错误。反作用指方法在执行过程当中对输入对象或 this 对象进行了修改（对其成员变量进行了赋值，或者调用其修改方法）。
 类型规格指针对Java程序中定义的数据类型所设计的限制规则，通常而言，就是指针对类或接口所设计的约束规则。

(2)应用工具链状况

 openjml，使用SMT Solver来对检查程序实现是否知足所设计的规格。目前openjml封装了四个主流的solver：z3, cvc4, simplify, yices2。
 JMLUuitNG/JMLUuit则根据规格自动化生成测试样例，进行单元测试。

二.部署JMLUnitNG/JMLUnit，针对Graph接口的实现自动生成测试用例， 并结合规格对生成的测试用例和数据进行简要分析

部分测试以下：

package o.c10;
import org.junit.After;
import org.junit.Assert;
import org.junit.Before;
import org.junit.Test;

public class MyGraphTest {
    private MyGraph myGraph = new MyGraph();
    private MyPath path1, path2, path3, path4;

    @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);
        path4 = new MyPath(2, 5, 6, 8, 9);
        myGraph.addPath(path1);
        myGraph.addPath(path2);
        myGraph.addPath(path3);
    }
    
    @After
    public void after() {
    }
    
    @Test
    public void testSize() {
        Assert.assertEquals(myGraph.size(), 2);
    }
    
    @Test
    public void testContainsPath() {
        Assert.assertTrue(myGraph.containsPath(path1));
        Assert.assertTrue(myGraph.containsPath(path2));
        Assert.assertTrue(myGraph.containsPath(path3));
        Assert.assertFalse(myGraph.containsPath(path4));
    }
        
    public void testContainsPathId() {
        Assert.assertTrue(myGraph.containsPathId(1));
        Assert.assertTrue(myGraph.containsPathId(2));
        Assert.assertFalse(myGraph.containsPathId(3));
    }
    
    @Test
    public void testGetPathById() throws Exception {
        Assert.assertEquals(myGraph.getPathById(1), path1);
        Assert.assertEquals(myGraph.getPathById(2), path3);
    }
    
    @Test
    public void testGetPathId() throws Exception{
        Assert.assertEquals(myGraph.getPathId(path2), 1);
        Assert.assertEquals(myGraph.getPathId(path3), 2);
    }
    
    @Test
    public void testAddPath() {
        Assert.assertEquals(myGraph.addPath(path1), 1);
        Assert.assertEquals(myGraph.addPath(path3), 2);
    }
    
    @Test
    public void testRemovePath()throws Exception {
        Assert.assertEquals(myGraph.removePath(path2), 1);
        Assert.assertEquals(myGraph.removePath(path3), 2);
    }
    
    @Test
    public void testRemovePathById() throws Exception {
        myGraph.removePathById(1);
        Assert.assertTrue(!myGraph.containsPath(path2));
        myGraph.removePathById(2);
        Assert.assertTrue(!myGraph.containsPath(path3));
    }
    
    @Test
    public void testGetDistinctNodeCount() throws Exception {
        Assert.assertEquals(myGraph.getDistinctNodeCount(), 5);
    }
    
    @Test
    public void testContainsNode() throws Exception {
        Assert.assertTrue(myGraph.containsNode(1));
        Assert.assertTrue(myGraph.containsNode(2));
        Assert.assertFalse(myGraph.containsNode(9));
    }
    
    @Test
    public void testContainsEdge() throws Exception {
        Assert.assertTrue(myGraph.containsEdge(1,2));
        Assert.assertFalse(myGraph.containsEdge(1,3));
        Assert.assertFalse(myGraph.containsEdge(1,9));
        Assert.assertFalse(myGraph.containsEdge(8,9));
    }
    
    @Test
    public void testIsConnected() throws Exception {
        Assert.assertTrue(myGraph.isConnected(1, 5));
        myGraph.addPath(path4);
        Assert.assertTrue(myGraph.isConnected(1, 9));
    }
    
    @Test
    public void testGetShortestPathLength() throws Exception {
        Assert.assertEquals(myGraph.getShortestPathLength(1, 5),4);
        myGraph.addPath(path4);
        Assert.assertEquals(myGraph.getShortestPathLength(1, 5),2);
    }
    
}

测试结果：

三.按照做业梳理本身的架构设计，并特别分析迭代中对架构的重构

第九次做业

类图：

 按照做业要求，设计了三个类，分别为Main类，MyPath类，MyPathContainer类。MyPath类，使用ArrayList存储结点序列；计算不一样点的方法，采起二分查找插入的方法。MyPathContainer类，新建了一个allList用来存储加入容器的全部结点；在添加路径和删除路径时，也采起二分查找插入的方法，修改allList中存储的结点；当要计算容器总的不一样点时，判断是否有新的点加入或者有旧的点消失，如果则遍历allList，若不是返回上次结果。

第十次做业

类图：

 按照做业要求，设计了四个类，分别为Main类，MyPath类，MyGraph类，Dis类。MyPath类跟第九次做业类似。Dis类，是用来储存结点信息的一个类，记录一个结点的链接点，是否被访问等信息。MyGraph类，调用Dis类，新建一个diList用来存储加入容器的全部结点；在添加路径和删除路径时，也采起二分查找插入的方法，修改allList中存储的结点,以及结点相应的链接点信息；当要计算容器总的不一样点时，直接返回diList的size()；当要判断是否存在点或边时，直接二分查找diList；当要判断是否相连或者找最短路径时，采起广度优先算法，查找diList。

第十一次做业

类图：

 按照做业要求，设计了六个类，分别为Main类，MyPath类，MyRailwaySystem类，Dis类，Dfs类，Pathdis类。MyPath类跟第九次做业类似。Dis类跟第九次做业类似。Pathdis类，是用来储存路径信息的一个类，记录一条路径的链接路径，是否被访问等信息。MyRailwaySystem类，调用Dis类，新建一个diList用来存储加入容器的全部结点，并调用Pathdis类，新建一个pathdiList用来存储加入容器的全部路径；在添加路径和删除路径时，也采起二分查找插入的方法，修改allList中存储的结点和结点相应的链接点信息，以及修改pathdiList存储的路径和路径的链接路径信息；当要计算容器总的不一样点时，直接返回diList的size()；当要判断是否存在点或边时，直接二分查找diList；当要判断是否相连或者找最短路径时，采起广度优先算法，查找diList。当要查找最少换乘时，使用pathdiList，而后采起广度优先算法。当要计算连通块时，调用Dfs类，采起深度优先算法，查找diList。因为计算最小满意度和最小票价的方法，没有来得及完成，因此也就再也不多述。

四.按照做业分析代码实现的bug和修复状况

第九次做业

 均为一个BUG，CPU超时。由于在查找容器的不一样点时，采起的是两层嵌套的遍历。修复则经过新建一个集合来记录全部结点，查找不一样点时，则直接查找这个集合。

第十次做业

 本次做业没有BUG。

第十一次做业

 因为本次做业并未及时完成，因此再也不多述。

五.阐述对规格撰写和理解上的心得体会

 当方法要实现的功能愈来愈难，JML语言就变得复杂和冗长。从第九次到第十一次做业中能够看到，随着需求的增长，每一个方法的规格愈来愈长，也愈来愈难懂。在写做业的途中，理解规格就占据了三成的做业时间，而且第十一次做业，一个需求被多个方法共同辅助完成时，在理解完方法的规格后，还要考虑方法之间的联系，这使得第十一次做业并未及时完成。  同时也感觉到，JML做为对Java程序进行规格化设计的一种表示语言，在大型工程和团队开发中，会起到很大的做用，由于其确保了每一个模块的准确性，避免了没必要要信息或错误信息的产生和传达。