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是一門值得了解和學習的技術。