天天看點
傳回

第三單元總結：JML規格定義下的程式設計、驗證與測試

JML語言及工具

JML語言理論

JML語言利用前置條件、後置條件、不變式等限制文法，描述了Java程式的資料、方法、類的規格，是一種契約式程式設計的實作工具。

  1. 常用的JML語言特性
    • \result：表示方法的傳回值。
    • \old(expr)：表示在方法執行前的值。一般将所關心的表達式取值整體括起來。
    • \forall：全稱量詞修飾的布爾表達式，可聲明局部變量、覆寫變量的取值範圍，對目标條件進行驗證。
    • \exists：存在量詞修飾的布爾表達式，類似\forall。
    • \sum, \max, \min：對給定範圍的表達式進行運算。表達式的由聲明變量、取值範圍、表達式定義給出。
    • <==>, <==, ==>：邏輯推理表達式，含義與數理邏輯中相同。
    • \nothing, \everything：目前作用域下的變量範圍。
  2. 資料規格
    • 不變式 invariant ：在成員處于可見狀态下必須滿足的特性。其中可見狀态可了解為完整的穩定狀态。
    • 修改限制 constraint ：描述前序可見狀态 —> 目前可見狀态的變化限制。
    • 和方法的後置條件一起對資料的變化作出規約。
    • 資料規格可被子類繼承。
  3. 方法規格
    • 前置條件 requires BoolExpr1 || BoolExpr2 || …;
    • 後置條件 ensures BoolExpr1 || BoolExpr2 || …;
    • 副作用影響要求 assignable modifiable
    • 副作用影響判斷 \not_assigned(x,y,…) \not_modified(x,y,…)，可應用于後置條件的判斷。
    • pure方法：可以被JML引用，隻需撰寫後置條件。
    • JML可以調用Java程式中的pure方法進行通路、判斷等操作。
    • 方法的異常行為：normal_behavior, also, exceptional_behavior, signals () expr, signals_only;
    • 方法規格需要考慮到的範圍：
      • 修改參數
      • 傳回值
      • 修改成員變量
      • 修改this的引用
    • 方法規格的原則：
      • 關注執行效果（需求決定）和造成的其他影響
      • 無需關注實作方式本身
      • 本質仍是資料限制（讓資料産生變化、類間的資料通信）
      • requires語句需要覆寫所有可能的情況，包括exceptional_behavior和normal_behavior！
      • 條件互斥，并集為全集。

  4. 類規格

    在類内利用一些規格變量對類的資料結構維護進行抽象描述，同樣的與具體容器、對象等無關。（如pathList、pathIdList的雙數組例子）

    • 規格變量和類中維護的資料有功能上的聯系，但沒有實作上的聯系。
    • 從類的階層化上來看，子類繼承父類規格
    • 子類可以重寫父類的方法規格
    • 子類不能違反父類的規格，但是可以進一步收窄

JML工具鍊

  • 使用OpenJML對實作的代碼進行：
    1. JML文法靜态檢查：給出JML語言上的文法錯誤，并不關心代碼 
      java -jar specs/openjml.jar -check SourceToCheck.java
    2. 程式代碼靜态檢查：給出程式中可能出現的潛在問題，并不關心JML語言 
      java -jar specs/openjml.jar -esc SourceToCheck.java
    3. 運作時檢查：生成一個新的.class檔案，其中包含了運作時檢查的assertion，在運作和單元測試的時候将發揮作用 
      java -jar specs/openjml.jar -rac SourceToCheck.java
  • 使用JMLUnitNG根據JML語言自動生成TestNG測試
    1. 基于JML生成測試檔案： 
      java -jar ./specs/jmlunitng.jar SourceToTest.java
    2. 利用OpenJML的rac，生成含有運作時檢查的特殊.class檔案并替換原檔案 
      java -jar ./specs/openjml.jar -d bin/ -rac SourceToTest.java
    3. 運作TestNG測試 
      java -cp ./specs/jmlunitng.jar:bin SourceToTest_JML_Test

  • 組合使用，效果為：（對讨論區中的Demo.java進行試運作）

    确定自己的JML規格的文法正确性。

    運作前給出部分可能的警告：

    第三單元總結：JML規格定義下的程式設計、驗證與測試
    運作TestNG時針對性的進行測試：
    第三單元總結：JML規格定義下的程式設計、驗證與測試
  • 使用注意：
    • 環境應為java-8
    • 路徑内不能包含中文
    • 在開展TestNg測試前要使用OpenJML的RAC（運作時assertion檢查）重新編譯待測程式位元組碼
    • OpenJML不支援\forall int[] 和 \exists int[]

