北航OO（2020）第三單元博客做業

時間  2020-05-20
標籤 北航 第三 單元 博客 简体版
原文   原文鏈接

北航OO（2020）第三單元博客做業

目錄

JML語言總結

理論基礎

JML是用於對Java程序進行規格化設計的一種表示語言，它使用JavaDoc註釋的方式來表示規格。JML以Java語法爲基礎並進行了必定的擴充。JML的語法分爲幾個層次，下面對JML Level 0的核心特性進行簡要的總結。html

規格變量的聲明

規格變量分爲靜態規格變量和實例規格變量兩種。以整型數組爲例，它們分別能夠聲明爲//@public static model non_null int []elements和//@public instance model non_null int []elements。java

經常使用表達式

表達式 含義
\result 非void類型的方法的返回值
\old(expr) 一個表達式expr在相應方法執行前的取值（聽從引用規則）
\not_assigned(x, y, ...) 括號中的變量是否在方法執行過程當中未被賦值
\not_modified(x, y, ...) 限制括號中的變量在方法執行期間的取值未發生變化
(\forall T x; R(x); P(x)) 全稱量詞，表示知足R(x)的x都知足P(x)
(\exists T x; R(x); P(x)) 存在量詞，表示存在知足R(x)的x知足P(x)
(\sum T x; R(x); expr) 對於知足R(x)的x，求expr的和
(\max T x; R(x); expr) 對於知足R(x)的x，求expr的最大值
(\min T x; R(x); expr) 對於知足R(x)的x，求expr的最小值
<==> 等價操做符
==> 蘊含操做符
\nothing 空集

方法規格

方法規格分爲正常行爲規格和異常行爲規格兩種，分別對應normal_behavior和exceptional_behavior。多個規格之間使用also鏈接。每種規格又可分爲前置條件、反作用範圍限定和後置條件，分別對應requires、assignable和ensures。多個子句之間爲合取關係。算法

對於純粹訪問性的方法，即不會對對象的狀態進行任何改變，也不須要提供輸入參數，這樣的方法無需描述前置條件，也不會有任何反作用，且執行必定會正常結束。對於這類方法，可使用簡單的（輕量級）方式來描述其規格，即便用pure關鍵詞。在方法規格中，前置條件能夠引用pure方法返回的結果。windows

對於異常行爲規格，咱們一般會使用signals或signals_only子句來拋出異常。signals子句的結構爲signals (***Exception e) expr;意思是當expr 爲true 時，方法會拋出括號中給出的相應異常e；signals_only子句的結構爲signals_only ***Exception;，意思是一旦進入此子句，就會拋出相應的異常。設計模式

類型規格

類型規格指針對Java程序中定義的數據類型所設計的限制規則，通常而言，就是指針對類或接口所設計的約束規則。課程中的重點是不變式invariant和狀態變化約束constraint。不變式invariant是要求在全部可見狀態下都必須知足的特性，而狀態變化約束constraint對對象狀態的變化進行約束。數組

應用工具鏈狀況

JML的工具鏈較不完善，且大都已很長時間沒有維護。經常使用的JML工具主要有OpenJML（對JML進行語法檢查、配合Solver進行簡單的靜態驗證、以及運行時驗證）、JMLUnitNG（自動化單元測試生成工具）和JMLUnit（相似前者）等。OpenJML有Eclipse插件版，使用體驗較好。可是沒有可用的IDEA插件是一個遺憾。架構

在http://www.eecs.ucf.edu/~leavens/JML//download.shtml這個頁面上，有更多JML相關工具的介紹。工具

OpenJML驗證狀況

因爲後兩次做業沒法經過OpenJML的語法檢查，下面以第一次做業爲例，演示OpenJML的驗證。單元測試

Parsing and Type-checking

本功能主要檢查JML規格的語法。測試

在IDEA的External Tools中，運行以下命令：java -jar openjml.jar -check "$FilePath$" -cp "$Classpath$" -sourcepath "$Sourcepath$" -encoding utf-8，便可進行JML的靜態語法檢查。-check參數指定檢查類型爲Parsing and Type-checking，-cp和-sourcepath命令用於指定Classpath和源文件目錄，-encoding參數用於指定文件編碼。

第一次做業的JML規格成功經過了該檢查，返回值爲0。

Extended Static Checking

本功能主要利用Solver對按照JML編寫的程序進行簡單的靜態檢查。

