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程序進行規格化設計的一種表示語言，在大型工程和團隊開發中，會起到很大的做用，由於其確保了每一個模塊的準確性，避免了沒必要要信息或錯誤信息的產生和傳達。