面向對象OO第三單元總結

来源:https://www.cnblogs.com/vanellopeblog/archive/2019/05/22/OOUnit3.html
-Advertisement-
Play Games

第三單元OO總結博客 1 梳理JML語言的理論基礎、應用工具鏈情況 由於篇幅原因，這裡只梳理幾個在本單元常用的 註釋結構 行註釋://@annotation 塊註釋：/* @ annotation @*/ 例如：純粹查詢方法/*@ pure @ */，即方法的執行不會有任何副作用 JML表達式 原子 ...


第三單元OO總結博客

 

1 梳理JML語言的理論基礎、應用工具鏈情況

由於篇幅原因，這裡只梳理幾個在本單元常用的

註釋結構

  1. 行註釋://@annotation

  2. 塊註釋：/* @ annotation @*/

    例如：純粹查詢方法/*@ pure @ */，即方法的執行不會有任何副作用

 

JML表達式

原子表達式

  • \result：表示一個非 void 類型的方法執行所獲得的結果，即方法執行後的返回值

  • \old(expr): 用來表示一個表達式 expr 在相應方法執行前的取值。作為一般規則，任何情況下，都應該使用\old把關心的表達式取值整體括起來。

量化表達式

  • \forall：全稱量詞修飾的表達式，表示對於給定範圍內的元素，每個元素都滿足相應的約束。

    作業中的例子：

    1 (\forall int i; 0 <= i && (i < npath.length - 1); containsEdge(npath[i], npath[i + 1])));

    保證isConnected 的前提之一是，這兩個點之間有連續的邊將他們相連（否則不通）

  • \exist：存在量詞修飾的表達式，表示對於給定範圍內的元素，存在某個元素滿足相應的約束

    作業中的例子：

    1 requires (\exists Path path; path.isValid() && containsPath(path); path.containsNode(fromNodeId)) &&
2          (\exists Path path; path.isValid() && containsPath(path); path.containsNode(toNodeId));

    保證isConnected 的前提之一，要存在某個Path，這個Path上包含這個點（否則就Not Found Exception）

     

操作符

  • 子類型關係操作符: E1<:E2

  • 等價關係操作符: 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指示一個空集:

      例如：assignable \nothing表示當前作用域下每個變數都不可以在方法執行過程中被賦值

    • \everything指示一個全集

方法規格

正常行為規格normal_behavior

前置條件

  • 通過requires子句來表示

    • 例如增加一條路徑的前提條件：增加的這條路徑必須合法有效

      1 requires path != null && path.isValid();
後置條件

  • 通過ensures子句來表示

    • getPathId必須確保返回的ID確實屬於當前存在的路徑

    • 1 ensures (\exists int i; 0 <= i && i < pList.length; pList[i].equals(path) && pidList[i] == \result);
副作用

  • 使用關鍵詞 assignable 或者 modifiable，這個函數要改什麼變數，就在後面加那個變數的名字

    • 例如addPath

       1  /*@ normal_behavior
 2       @ requires path != null && path.isValid();
 3       @ assignable pList, pidList; 需要修改這兩個List
 4       省略一部分
 5       @ also
 6         省略一部分
 7       @ assignable \nothing; 如果Path不合法，那麼返回0，沒有需要修改的東西
 8       @ ensures \result == 0;
 9       @*/
10     public int addPath(Path path);

       

       

異常行為規格expcetional_behavior

  • also: 有兩種場景使用

    1. 除了正常功能規格外，還有一個異常功能規格，需要使用also來分隔。

    2. 父類中對相應方法定義了規格，子類重寫了該方法，需要補充規格，這時應該在補充的規格之前使用also;

     

  • signals子句

    • 結構為signals (***Exception e) b_expr，意思是當b_expr為true時，方法會拋出括弧中給出 的相應異常e。

      例子：

       1 /*@ public normal_behavior
 2      省略
 3       @ also 下麵是異常行為
 4       @ public exceptional_behavior 
 5       @ assignable \nothing;
 6       @ signals (PathNotFoundException e) path == null;
 7       @ signals (PathNotFoundException e) path.isValid() == false;
 8       @ signals (PathNotFoundException e) !containsPath(path);
 9       @*/
10     public int removePath(Path path) throws PathNotFoundException;

      • 當 path == null條件成立，拋出異常

      • 當 path.isValid條件成立，拋出異常

      • 當容器內不含 path，拋出異常

 

線上OpenJML鏈接

 

