天天看點
傳回

OOJML系列總結

目錄

  • 0x0 JML理論相關
    • 0.0 概念及作用
    • 0.1 JML文法學習
  • 0x1 使用openJml以及JMLUnitNG
    • 1.0 使用openjml
    • 1.1使用JMLUnitNG
  • 0x2 作業架構設計與分析
    • 2.0 第一次作業
    • 2.1 第二次作業
    • 2.2 第三次作業
  • 0x3bug分析與測試
    • 3.0 bug分析
    • 3.1 Junit4測試
    • 3.2 python對拍
  • 0x4 感想

  • JML(Java Modeling Language)是用于對Java程式進行規格化設計的一種表示語言。
  • JML為嚴格的程式設計提供了一套行之有效的方法。通過JML及其支援工具（openJML與SMT Solver、JMLUnitNG等），不僅可以基于規格自動構造測試用例，還可以以靜态方式來檢查代碼實作對規格的滿足情況。
  • 邏輯化規約代碼實作人員與調用者，同時提高代碼的可維護性與複用性。

僅列舉作業中常出現的

  • 注釋結構：塊注釋的方式為 /* @ annotation @*/，類似于Javadoc
  • 量化表達式：
    • \forall表達式：全稱量詞修飾的表達式，表示對于給定範圍内的元素，每個元素都滿足相應的限制。 (\forall int i,j; 0 <= i && i < j && j < 10; a[i] < a[j]) ，意思是針對任意 0<=i<j<10，a[i]<a[j] 。
    • \exists表達式：存在量詞修飾的表達式，表示對于給定範圍内的元素，存在某個元素滿足相應的限制。 (\exists int i; 0 <= i && i < 10; a[i] < 0) ，表示針對0<=i<10，至少存在一個a[i]<0。
    • \sum表達式：傳回給定範圍内的表達式的和。 (\sum int i; 0 <= i && i < 5; i) ，這個表達式的意思計算[0,5)範圍内的整數

      i

       的和，即0+1+2+3+4==10。
    • \max表達式：顧名思義，傳回給定範圍内的表達式的最大值。
    • \min表達式：顧名思義，傳回給定範圍内的表達式的最小值。
    原子表達式：
    • \result表達式：表示一個非 void 類型的方法執行所獲得的結果，即方法執行後的傳回值。
    • \old( expr )表達式：用來表示一個表達式 expr 在相應方法執行前的取值。

      • warning

         ：針對一個對象引用而言，隻能判斷引用本身是否發生變化，而不能判斷引用所指向的對象實體内容是否發生變化。注意區分v.size() 、\old(v). size() 和\old(v.size())。
    • 等等
    方法規格：
    • 前置條件(pre-condition)：requires：例如

      requires P1||P2;

    • 後置條件(post-condition)：ensures：例如

      ensures P1||P2;
    • 副作用範圍限定(side-effects)：JML提供了副作用限制子句，使用關鍵詞

      assignable

       或者

      modifiable

       。 
      • /*@
@ ...
@ assignable \nothing;
@ assignable \everything;
@ modifiable \nothing;
@ modifiable \everthing;
@ assignable elements;
@ modifiable elements;
@ assignable elements, max, min;
@ modifiable elements, max, min;
@*/

      • assignble

         表示可指派，而

        modifiable

         則表示可修改。

        \nothing

         和

        \everthing

         等表示作用域。
    區分方法的正常功能行為和異常行為：

    • public normal_behavior

       表示接下來對方法的正常功能給出規格。
    • 關鍵詞

      also

       ，它的意思是還有其他正常功能或異常功能。

    • public exceptional_behavior

       表示接下來對方法的異常功能給出規格。
      • signals子句用來聲明将會抛出的異常：
        • 結構為 signals (Exception e) expr ，意思是當 expr 為 true 時，方法會抛出括号中給出的相應異常e。

    不變式invariant

    狀态變化限制constraint

JML工具鍊在這

warning：路徑不能含有中文，血的教訓，浪費了很多時間

openjml下載下傳位址在這

環境：Windows，使用z3-4.7.1，jdk-8u251-windows-x64.exe

使用的指令：

*靜态檢查*：java -jar .\openjml.jar -exec (SMT Solvers的路徑) .\Solvers-windows\z3-4.7.1.exe -esc -dir (項目目錄)

針對本單元第三次作業的效果：貌似zyy帶師的JML有些許問題？咱也不知道