嘗試使用OpenJML的SMT Solver對簡單的類進行靜态驗證

首先，筆者嘗試使用OpenJML的靜态檢查（"-esc"）對Path.java進行驗證：

部分值得關注的規格代碼如下：

  •  構造函數及其規格： 
    1     private /*@spec_public@*/ ArrayList<Integer> nodes;
 2     private /*@spec_public@*/ HashSet<Integer> distinct;      // keep a unique set

 3 　　/*@ public normal_behavior
 4 　　@ requires nodeList != null && nodeList.length != 0;
 5 　　@ assignable \everything;
 6 　　@ ensures (\forall int i; 0<=i && i<nodeList.length; nodeList[i] == nodes.get(i));
 7 　　@ ensures (\forall int i; 0<=i && i<nodeList.length; distinct.contains(nodeList[i]));
 8 　　@ ensures (nodes.size() == nodeList.length);
 9 　　@ also
10 　　@ public normal_behavior
11 　　@ requires nodeList == null || nodeList.length == 0;
12 　　@ assignable \everything;
13 　　@ ensures (nodes != null && nodes.size() == 0);
14 　　@ ensures (distinct != null && distinct.size() == 0);
15 　　@*/
17     public Path(int... nodeList) {
18         if (nodeList == null || nodeList.length == 0) {
19             nodes = new ArrayList<Integer>();
20             distinct = new HashSet<Integer>();
21         } else {
22             nodes = new ArrayList<Integer>(nodeList.length);
23             distinct = new HashSet<Integer>(nodeList.length);
24             for (int x : nodeList) {
25                 nodes.add(x);
26                 distinct.add(x);
27             }
28         }
29     }
  • containsNode()方法及其規格： 
    　　//@ ensures \result == distinct.contains(node);
    public /*@pure@*/ boolean containsNode(int node) {
        return distinct.contains(node);
    }

這兩個方法和規格隻是作為兩個例子，剩下的規格大緻按照指導書即可。（注意OpenJML不支援 \forall int[] 和 \exists int[] ）

當運作靜态文法檢查時，沒有warning和error。

當運作靜态規格檢查時，出現如下的很多warning：

