OO第三單元總結

JML語言理論基礎梳理及工具鏈

註釋結構

JML以javadoc註釋的方式來表示規格，每行都以@起頭。

• 行註釋：//@annotation
• 塊註釋：/* @ annotation @*/

JML表達式

JML的表達式是對Java表達式的擴展，新增了一些操作符和原子表達式。

• 原子表達式
  • \result表達式：表示一個非 void 類型的方法執行所獲得的結果，即方法執行後的返回值。\result表達式的類型就是方法聲明中定義的返回值類型。
  • \old(expr)表達式：用來表示一個表達式expr在相應方法執行前的取值。針對一個對象引用而言，只能判斷引用本身是否發生變化，而不能判斷引用所指向的對象實體內容是否發生變化。
  • \not_assigned(x, y, ...)表達式：用來表示括弧中的變數是否在方法執行過程中被賦值。如果沒有被賦值，返回為true，否則返回false。
  • \not_modified(x, y, ...)表達式：該表達式限制括弧中的變數在方法執行期間的取
    值未發生變化。
  • \nonnullelements(container)表達式：表示container對象中存儲的對象不會有 null。
  • \type(type)表達式：返回類型type對應的類型(Class)。
  • \typeof(expr)表達式：該表達式返回expr對應的準確類型。
• 量化表達式
  • \forall表達式：全稱量詞修飾的表達式，表示對於給定範圍內的元素，每個元素都滿足相應的約束。
  • \exists表達式：存在量詞修飾的表達式，表示對於給定範圍內的元素，存在某個元素滿足相應的約束。
  • \sum表達式：返回給定範圍內的表達式的和。
  • \product表達式：返回給定範圍內的表達式的連乘結果。
  • \max表達式：返回給定範圍內的表達式的最大值。
  • \min表達式：返回給定範圍內的表達式的最小值。
  • \num_of表達式：返回指定變數中滿足相應條件的取值個數。
• 集合表達式：可以在JML規格中構造一個局部的集合(容器)，明確集合中可以包含的元素。
• 操作符
  • 子類型關係操作符：E1<：E2，如果類型E1是類型E2的子類型(sub type)，則該表達式的結果為真，否則為假。如果E1和E2是相同的類型，該表達式的結果也為真。
  • 等價關係操作符：b_expr1<==>b_expr2或者b_expr1<=!=>b_expr2，其中b_expr1和b_expr2都是布爾表達式，這兩個表達式的意思是b_expr1==b_expr2或者b_expr1!=b_expr2。
  • 推理操作符：b_expr1==>b_expr2或者b_expr2<==b_expr1。對於表達式b_expr1==>b_expr2而言，當b_expr1==false，或者b_expr1==true且b_expr2==true時，整個表達式的值為true。
  • 變數引用操作符
    • \nothing指示一個空集。
    • \everything指示一個全集。

方法規格

• 前置條件(pre-condition)：是對方法輸入參數的限制，通過requires子句來表示。
• 後置條件(post-condition)：是對方法執行結果的限制，通過ensures子句來表示。
• 副作用範圍限定(side-effects)
  • assignble表示可賦值。
  • modifiable則表示可修改。
• signals子句
  • signals (Exception e) b_expr：當b_expr為true時，方法會拋出括弧中給出
    的相應異常e。
  • signals_only：後面跟著一個異常類型，不強調對象狀態條件，強調滿足前置條件時拋出相應的異常。

類型規格

• 不變式(invariant)：要求在所有可見狀態下都必須滿足的特性，語法上定義invariant P，其中invariant為關鍵詞， P 為謂詞。
• 狀態變化約束(constraint)：對前序可見狀態和當前可見狀態的關係進行約束。

工具鏈

• OpenJML
• SMTSolver
• JMLUnitNG

部署JMLUnitNG自動生成測試用例

一開始想對Path中的一些簡單方法進行測試，但是報了很奇怪的錯誤，也不懂如何解決，遂放棄。

於是我手寫了一個簡單的測試程式Test.java，其功能是非負數的加法，且未對溢出情況做處理。

package test;

public class Test {
    //@ public normal_behavior
    //@ requires a >= 0 && b >= 0;
    //@ ensures \result == a + b;
    public static int sum(int a, int b) {
        return a + b;
    }

    public static void main(String[] args) {
        sum(1, 2);
    }
}

初始目錄結構如下：

test
└── Test.java

執行java -jar jmlunitng.jar test/Test.java

test
├── PackageStrategy_int.java
├── PackageStrategy_java_lang_String.java
├── PackageStrategy_java_lang_String1DArray.java
├── Test.java
├── Test_InstanceStrategy.java
├── Test_JML_Data
│   ├── ClassStrategy_int.java
│   ├── ClassStrategy_java_lang_String.java
│   ├── ClassStrategy_java_lang_String1DArray.java
│   ├── main__String1DArray_args__10__args.java
│   ├── sum__int_a__int_b__0__a.java
│   └── sum__int_a__int_b__0__b.java
└── Test_JML_Test.java