2 部署SMT Solver，至少選擇3個主要方法來嘗試進行驗證，報告結果

跳過

 

3 部署JMLUnitNG/JMLUnit，針對Graph介面的實現自動生成測試用例， 並結合規格對生成的測試用例和數據進行簡要分析

生成數據

我研究了好久貌似OpenJML對MacOS不是很友好……好像也沒有搞清楚TestNG怎麼生成測試樣例

寫了一個python程式來生成測試指令

 1 import random
 2 SEQUENCE = 0;
 3 ID = 1;
 4 DOUBLE_ID = 2;
 5 NONE = 3;
 6 ID_NODE = 4;
 7 queries = [("PATH_ADD", SEQUENCE),
 8            ("PATH_REMOVE", SEQUENCE),
 9            ("PATH_REMOVE_BY_ID", ID),
10            ("PATH_GET_ID", SEQUENCE),
11            ("PATH_GET_BY_ID", ID),
12            ("PATH_COUNT", NONE),
13            ("PATH_SIZE", ID),
14            ("PATH_DISTINCT_NODE_COUNT", ID),
15            ("CONTAINS_PATH", SEQUENCE),
16            ("CONTAINS_PATH_ID", ID),
17            ("DISTINCT_NODE_COUNT", NONE),
18            ("COMPARE_PATHS", DOUBLE_ID),
19            ("PATH_CONTAINS_NODE", ID_NODE)
20            ]
21 
22 NUMBER = 100
23 PATH_LENGTH = 500
24 query_count = len(queries)
25 path_count = 0
26 
27 
28 def gen_node():
29     """generate random node"""
30     return random.randint(-2**31, 2**31 -1)
31 
32 def gen_none():
33     """"""
34     return []
35 
36 def gen_sequence():
37     """generate id sequence"""
38     len = random.randint(2, PATH_LENGTH)
39     sequence = []
40 
41     for i in range(len):
42         sequence.append(gen_node())
43 
44     path_count + 1;
45     return sequence
46 
47 def gen_id():
48     """generate id"""
49     return [random.randint(1, path_count * 2 + 1)]
50 
51 def gen_doubel_id():
52     """generate two ids"""
53     return [random.randint(1, path_count + 1), random.randint(1, path_count + 1)]
54 
55 def gen_id_node():
56     return [random.randint(1, path_count + 1), gen_node()]
57     
58 # print(gen_sequence())
59 
60 generators = {SEQUENCE : gen_sequence,
61               ID: gen_id,
62               DOUBLE_ID: gen_doubel_id,
63               NONE: gen_none,
64               ID_NODE: gen_id_node }
65 
66 for i in range(13):
67     (op, arg) = queries[0]
68     print(op + ' ' + ' '.join(map(lambda x: str(x), generators[arg]())))
69 for i in range(NUMBER):
70     (op, arg) = queries[random.randint(0, query_count - 1)]
71     print(op + ' ' + ' '.join(map(lambda x: str(x), generators[arg]())))

 

IDEA TestMe插件和 TestNG和OpenJML的安裝歷程

  1. 安裝TestMe插件，可以直接在Plugin 的Market裡面下載，TestNG失敗

  2. 下載TestNG

(TestNG下載及安裝教程鏈接)

（TestNG6.8.7JAR包的下載鏈接）

Build TestNG from source code

TestNG is also hosted on GitHub, where you can download the source and build the distribution yourself:

 

然後把Jar包導入新創建的Maven項目當中，課程組的Jar包導入項目當中

在右側邊欄的Maven，點擊加號，把課程組給的pom.xml導入

後來弄出了形如這樣的一堆令人頭疼的代碼，遂放棄

  
 1     @Test
 2     public void testGetConnectedBlockCount() {
 3         when(bfs.getBlockSize()).thenReturn(0);
 4         when(bfs.updateGraph(any())).thenReturn(new HashMap<Integer, HashMap<Integer, Integer>>() {{
 5             put(Integer.valueOf(0), new HashMap<Integer, Integer>() {{
 6                 put(Integer.valueOf(0), Integer.valueOf(0));
 7             }});
 8         }});
 9 
10         int result = myRailwaySystem.getConnectedBlockCount();
11         Assert.assertEquals(result, 0);
12     }

（錯誤示範）

 

正確使用OpenJML

在許多大佬的帖子中已經把如何生成測試代碼講得很清楚了

示例主程式在Demo.java裡面