src/Path.java:17: 警告: The prover cannot establish an assertion (Postcondition: src/Path.java:11: 注: ) in method Path
    public Path(int... nodeList) {
           ^
src/Path.java:11: 警告: Associated declaration: src/Path.java:17: 注:
      @ ensures (\forall int i; 0 <= i && i < nodeList.length;
        ^
src/Path.java:17: 警告: The prover cannot establish an assertion (Postcondition: src/Path.java:13: 注: ) in method Path
    public Path(int... nodeList) {
           ^
src/Path.java:13: 警告: Associated declaration: src/Path.java:17: 注:
      @ ensures (\forall int i; 0 <= i && i < nodeList.length;
        ^
src/Path.java:17: 警告: The prover cannot establish an assertion (Postcondition: src/Path.java:15: 注: ) in method Path
    public Path(int... nodeList) {
           ^
src/Path.java:15: 警告: Associated declaration: src/Path.java:17: 注:
      @ ensures (nodes.size() == nodeList.length);
      
src/Path.java:93: 警告: The prover cannot establish an assertion (Postcondition: src/Path.java:91: 注: ) in method containsNode
        return distinct.contains(node);
        ^
src/Path.java:91: 警告: Associated declaration: src/Path.java:93: 注:
    //@ ensures \result == distinct.contains(node);

可以看到，OpenJML的ESC檢查認為我沒有滿足規格，甚至沒有滿足containsNode()方法中的return語句的規格（這個return和\result的對象是一模一樣的）。

而筆者對其他小的程式的驗證則沒有問題。

由此看來，OpenJML單獨作為一個驗證器去對類和方法進行靜态檢查，是不靠譜的。

其根本原因在于OpenJML所支援和識别的類型和類型的方法太少，其對基本資料類型的支援基本可用，但一旦涉及到了ArrayList等進階資料結構類，就表現地十分迷惑。

應該将其的runtime assertion checking（RAC）與JMLUnitNg一起使用，才能發揮其部分功能（為TestNg中的測試提供Assertion）。

使用JMLUnitNg自動生成測試用例并進行測試

首先對Path.java進行RAC注入下的TestNg測試

改寫JML和Java代碼後的，可用的MyPath.java源檔案如下Ubuntu PasteBin連結所示：

https://paste.ubuntu.com/p/zgsSCyRN5M/

首先進行如下生成操作：（可以寫作一個AutoGenerate.sh，之後直接運作 ./AutoGenerate.sh src/MyPath.java 即可）

java -jar ./specs/jmlunitng.jar -cp lib/oolib.jar:src "$@"　　　　　　　　# 生成TestNg和測試政策檔案
javac -cp ./specs/jmlunitng.jar:lib/oolib.jar -d bin/ src/*.java　　　　 # 編譯位元組碼
java -jar ./specs/openjml.jar -d bin/ -cp lib/oolib.jar:src -rac "$@"　　# 将RAC的assertion注入到Path.class中

 之後進行測試：（可以寫作一個AutoTest.sh，之後直接運作 ./AutoTest.sh MyPath 即可）

java -cp ./specs/jmlunitng.jar:lib/oolib.jar:bin "$@""_JML_Test"　　　　# 運作TestNg主檔案

得到如下結果： 

第三單元總結：JML規格定義下的程式設計、驗證與測試

可以看到，JMLUnitNg為TestNg生成了31個測試政策/用例。

首先測試Runtime Assertion Checking是否開啟，之後對各個方法進行測試（包括構造函數）。

對于參數為對象的方法，其生成的用例常常包括 NULL 和 空。

對于參數為int的方法，其生成的用例常常包括極值邊界資料和0。

一般地，JMLUnitNg生成的資料多在參數上和this上作出兩種變化，進行組合測試。

之後對PathContainer.java進行RAC注入下的TestNg測試

改寫JML和Java代碼後的，可用的MyPathContainer.java源檔案如下Ubuntu PasteBin連結所示：

https://paste.ubuntu.com/p/RTWW6SmrfB/

首先仍然進行如下生成操作：

./AutoGenerate.sh src/MyPathContainer.java

 之後進行測試：

./AutoTest.sh MyPathContainer

 得到如下結果：

第三單元總結：JML規格定義下的程式設計、驗證與測試

可以看到，本套件隻會盲目的進行邊界值、特殊值、NULL、空的測試，最多對this進行某些構造（外界不可知），

但是并不能對其進行針對性的測試，如傳入有特定意義的Path對象。

中間會遇到一個“A catastrophic JML internal error occurred.”錯誤。

經筆者實驗，原因為OpenJML不支援如下的forEach + Iterator語言特性：

1 for (int node : path) { // using the Path iterator, which implements the Iterable<>
2     // ...
3 }

應該換成如下顯式的Iterator寫法：

1 Iterator<Integer> it = path.iterator();
2 while (it.hasNext()) {
3     int node = it.next();  // using the iterator EXPLICITLY !!
4     // ...
5 }

恕我直言，如果真的使用這些組合工具，那麼程式員在寫代碼的時候不能首先考慮其美觀性、整潔性、（程式和程式員的）高效性，

反而要時刻考慮自己寫的代碼能否被OpenJML了解，

那麼這肯定是違背了我們使用這些工具的初衷的！

由于從Path和PathContainer中看出其測試水準十分平凡，故筆者不再打算繼續對Graph類進行自動測試。 

結論 

經過筆者的測試，OpenJML + JMLUnitNG的實用工具組合——一點也不“實用”！

具體總結如下：

  • 對複雜資料結構的支援差，對基本資料類型的支援好，對基本資料類型數組不支援量化表達式。
  • 不支援對自定義類的自動智能構造，隻能盲目測試null、empty等，更不用說自動構造一些特殊的Path對象來進行測試。
  • 對稍稍進階的Java語言特性不支援，寫代碼的時候居然還要考慮其“可跑性”。

是以，筆者認為：

JML語言是一個好的契約化程式設計的工具，但它絕不是導緻程式員花費額外時間去伺候、适應的理由。

JML語言（甚至混入一些自然語言進行描述）能夠顯著提升大型工程的正确性，進一步解放程式員和設計師等的工作，

但是其并不一定要用來真正的“跑起來”！

JML的重點是給人看的，而不是給機器看的。隻要程式員會看、會寫、會讀JML，會用它來給自己和産品帶來好處，這就夠了！

架構設計與疊代

 第一次作業

第一次作業十分簡單，故沒有采取什麼特殊的設計。

由于對未來需求的不明朗，暫時沒有使用Trie樹手寫的專一性強的資料結構等維護序列，而是使用了雙向HashMap這一相容性強的結構來維護Path。

類圖如下：

第三單元總結：JML規格定義下的程式設計、驗證與測試

第二次作業

第二次作業中，開始出現了圖的結構模型。

類似傳統算法競賽中的鄰接表結構存儲圖，筆者定義了若幹輔助類對圖結構進行管理：

  • Pair類：統計無向邊使用，本質是一個無序對。即(Node1, Node2)和(Node2, Node1)視作相等。
  • Edges類：類似鄰接表的資料結構，本質是 HashMap<Node, HashSet<Node>> 。即第一層HashMap為（有向）邊的起始點索引用，第二層儲存其所鄰接的所有結點。
  • Matrix類：類似二維不定長數組的資料結構，本質是HashMap<Node, HashMap<Node, Integer>> 。用來維護最短路徑結果的dis[][]數組。

在第一次作業擴充上的類圖如下：

第三單元總結：JML規格定義下的程式設計、驗證與測試

第三次作業

第三次作業中，出現了帶邊權的有向圖模型（拆點表示換乘後，圖成為了有向圖）。

在第二次作業的Matrix基礎上，筆者将Matrix進行改造，使其：

  • 既能表示(u, v)間的dis最短路徑距離：(u, v, dis[u][v])
  • 又能用于存儲有向圖及其邊權：(u, v, w)

達成了資料結構的複用（源于二者的本質都是點-點-資料關系）。

此外，将原本的Integer表示節點，更改為封裝一個Node(NodeId, PathId)類來進行管理：

  • NodeId表示原先的結點号
  • PathId表示由哪條線路拆點而來
  • 拆點算法中，NodeId的公共源點為Node(NodeId, -1)（由于PathId滿足PathId>0恒成立）
  • 拆點算法中，NodeId的公共彙點為Node(NodeId, 0) （由于PathId滿足PathId>0恒成立）

同時，将原先的無序對Pair擴充，變成有序對OrderedPair和無序對Pair，便于對原圖（拆點前）和最短路圖（拆點後）的邊進行統計管理。

将部分操作移出MyRailwaySystem類，分散、歸因到負責求最短路的ShortestPath類、負責求聯通性的Connectivity類、負責維護圖結構的GraphAction類中。

第三單元總結：JML規格定義下的程式設計、驗證與測試

 這樣設計的直接好處是程式的各個方法和類的複雜度都不高，隻有compareTo、查詢鄰接表等方法稍稍高，

但比起第一單元的多項式程式而言，複雜度控制有了長足的進步。

第三單元總結：JML規格定義下的程式設計、驗證與測試

bug與測試

測試部分，由于本次作業屬于傳統的非時序輸入-非時許輸出問題，故可以使用對拍器+資料生成器進行對拍檢查。

而對于資料生成器的構造政策，由于本單元的正确性和算法效率要求并存，故采用以下的測試政策：

  • 針對算法時間複雜度測試，構造完全包含公測和互測資料規模的資料進行極限測試。

    如要求PATH_ADD + PATH_REMOVE總共不超過50條時，構造PATH_ADD 和 PATH_REMOVE 均達到50條的規模。

    這樣測試才能保證自己的測試 完全覆寫了 正式測試的資料規模。

  • 針對正确性測試，由于本單元作業中查詢的正确性至關重要，故将資料規模減小，同時增加查詢操作條數，加大随機查詢點對的覆寫率。

在自我線下檢查後，三次作業中均未出現公測和互測BUG。

規格和測試總結

  • 撰寫JML語言時應當注意對參數的所有不同的pre-condition進行全覆寫，即所有的pre-con互斥，且并集應為全集。
  • JML對post-condition的描述不必要考慮實作，應該使用最簡單、最本質的描述。
  • 在實作功能後，首先利用單元測試架構，對規格中最大的normal_behavior進行幾個基礎功能測試。
  • 之後，應當根據撰寫的規格，對每一個方法 分支針對性地 對應開展單元測試。
    • 注意組合pre-con（既有參數的狀态、也有對象本身this的狀态）的情況
    • 注意組合post-con的情況，確定每個分支都進行了至少一次測試
  • 使用OpenJML可以提示JML的文法錯誤和可能的簡單錯誤（如溢出等），但不能指望其自動生成的測試資料和政策，還是應該手動根據規格構造樣例。
oop
上一篇: 2017年軟體工程基礎-個人項目作業
下一篇: 結對項目-數獨程式擴充

繼續閱讀