執行javac -cp jmlunitng.jar test/*.java

test
├── PackageStrategy_int.class
├── PackageStrategy_int.java
├── PackageStrategy_java_lang_String.class
├── PackageStrategy_java_lang_String.java
├── PackageStrategy_java_lang_String1DArray.class
├── PackageStrategy_java_lang_String1DArray.java
├── Test.class
├── Test.java
├── Test_InstanceStrategy.class
├── Test_InstanceStrategy.java
├── Test_JML_Data
│   ├── ClassStrategy_int.class
│   ├── ClassStrategy_int.java
│   ├── ClassStrategy_java_lang_String.java
│   ├── ClassStrategy_java_lang_String1DArray.class
│   ├── ClassStrategy_java_lang_String1DArray.java
│   ├── main__String1DArray_args__10__args.class
│   ├── main__String1DArray_args__10__args.java
│   ├── sum__int_a__int_b__0__a.class
│   ├── sum__int_a__int_b__0__a.java
│   ├── sum__int_a__int_b__0__b.class
│   └── sum__int_a__int_b__0__b.java
├── Test_JML_Test.class
└── Test_JML_Test.java

執行java -jar openjml.jar -rac test/Test.java

執行java -cp jmlunitng.jar test.Test_JML_Test

測試結果：

[TestNG] Running:
  Command line suite

Passed: racEnabled()
Passed: constructor Test()
Passed: static main(null)
Failed: static sum(-2147483648, -2147483648)
Passed: static sum(0, -2147483648)
Passed: static sum(2147483647, -2147483648)
Passed: static sum(-2147483648, 0)
Passed: static sum(0, 0)
Passed: static sum(2147483647, 0)
Passed: static sum(-2147483648, 2147483647)
Passed: static sum(0, 2147483647)
Failed: static sum(2147483647, 2147483647)

===============================================
Command line suite
Total tests run: 12, Failures: 2, Skips: 0
===============================================

可以看到自動生成的測試用例採用的是極端數據的組合，對於負數以及溢出都顯示Failed表明未通過測試，這與我們的預期相符。

作業架構設計

第九次作業

第一次作業比較簡單，只有對路徑的增刪查改等基本功能，僅需實現Path和PathContainer兩個容器類再加上一個主類即可，實現的時候根據JML按部就班地寫就沒什麼問題。唯一要註意的一點是時間複雜度的問題，因為查詢指令很多，使用HashMap和HashSet是一個較好的選擇，能基本保證O(1)的複雜度。

第十次作業

從這次作業開始涉及到圖結構，增加了判斷容器中是否存在某個結點、容器中是否存在某一條邊、兩個結點是否連通以及計算兩個結點之間的最短路徑的方法。

對於結點我使用HashMap存儲，以結點Id為值，重覆個數為鍵。對於邊我採用的是嵌套的HashMap,由結點再映射到一個HashMap,內容是與它連接的結點及其重覆個數。這樣，就能把圖結構完整的保存下來，查詢效率高，同時也易於增刪維護。

對於連通性和最短路，我採用了bfs，遍歷的過程中會用到一個WeightedNode類，用來保存源點到當前節點的最短路徑長度，並傳遞給下一個節點累加使用。此外，我還用ShortestPath類來描述已經算出的最短路，它包含兩個節點的信息，並重寫了equals()和hashCode()，從而可以保存在HashMap中作為最短路的緩存。值得一提的是，a -> b和b -> a的最短路是一樣的，在重寫以上兩個方法時要註意對稱性。

第十一次作業

本次作業需要實現一個動態的地鐵系統。從類圖中的繼承關係可以看出，這三次作業是一脈相承、逐次遞進的，模擬了實際OOP開發中一個功能模塊的演化過程。

在保留了上次作業的大體架構的基礎上，引入MultiNode來描述在不同路徑上具有相同Id的結點，這是因為我採用的是"拆點"的建圖方法，需要區分這些重覆的結點。此外，用Pair類代替並擴展了ShortestPath類，使其可以同時描述最短路路徑、最低票價、最少換乘次數、最少不滿意度多種兩點結構。演算法上採用Dijkstra演算法，在每次查詢時計算出源點到其所在連通塊的所有節點的最低票價/最少換乘次數/最少不滿意度，並存入緩存以便下次直接使用。至於最短路和連通塊，依然是用bfs進行計算。

本次作業主要有兩方面的不足：

1. "拆點"方法本身的缺陷：對於多重邊重點的情況，拆點會讓圖結構變得異常複雜，使得用Dijkstra演算法時時間複雜度急劇上升。
2. 程式架構不OO：代碼基本就是在上次作業的基礎上做累加，繼承、重用做的不夠好。此外，沒有將圖結構和演算法分離，程式耦合度較高。事實上，應該將圖的相關計算封裝成類，單獨進行維護。

BUG及修複情況

三次作業均用對拍進行測試。

第九次作業

可能是因為比較簡單，沒有被測出bug，也沒有測出別人的bug。

第十次作業

依然沒有測出或被測出bug。

第十一次作業

提交前就在擔心會不會因為拆點複雜度過高而超時，結果果然慘不忍睹，未通過的點都是因為TLE。目前正在bug修複階段，考慮換一種建圖的方法。

心得體會

本單元主要學習JML規格，具體來說包含兩方面的內容：根據需求撰寫規格，以及根據規格實現代碼。JML是基於"契約式編程"的一種規格描述語言，相比於自然語言註釋，JML更加嚴謹和清晰。只要能保證規格本身是滿足需求的，並且編程時嚴格按照規格實現，理論上就程式就一定是正確的。在這種情況下，即使出現了bug，也能通過OpenJML、JMLUnitNG等工具自動化地定位問題所在。

但JML也有美中不足的地方，比如學習成本高，讀起來沒有自然語言那麼易於理解。尤其是撰寫規格是一件極其費時費力的工作，其難度不亞於代碼實現本身。可能在工業界，尤其是那些不容許任何程式錯誤的場景下（如航空航天、軍事領域），使用JML是一種較好的易於溝通和協作的編程方式，且能在最大程度上避免錯誤的產生。但在小團隊的常規開發中，私以為自然語言會是相對更好的選擇。

然而無論如何，JML是一門值得瞭解和學習的技術。