java -jar jmlunitng.jar src/Demo.java 
javac -cp jmlunitng.jar src/*.java
 

然後會出現很多名字奇怪的.java文件，其中有一個叫Demo_JML_Test.java，也就是測試時要運行的主程式

我把生成的.java測試文件都加入到IDEA工程的src文件夾下麵，需要導入的包有openjml.jar，jmlunitng.jar

但是我在運行Demo_JML_Test的時候有一些奇怪的報錯 “org.jmlspecs.utils.JmlAssertionError 中是 protected訪問控制”

於是把報錯代碼Catch 的 Exception刪了

 

在艱苦卓絕的研究下，和修改了一堆版本不相容的問題後，測試代碼終於運行成功了！

（racEnabled尚未解決）

 

Junit 測試代碼

創建單元測試可以直接在IDEA裡面自動生成一個測試代碼的框架

 

 

Junit中集中基本註解，是必須掌握的：

  • @BeforeClass – 表示在類中的任意public static void方法執行之前執行

  • @AfterClass – 表示在類中的任意public static void方法執行之後執行

  • @Before – 表示在任意使用@Test註解標註的public void方法執行之前執行

  • @After – 表示在任意使用@Test註解標註的public void方法執行之後執行

  • @Test – 使用該註解標註的public void方法會表示為一個測試方法

 

junit中的assert方法全部放在Assert類中，總結一下junit類中assert方法的分類。

Junit中部分Assert方法總結：（來自這個博客）

  1. assertTrue/False([String message,]boolean condition); 判斷一個條件是true還是false。感覺這個最好用了，不用記下來那麼多的方法名。

  1. fail([String message,]); 失敗，可以有消息，也可以沒有消息。

  1. assertEquals([String message,]Object expected,Object actual); 判斷是否相等，可以指定輸出錯誤信息。 第一個參數是期望值，第二個參數是實際的值。 這個方法對各個變數有多種實現。在JDK1.5中基本一樣。 但是需要主意的是float和double最後面多一個delta的值。

  1. assertNotEquals([String message,]Object expected,Object actual); 判斷是否不相等。 第一個參數是期望值，第二個參數是實際的值。

  1. assertArrayEquals([java.lang.String message,] java.lang.Object[] expecteds, java.lang.Object[] actuals) ;

  1. assertNotNull/Null([String message,]Object obj); 判讀一個對象是否非空(非空)。

  1. assertSame/NotSame([String message,]Object expected,Object actual); 判斷兩個對象是否指向同一個對象。看記憶體地址。

  1. failNotSame/failNotEquals(String message, Object expected, Object actual) 當不指向同一個記憶體地址或者不相等的時候，輸出錯誤信息。 註意信息是必須的，而且這個輸出是格式化過的。

下麵僅寫出部分函數的測試代碼

 1 public class MyGraphTest {
 2     MyGraph graph = new MyGraph();
 3     int[] nodelist1 = {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 13};
 4     int[] nodelist2 = {-1, 6, -2, -3, -4, -5, -6, -7, -8};
 5     int[] nodelist3 = {0,1205, 999, 888, 777, 666};
 6     @Before
 7     public void before() throws Exception { // 每個方法檢測之前，都另這個圖裡面有這三條路徑
 8         System.out.println("Ready to test " );
 9         //MyGraph graph = new MyGraph();
10         graph.addPath(new MyPath(nodelist1));
11         graph.addPath(new MyPath(nodelist2));
12         graph.addPath(new MyPath(nodelist3));
13     }
14 
15     @After
16     public void after() throws Exception { // 每個函數檢測完畢都會輸出“test successfully!”
17         System.out.println("test successfully!");
18     }
19 
20 @Test
21 public void testContainsPath() throws Exception { 
22 //TODO: Test goes here...
23     System.out.println("Testing ContainsPath!");
24     Assert.assertTrue(graph.containsPath(new MyPath(nodelist1)));
25     Assert.assertTrue(graph.containsPath(new MyPath(nodelist2)));
26     Assert.assertTrue(graph.containsPath(new MyPath(nodelist3)));
27     int[] nodelist4 = {9,9,9,9};
28     Assert.assertFalse(graph.containsPath(new MyPath(nodelist4)));
29 } 
30 
31 @Test
32 public void testContainsPathId() throws Exception { 
33     System.out.println("Testing contains Path id!");
34     Assert.assertTrue(graph.containsPathId(1));
35     Assert.assertTrue(graph.containsPathId(2));
36     Assert.assertTrue(graph.containsPathId(3));
37     Assert.assertFalse(graph.containsPathId(100));
38 } 
39 
40 
41 @Test
42 public void testRemovePath() throws Exception { 
43 //TODO: Test goes here...
44     graph.removePath(new MyPath(nodelist1));
45     Assert.assertFalse(graph.containsPathId(1));
46 } 
47 
48 @Test
49 public void testRemovePathById() throws Exception { 
50 //TODO: Test goes here...
51     graph.removePathById(2);
52     Assert.assertFalse(graph.containsPath(new MyPath(nodelist2)));
53 } 
54 
55 @Test
56 public void testContainsNode() throws Exception { 
57 //TODO: Test goes here...
58     Assert.assertTrue(graph.containsNode(999));
59     Assert.assertFalse(graph.containsNode(14));
60 
61 
62 @Test
63 public void testIsConnected() throws Exception { 
64 //TODO: Test goes here...
65     System.out.println("Testing is Connected@");
66     Assert.assertTrue(graph.isConnected(2,-8)); // 判斷這個連接是對的
67     Assert.assertTrue(graph.isConnected(13,-8));
68     Assert.assertFalse(graph.isConnected(0, 1));
69     // 把這個文件拖到src文件夾裡面即可運行
70 
71 }
72 
73 }

愉快的Tests passed!

您的分享是我們最大的動力!

-Advertisement-
Play Games
更多相關文章
  • Phpstorm建立連接Wampserver的資料庫
    phpstorm是一款php集成開發環境軟體，集成了很多功能，不但有強大的代碼編輯及調試功能，還能連接資料庫。本文寫的就是如何用phpstorm來建立訪問wampserver資料庫，查詢輸出數據，方便我們開發工作。 1、新建資料庫 方法一：點擊wampserver的綠色圖標，直接選擇phpMyAdm ...
  • js計算兩個時間差 天 時 分 秒 毫秒
    // 計算兩個時間差 dateBegin 開始時間 function timeFn(dateBegin) { //如果時間格式是正確的，那下麵這一步轉化時間格式就可以不用了 var dateEnd = new Date();//獲取當前時間 var dateDiff = dateEnd.getTim... ...
  • 大廠-十道前端面試題
    第 1 題：請設計一個攻擊伺服器的策略 難度：阿裡p5 ~ p7、騰訊t21 ~ t31 提供幾個常見的策略 前段時間很火的一個例子，偽造虛假npm包 + nodejs版本的payload nodejs的反序列化攻擊 第 2 題：請寫一個正則，去除掉html標簽字元串里的所有屬性，並保留src和hr ...
  • js 調用棧機制與ES6尾調用優化介紹
    調用棧的英文名叫做Call Stack，大家或多或少是有聽過的，但是對於js調用棧的工作方式以及如何在工作中利用這一特性，大部分人可能沒有進行過更深入的研究，這塊內容可以說對我們前端來說就是所謂的基礎知識，咋一看好像用處並沒有很大，但掌握好這個知識點，就可以讓我們在以後可以走的更遠，走的更快！ "博 ...
  • JS - 計算兩個數組的交集、差集、並集、補集（多種實現方式）
    方法一：最普遍的做法 使用 ES5 語法來實現雖然會麻煩些，但相容性最好，不用考慮瀏覽器 JavaScript 版本。也不用引入其他第三方庫。 1，直接使用 filter、concat 來計算 var a = [1,2,3,4,5] var b = [2,4,6,8,10] //交集 var c = ...
  • Node.js學習（第四章：初見express）
    `Express Express API`的事情，這就使得我們更加註重業務的功能和開發效率上，不必糾結過多底層的事情。 Express中文官網： "Express" 快速入門 1. 安裝： 2. 項目中引入： 3. 運行項目: 利用express框架可以減少我們的代碼量，比起之前使用node核心模塊 ...
  • vue3.0學習筆記（一）
    一、搭建工作環境環境 1、從node.js官網下載相應版本進行安裝即可 https://nodejs.org/zh-cn/download/，安裝完成後在命令行輸入 node -v 如果可以查詢到版本號，說明安裝成功。 2、node自帶npm包管理工具，在命令行輸入 npm -v 如果查詢到版本號， ...
  • 設計模式實戰研磨 ——第1篇 UML環境搭建
    starUML是開源的基於統一模式語言與模式驅動開發的平臺，前身是Plastic，從1996年開始開發。1998年開始，Plastic轉變為UML建模工具。2005年改名為StarUML，最新版本StarUML 5.0已經是一款功能全面的產品，支持UML2.0，支持MDA，Java、C++、C#轉換 ...
一周排行
    -Advertisement-
    Play Games
  • 移動開發（一）：使用.NET MAUI開發第一個安卓APP
    移動開發（一）：使用.NET MAUI開發第一個安卓APP 對於工作多年的C#程式員來說，近來想嘗試開發一款安卓APP，考慮了很久最終選擇使用.NET MAUI這個微軟官方的框架來嘗試體驗開發安卓APP，畢竟是使用Visual Studio開發工具，使用起來也比較的順手，結合微軟官方的教程進行了安卓 ...
  • wpf ToggleButton選中效果和一個登錄界面
    前言 QuestPDF 是一個開源 .NET 庫，用於生成 PDF 文檔。使用了C# Fluent API方式可簡化開發、減少錯誤並提高工作效率。利用它可以輕鬆生成 PDF 報告、發票、導出文件等。 項目介紹 QuestPDF 是一個革命性的開源 .NET 庫，它徹底改變了我們生成 PDF 文檔的方 ...
  • 彈幕樹洞項目功能新增篇
    項目地址 項目後端地址： https://github.com/ZyPLJ/ZYTteeHole 項目前端頁面地址： ZyPLJ/TreeHoleVue (github.com) https://github.com/ZyPLJ/TreeHoleVue 目前項目測試訪問地址： http://tree ...
  • 第27篇 sqlserver2022詳細安裝步驟
    話不多說，直接開乾 一.下載 1.官方鏈接下載： https://www.microsoft.com/zh-cn/sql-server/sql-server-downloads 2.在下載目錄中找到下麵這個小的安裝包 SQL2022-SSEI-Dev.exe，運行開始下載SQL server； 二. ...
  • .NET 開源高性能 MQTT 類庫
    前言 隨著物聯網（IoT）技術的迅猛發展，MQTT（消息隊列遙測傳輸）協議憑藉其輕量級和高效性，已成為眾多物聯網應用的首選通信標準。 MQTTnet 作為一個高性能的 .NET 開源庫，為 .NET 平臺上的 MQTT 客戶端與伺服器開發提供了強大的支持。 本文將全面介紹 MQTTnet 的核心功能 ...
  • Serilog文檔翻譯系列（六） - 可用的接收器、增強器、格式化輸出
    Serilog支持多種接收器用於日誌存儲，增強器用於添加屬性，LogContext管理動態屬性，支持多種輸出格式包括純文本、JSON及ExpressionTemplate。還提供了自定義格式化選項，適用於不同需求。 ...
  • 警惕 Visual Studio 屬性求值副作用導致邏輯不符合預期
    目錄簡介獲取 HTML 文檔解析 HTML 文檔測試參考文章 簡介 動態內容網站使用 JavaScript 腳本動態檢索和渲染數據，爬取信息時需要模擬瀏覽器行為，否則獲取到的源碼基本是空的。 本文使用的爬取步驟如下： 使用 Selenium 獲取渲染後的 HTML 文檔 使用 HtmlAgility ...
  • [使用目前最新版]HybridCLR6.9.0+YooAsset2.2.4實現純C# Unity熱更新方案 (一)
    1.前言 什麼是熱更新 游戲或者軟體更新時，無需重新下載客戶端進行安裝，而是在應用程式啟動的情況下，在內部進行資源或者代碼更新 Unity目前常用熱更新解決方案 HybridCLR，Xlua，ILRuntime等 Unity目前常用資源管理解決方案 AssetBundles，Addressable， ...
  • 在 ASP.NET Core Web API 中使用操作篩選器統一處理通用操作
    本文章主要是在C# ASP.NET Core Web API框架實現向手機發送驗證碼簡訊功能。這裡我選擇是一個互億無線簡訊驗證碼平臺，其實像阿裡雲，騰訊雲上面也可以。 首先我們先去 互億無線 https://www.ihuyi.com/api/sms.html 去註冊一個賬號 註冊完成賬號後，它會送 ...
  • 第28篇 如何.net中實現高效可靠數據同步api
    通過以下方式可以高效，並保證數據同步的可靠性 1.API設計 使用RESTful設計，確保API端點明確，並使用適當的HTTP方法（如POST用於創建，PUT用於更新）。 設計清晰的請求和響應模型，以確保客戶端能夠理解預期格式。 2.數據驗證 在伺服器端進行嚴格的數據驗證，確保接收到的數據符合預期格 ...
所有分類