OO-JML總結

時間 2019-11-12

標籤 jml 總結简体版

原文原文鏈接

JML語言理論基礎

JML是對java代碼進行規格抽象的一種表達手段。java

面向對象的重要原則就是過程性的思考應該儘量地推遲。而JML能夠幫助咱們去靠近這個原則。其經過一些邏輯符號等表示一個方法是幹什麼的，卻並不關心它的實現，幫助你更好的用面向對象的思想去實現代碼。node

JML應用工具鏈

使用JML編譯器能夠編譯含有JML標記的代碼，所生成的類文件會檢查JML規範。git

若是程序沒有遵循規範，則會拋出unchecked exception來講明程序違背哪一條規範。github

JML工具備JML運行期斷言檢查編譯器、Jmldoc、jmlunnit等，其中jmlunit能夠生成一個java類文件測試的框架，能夠方便得使用Junit工具測試含有JML標記的java代碼。算法

部署SMT Solver

由於windows下用命令行真是太不方便了，我直接在IDEA中部署了openJML，官方github下載openjml，解壓，而後導入IDEAwindows

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