OOJML系列總結

JMLUnitNG1.4下載下傳位址在這

環境同上

java -jar .\jmlunitng-1_4.jar *.java
javac -cp .\jmlunitng-1_4.jar *.java
java -cp .\jmlunitng-1_4.jar myitem.MyGroup_JML_Test

針對本單元第三次作業的MyGroup的使用效果：

OOJML系列總結

評價：

學長誠不欺我，JMLUnitNG果然雞肋，可以看到就是針對
  • 以對象為參數的方法傳諸如

    null
  • 以整數為參數的方法傳INT_MAX或INT_MIN
  • 無參數的直接調用

測試力度僅此而已，相較之下自己寫的JUnit覆寫性都要高得多，更無法相比黑盒測試了。

另外，注意到

Failures

 都是出在不符合正常行為規格的傳參上，是以也無關緊要

本單元作業不涉及重構，隻有加構。

實作起來有難度或有坑的方法：

isCircle

isLinked

isCircle

直接使用BFS，小政策：每次

isCircle

都會記錄結果，隻要沒有

addRelation

下次也可以使用。

isLinked

要注意自己和自己也是傳回

true

難度較低，自主測試、公測、互測均無bug，互測對同屋同學無差别轟炸無果，遂放棄

Group内部的諸如relationSum/ValueSum的查詢方法

進行複雜度分析後認為無腦照着規格填代碼有ctle風險，是以着重考慮盡量避免循環

采取政策思想：hashmap O(1)查詢 + 操作離散化 + 資料破壞分析與維護

在此僅拿

conflictSum

舉例，隻有

atg

指令才有可能破壞資料，是以在

MyGroup

的addPerson中每次都進行更新操作即可

public class MyGroup implements Group {
		//...

	    @Override
    	public void addPerson(Person person) {
        	//...
        	conflictSum = conflictSum.xor(person.getCharacter());
        	//...
   	 	}

 		@Override
    	public BigInteger getConflictSum() {
        	return conflictSum;
    	}
    	
    	//...
}

addPerson可以做很多文章，最大化避免循環

值得一提的是：getAgeVar()方法可以使用概統的方差公式進行維護，不過要注意與規格精度相同。

實作起來有難度的方法：quaryStronglinked，blockSum，quaryMinPath等。

第三次作業考慮到blockSum實際上是求連通塊數量：

  • 一個思路是維護互相之間有關系的人的集合，這樣子ap和ar就是将人加入集合以及集合合并的操作，有幾個集合就有幾個block，解決了blocksum；同時，isCircle就是看二者在不在一個set。
  • 另一個思路就是并查集，第一個進入集合的人就是整個集合的boss（初始化每個人都是自己的boss），每次ar就對雙方進行判定，看誰是誰的boss，使得關系層次變低，提高效率(路徑壓縮)，isCircle就是對兩個人進行最高層boss查找（找整個集合的boss相當于樹的祖先節點）同時路徑壓縮，這樣子blocksum也就是看people中自己是自己的boss的情況的個數。

最終采用

qsl:Tarjan + qmp:迪傑斯特拉算法與堆優化 + isCircle AND qbs:并查集

等等算法，分别用邊權内部類

PersonAndLength

以及邊邊内部類

Edge

開展

Tarjan算法

dijkstra

算法。充分的測試帶來的也就是理所應當的公測、互測無bug。

附上第三次作業UML類圖

OOJML系列總結

不足：network太過臃腫，内含兩個内部類，邊權相關，應該與圖論算法封裝成一個圖類，便于管理，同時優化架構，降低耦合。

前兩次作業難度較低，自主測試、公測、互測均未發現bug

第三次作業對于性能方面要求不容小觑，自主測試時發現qsl所使用的Tarjan算法結束判定有問題，導緻未搜尋完全便結束，另外極端測試用例也暴露出性能上的危險。

發現同屋bug分析：

  • 第二次作業hack了一個WR，無外乎規格看漏了或者了解不到位。
  • 第三次作業hack了一個除零，在組内删除人更新方差的時候沒有考慮人數為0的情況。

針對

MyNetwork

的每個方法的JML描述情況進行覆寫性測試，以期基本功能的完善，複雜邏輯還須靠對拍

下面附上了第一次作業的Junit代碼，有針對性的覆寫了

isCircle

isLinked

兩個容易出錯的方法

package test.java.MyItem;