在IDEA的External Tools中，運行以下命令：java -jar openjml.jar -prover z3_4_7 -exec ".\Solvers-windows\z3-4.7.1.exe" -esc "$FilePath$" -cp "$Classpath$" -sourcepath "$Sourcepath$" -encoding utf-8，便可進行JML的靜態語法檢查。-prover參數用於指定Solver類型，-exec參數用於指定Solver可執行程序，-esc參數指定檢查類型爲Extended Static Checking。

在對MyPerson檢查的過程當中，觸發了36個警告，其中主要是The prover cannot establish an assertion，但這些警告彷佛並非因爲程序的錯誤，而是Solver沒法對程序進行充分的解析致使的；在對MyNetwork檢查的過程當中，觸發了100個警告，其中主要還是The prover cannot establish an assertion，且提示靜態檢查不支持對\not_assigned表達式進行檢查。因而可知，該功能對一些較爲複雜的程序的支持還十分欠缺。

下面展現部分MyPerson類的檢查結果：

.\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:82: 警告: The prover cannot establish an assertion (Postcondition: .\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:67: 注: ) in method compareTo
return name.compareTo(p2.getName());
^
.\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:67: 警告: Associated declaration: .\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:82: 注:
@ ensures \result == name.compareTo(p2.getName());
^
.\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:82: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: .\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:66: 注: ) in method compareTo
return name.compareTo(p2.getName());
^
.\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:66: 警告: Associated declaration: .\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:82: 注:
@ public normal_behavior
^
.\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:53: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: .\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:29: 注: ) in method equals
return id == person.getId();
^
.\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:29: 警告: Associated declaration: .\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:53: 注:
@ public normal_behavior
^
.\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:53: 警告: The prover cannot establish an assertion (Postcondition: .\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:32: 注: ) in method equals
return id == person.getId();
^
.\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:32: 警告: Associated declaration: .\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:53: 注:
@ ensures \result == (((Person) obj).getId() == id);
^
.\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:77: 警告: The prover cannot establish an assertion (Postcondition: .\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:62: 注: ) in method getAcquaintanceSum
return acquaintance.size();
^
.\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:62: 警告: Associated declaration: .\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:77: 注:
//@ ensures \result == acquaintance.length;
^
.\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:41: 警告: The prover cannot establish an assertion (Postcondition: .\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:25: 注: ) in method getAge
return age;
^
.\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:25: 警告: Associated declaration: .\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:41: 注:
//@ ensures \result == age;
^
.\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:36: 警告: The prover cannot establish an assertion (Postcondition: .\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:22: 注: ) in method getCharacter
return character;
^
.\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:22: 警告: Associated declaration: .\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:36: 注:
//@ ensures \result.equals(character);
^
.\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:26: 警告: The prover cannot establish an assertion (Postcondition: .\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:16: 注: ) in method getId
return id;
^
.\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:16: 警告: Associated declaration: .\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:26: 注:
//@ ensures \result == id;
^
.\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:31: 警告: The prover cannot establish an assertion (Postcondition: .\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:19: 注: ) in method getName
return name;
^
.\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:19: 警告: Associated declaration: .\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:31: 注:
//@ ensures \result.equals(name);
^
.\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:67: 警告: The prover cannot establish an assertion (Postcondition: .\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:43: 注: ) in method isLinked
return id == person.getId() || acquaintance.containsKey(person);
^
.\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:43: 警告: Associated declaration: .\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:67: 注:
@ ensures \result == (\exists int i; 0 <= i && i < acquaintance.length;
^
.\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:67: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: .\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:41: 注: ) in method isLinked
return id == person.getId() || acquaintance.containsKey(person);
^
.\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:41: 警告: Associated declaration: .\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:67: 注:
/@ public normal_behavior
^
.\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:72: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: .\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:55: 注: ) in method queryValue
return acquaintance.getOrDefault(person, 0);
^
.\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:55: 警告: Associated declaration: .\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:72: 注:
@ public normal_behavior
^
.\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:72: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: .\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:48: 注: ) in method queryValue
return acquaintance.getOrDefault(person, 0);
^
.\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:48: 警告: Associated declaration: .\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:72: 注:
/@ public normal_behavior
^
.\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:72: 警告: The prover cannot establish an assertion (Postcondition: .\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:58: 注: ) in method queryValue
return acquaintance.getOrDefault(person, 0);
^
.\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:58: 警告: Associated declaration: .\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:72: 注:
@ ensures \result == 0;
^
.\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:72: 警告: The prover cannot establish an assertion (Postcondition: .\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:52: 注: ) in method queryValue
return acquaintance.getOrDefault(person, 0);
^
.\Unit3Homework1\src\com\oocourse\spec1\main\Person.java:52: 警告: Associated declaration: .\Unit3Homework1\src\com\oocourse\implements1\MyPerson.java:72: 注:
@ ensures (\exists int i; 0 <= i && i < acquaintance.length;
^

Runtime Assertion Checking

本功能主要對按照JML編寫的程序進行簡單的運行時檢查。

在IDEA的External Tools中，運行以下命令：java -jar openjml.jar -rac "$FilePath$" -cp "$Classpath$" -sourcepath "$Sourcepath$" -encoding utf-8，便可進行JML程序的運行時檢查。-rac參數指定檢查類型爲Runtime Assertion Checking。

OpenJML在對MyPerson檢查的過程當中觸發了Internal JML bug，並拋出了NullPointerException；在對MyNetwork檢查的過程當中報錯：An internal JML error occurred。因而可知，該功能還不甚完善。

JMLUnitNG測試（針對MyGroup類）

首先將OpenJML中的jmlruntime.jar複製到環境變量CLASSPATH所在的目錄下，而後，在項目目錄下，運行以下命令：java -jar jmlunitng-1_4.jar -d .\test .\src便可生成測試類。

對於MyGroup類的測試，能夠直接運行MyGroup_JML_Test類中的main方法，獲得結果以下：

[TestNG] Running:
Command line suite

Failed: racEnabled()
Passed: constructor MyGroup(-2147483648)
Passed: constructor MyGroup(0)
Passed: constructor MyGroup(2147483647)
Failed: <com.oocourse.implements3.MyGroup@8000001f>.addPerson(null)
Failed: <com.oocourse.implements3.MyGroup@1f>.addPerson(null)
Failed: <com.oocourse.implements3.MyGroup@8000001e>.addPerson(null)
Passed: <com.oocourse.implements3.MyGroup@8000001f>.addRelation(-2147483648)
Passed: <com.oocourse.implements3.MyGroup@1f>.addRelation(-2147483648)
Passed: <com.oocourse.implements3.MyGroup@8000001e>.addRelation(-2147483648)
Passed: <com.oocourse.implements3.MyGroup@8000001f>.addRelation(0)
Passed: <com.oocourse.implements3.MyGroup@1f>.addRelation(0)
Passed: <com.oocourse.implements3.MyGroup@8000001e>.addRelation(0)
Passed: <com.oocourse.implements3.MyGroup@8000001f>.addRelation(2147483647)
Passed: <com.oocourse.implements3.MyGroup@1f>.addRelation(2147483647)
Passed: <com.oocourse.implements3.MyGroup@8000001e>.addRelation(2147483647)
Failed: <com.oocourse.implements3.MyGroup@8000001f>.delPerson(null)
Failed: <com.oocourse.implements3.MyGroup@1f>.delPerson(null)
Failed: <com.oocourse.implements3.MyGroup@8000001e>.delPerson(null)
Passed: <com.oocourse.implements3.MyGroup@8000001f>.equals(null)
Passed: <com.oocourse.implements3.MyGroup@1f>.equals(null)
Passed: <com.oocourse.implements3.MyGroup@8000001e>.equals(null)
Passed: <com.oocourse.implements3.MyGroup@8000001f>.equals(java.lang.Object@61baa894)
Passed: <com.oocourse.implements3.MyGroup@1f>.equals(java.lang.Object@b065c63)
Passed: <com.oocourse.implements3.MyGroup@8000001e>.equals(java.lang.Object@768debd)
Passed: <com.oocourse.implements3.MyGroup@8000001f>.getAgeMean()
Passed: <com.oocourse.implements3.MyGroup@1f>.getAgeMean()
Passed: <com.oocourse.implements3.MyGroup@8000001e>.getAgeMean()
Passed: <com.oocourse.implements3.MyGroup@8000001f>.getAgeVar()
Passed: <com.oocourse.implements3.MyGroup@1f>.getAgeVar()
Passed: <com.oocourse.implements3.MyGroup@8000001e>.getAgeVar()
Passed: <com.oocourse.implements3.MyGroup@8000001f>.getConflictSum()
Passed: <com.oocourse.implements3.MyGroup@1f>.getConflictSum()
Passed: <com.oocourse.implements3.MyGroup@8000001e>.getConflictSum()
Passed: <com.oocourse.implements3.MyGroup@8000001f>.getId()
Passed: <com.oocourse.implements3.MyGroup@1f>.getId()
Passed: <com.oocourse.implements3.MyGroup@8000001e>.getId()
Passed: <com.oocourse.implements3.MyGroup@8000001f>.getPeopleSum()
Passed: <com.oocourse.implements3.MyGroup@1f>.getPeopleSum()
Passed: <com.oocourse.implements3.MyGroup@8000001e>.getPeopleSum()
Passed: <com.oocourse.implements3.MyGroup@8000001f>.getRelationSum()
Passed: <com.oocourse.implements3.MyGroup@1f>.getRelationSum()
Passed: <com.oocourse.implements3.MyGroup@8000001e>.getRelationSum()
Passed: <com.oocourse.implements3.MyGroup@8000001f>.getValueSum()
Passed: <com.oocourse.implements3.MyGroup@1f>.getValueSum()
Passed: <com.oocourse.implements3.MyGroup@8000001e>.getValueSum()
Passed: <com.oocourse.implements3.MyGroup@8000001f>.hasPerson(null)
Passed: <com.oocourse.implements3.MyGroup@1f>.hasPerson(null)
Passed: <com.oocourse.implements3.MyGroup@8000001e>.hasPerson(null)
Passed: <com.oocourse.implements3.MyGroup@8000001f>.hashCode()
Passed: <com.oocourse.implements3.MyGroup@1f>.hashCode()
Passed: <com.oocourse.implements3.MyGroup@8000001e>.hashCode()

===============================================
Command line suite
Total tests run: 52, Failures: 7, Skips: 0

===============================================

Process finished with exit code 0

能夠看出，JMLUnitNG主要針對邊界數據和空引用進行了測試。在上面的測試中，主要因爲方法傳入null而失敗。而因爲本單元做業中，方法不會傳入null，所以在代碼中未進行處理。

做業架構分析

在本單元的做業中，我主要依據JML進行構建，同時採起一些實現上的優化，如應用容器和算法等。在本單元，我沒有進行過多的抽象，僅僅是編寫了Pair和SegmentTree工具類，並在MyNetwork類中編寫了Dijkstra和PointBiconnectedComponent內部類進行算法的封裝。我認爲若能將Graph類和Node類抽象出來，並使MyNetwork類和MyPerson類對其分別進行繼承或組合，或許能夠收到更好的效果。

下面是本單元第三次做業的UML類圖（略去了官方包）：

做業Bug狀況

本單元做業未在公測和互測中出現任何bug。

在第二次做業中，我在本地測試時發現Group中的getAgeVar方法在使用方差公式簡化計算時，若將括號中的項提取出來，可能會致使偏差，以下：

public int getAgeVar() {
    if (people.isEmpty()) {
        return 0;
    }
    return (ageSquaredSum - 2 * getAgeMean() * ageSum) / people.size()
            + getAgeMean() * getAgeMean();
}

須要改爲以下寫法：

public int getAgeVar() {
    if (people.isEmpty()) {
        return 0;
    }
    return (ageSquaredSum - 2 * getAgeMean() * ageSum
            + getAgeMean() * getAgeMean() * people.size()) / people.size();
}

經驗證，緣由是Java整數除法在取整時，採起向0取整的方式，而前面寫法的括號中可能會出現負數，致使舍入錯誤，而與正確結果差1。

心得體會：規格撰寫與理解

在本單元，我接觸了一種全新的程序設計模式：規格化設計。規格化設計可以使得設計與實現分離，同時，形式化的規格也便於進行嚴格的形式化驗證。

在撰寫規格時，咱們會更多地從需求而非實現的角度去思考程序的設計。此外，規格的前置條件會促使咱們考慮各類邊界條件與極端數據，必定程度上緩解了因爲前置條件考慮不周而致使程序出現Bug的現象。

在理解規格時，重點是對規格行爲的理解。一般狀況下，規格描述並不適合直接做爲代碼實現。所以，咱們須要對規格所描述的行爲進行理解，並由此選擇合適的實現。咱們甚至還能夠在規格的基礎上進一步抽象，設計出更加清晰合理的程序架構。

雖然如此嚴格而繁瑣的形式化規格表述在平常軟件的開發領域並不常見，但我相信，因爲其能夠進行嚴格的形式化驗證，形式化的規格在高可靠性領域必定大有用武之地。

相關文章
相關標籤/搜索
每日一句
    每一个你不满意的现在，都有一个你没有努力的曾经。
本站公眾號
   歡迎關注本站公眾號,獲取更多信息
聯繫我們 最近搜索 最新文章 沪ICP备13005482号-10 MyBatis教程 SQL 教程 MySQL教程 Java 教程 Thymeleaf 教程 Hibernate教程 Spring教程 Redis教程