import com.oocourse.spec1.exceptions.EqualPersonIdException;
import com.oocourse.spec1.exceptions.EqualRelationException;
import com.oocourse.spec1.exceptions.PersonIdNotFoundException;
import com.oocourse.spec1.exceptions.RelationNotFoundException;
import myitem.MyNetwork;
import myitem.MyPerson;
import org.junit.BeforeClass;
import org.junit.Test;

import static org.junit.Assert.*;

import org.junit.After;

import java.math.BigInteger;

/**
 * MyNetwork Tester.
 *
 * @author <Authors name>
 * @version 1.0
 * @since <pre>4月 25, 2020</pre>
 */
public class MyNetworkTest {
    private static MyPerson person1 = new MyPerson(1, "a", BigInteger.ONE, 1);
    private static MyPerson person2 = new MyPerson(2, "b", new BigInteger("12345678901234456"), 2);
    private static MyPerson person3 = new MyPerson(3, "c", BigInteger.ZERO, 10);
    private static MyPerson person4 = new MyPerson(100, "ab", BigInteger.TEN, 100);
    private static MyPerson person5 = new MyPerson(5, "c", BigInteger.ZERO, 10);
    private static MyNetwork network = new MyNetwork();

    @BeforeClass
    public static void before() throws Exception {
        network.addPerson(person1);
        network.addPerson(person2);
        network.addPerson(person3);
        network.addPerson(person4);
        network.addPerson(person5);
    }

    @After
    public void after() throws Exception {
    }

    /**
     * Method: contains(int id)
     */
    @Test
    public void testContains() throws Exception {
//TODO: Test goes here...
        assertTrue(network.contains(1));
        assertTrue(network.contains(2));
        assertTrue(network.contains(3));
        assertTrue(network.contains(100));
        assertTrue(network.contains(5));

        assertFalse(network.contains(4));
        assertFalse(network.contains(-1));
    }

    /**
     * Method: getPerson(int id)
     */
    @Test
    public void testGetPerson() throws Exception {
//TODO: Test goes here...
        assertEquals(person1, network.getPerson(1));
        assertEquals(person2, network.getPerson(2));
        assertEquals(person3, network.getPerson(3));
        assertEquals(person4, network.getPerson(100));
        assertEquals(person5, network.getPerson(5));

        assertNotEquals(person1, network.getPerson(4));
        assertNotEquals(person1, network.getPerson(-1));
    }

    /**
     * Method: addPerson(Person person)
     */
    @Test
    public void testAddPerson() {
//TODO: Test goes here...
        try {
            network.addPerson(person1);
            network.addPerson(new MyPerson(6, "ls", new BigInteger("10000"), 20));

            assertTrue(network.contains(6));
        } catch (EqualPersonIdException e) {
            e.print();
        }
    }

    /**
     * Method: addCircle(int id1, int id2)
     */
    @Test
    public void testAddCircle() throws Exception {
//TODO: Test goes here... 
    }

    /**
     * Method: addRelation(int id1, int id2, int value)
     */
    @Test
    public void testAddRelation() throws Exception {
//TODO: Test goes here...
        network.addRelation(1, 1, 100);
        try {
            network.addRelation(1, 2, 100);
        } catch (EqualRelationException e) {
            e.print();
        }
        assertTrue(person1.isLinked(person2));
        assertTrue(person2.isLinked(person1));
        assertTrue(person1.isLinked(person1));
        assertTrue(person2.isLinked(person2));
        try {
            network.addRelation(-1, -1, 100);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
        try {
            network.addRelation(1, -1, 100);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
        try {
            network.addRelation(-1, 1, 100);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
        try {
            network.addRelation(1, 2, 100);
        } catch (EqualRelationException e) {
            e.print();
        }
    }

    /**
     * Method: queryValue(int id1, int id2)
     */
    @Test
    public void testQueryValue() throws Exception {
//TODO: Test goes here...
        try {
            network.queryValue(-1, 1);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
        try {
            network.queryValue(2, 1);
        } catch (RelationNotFoundException e) {
            e.print();
        }
    }

    /**
     * Method: queryConflict(int id1, int id2)
     */
    @Test
    public void testQueryConflict() throws Exception {
//TODO: Test goes here...
        assertEquals(person1.getCharacter().xor(person2.getCharacter()), network.queryConflict(1, 2));
        try {
            network.queryConflict(-1, 1);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
    }

    /**
     * Method: queryAcquaintanceSum(int id)
     */
    @Test
    public void testQueryAcquaintanceSum() throws Exception {
//TODO: Test goes here...
        assertEquals(person1.getAcquaintanceSum(), network.queryAcquaintanceSum(1));
        try {
            network.queryAcquaintanceSum(-1);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
    }

    /**
     * Method: compareAge(int id1, int id2)
     */
    @Test
    public void testCompareAge() throws Exception {
//TODO: Test goes here...
        assertEquals(person1.getAge() - person2.getAge(), network.compareAge(1, 2));
        try {
            network.compareName(1, -1);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
    }

    /**
     * Method: compareName(int id1, int id2)
     */
    @Test
    public void testCompareName() throws Exception {
//TODO: Test goes here...
        assertEquals(person1.getName().compareTo(person2.getName()), network.compareName(1, 2));
        try {
            network.compareName(1, -1);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
    }

    /**
     * Method: queryPeopleSum()
     */
    @Test
    public void testQueryPeopleSum() throws Exception {
//TODO: Test goes here...
        assertEquals(6, network.queryPeopleSum());
    }

    /**
     * Method: queryNameRank(int id)
     */
    @Test
    public void testQueryNameRank() throws Exception {
//TODO: Test goes here...
        assertEquals(1, network.queryNameRank(1));
        assertEquals(2, network.queryNameRank(100));
        assertEquals(3, network.queryNameRank(2));
        assertEquals(4, network.queryNameRank(3));
        assertEquals(4, network.queryNameRank(5));
        try {
            network.addPerson(new MyPerson(6, "ls", new BigInteger("10000"), 20));
        } catch (EqualPersonIdException e) {
            e.print();
        }


        assertTrue(network.contains(6));
        assertEquals(6, network.queryNameRank(6));
    }

    /**
     * Method: isCircle(int id1, int id2)
     */
    @Test
    public void testIsCircle() throws Exception {
//TODO: Test goes here...
        network.addRelation(1, 2, 10);
        network.addRelation(2, 3, 10);
        network.addRelation(3, 5, 10);
        network.addRelation(5, 100, 10);
        try {
            network.addPerson(new MyPerson(6, "ls", BigInteger.ZERO, 20));
        } catch (EqualPersonIdException e) {
            e.print();
        }

        assertTrue(network.isCircle(1, 1));
        assertTrue(network.isCircle(100, 100));
        assertTrue(network.isCircle(5, 5));
        assertTrue(network.isCircle(3, 3));
        assertTrue(network.isCircle(2, 2));

        assertTrue(network.isCircle(1, 2));
        assertTrue(network.isCircle(1, 2));
        assertTrue(network.isCircle(100, 2));
        assertTrue(network.isCircle(5, 3));
        assertTrue(network.isCircle(100, 5));
        assertTrue(network.isCircle(1, 100));
        assertFalse(network.isCircle(1, 6));

        try {
            network.isCircle(1, -1);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
        try {
            network.isCircle(-1, -1);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }
        try {
            network.isCircle(-1, 1);
        } catch (PersonIdNotFoundException e) {
            e.print();
        }

    }


}

對拍是真的好使用，拉上幾個hxd，xdm一起多人運動，發現bug效率倍增。

在此附上目錄與效果，check為簡單字元串比對，normal_data為規模可調全随機資料，extreme為精心構造的極端資料

OOJML系列總結
OOJML系列總結
OOJML系列總結

本單元體驗依舊極佳

終于有一單元bugClear六根清淨

第三單元主要是按照規格實作接口，認真閱讀JML十分重要，不能放過任何一個細節，另外，還要要結合課程組給出的資料範圍以及标程複雜度從全局出發考量方法實作的複雜度。

此單元疊代開發較容易，原因是大架構課程組已經給出，但是，還是要從全局方面設計算法架構，以帶來更好的實作體驗以及更優的算法複雜度，此次作業除了給定的幾個接口，其他的類都可以為所欲為，可以選擇将算法獨立出來為一個類，提供相應方法供network調用，如此一來，便于換算法，可擴充性提高了。

照例還是要誇一波課程組的，如此好的課程體驗最大的功臣就是我們的老師和助教大大！！

希望OO越來越好！！

上一篇: [LeetCode] 94. Binary Tree Inorder Traversal 二叉樹的中序周遊
下一篇: Java代碼度量分析工具：DesigniteJava簡介