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

来源:https://www.cnblogs.com/refkxh/archive/2020/05/19/12919460.html
-Advertisement-
Play Games

北航OO（2020）第三單元博客作業 [TOC] JML語言總結 理論基礎 JML是用於對Java程式進行規格化設計的一種表示語言，它使用JavaDoc註釋的方式來表示規格。JML以Java語法為基礎併進行了一定的擴充。JML的語法分為幾個層次，下麵對JML Level 0的核心特性進行簡要的總結。 ...


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

目錄

JML語言總結

理論基礎

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

規格變數的聲明

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

常用表達式

表達式 含義
\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方法返回的結果。

對於異常行為規格，我們通常會使用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的現象。

在理解規格時，重點是對規格行為的理解。通常情況下，規格描述並不適合直接作為代碼實現。因此，我們需要對規格所描述的行為進行理解，並由此選擇合適的實現。我們甚至還可以在規格的基礎上進一步抽象，設計出更加清晰合理的程式架構。

雖然如此嚴格而繁瑣的形式化規格表述在日常軟體的開發領域並不常見，但我相信，由於其可以進行嚴格的形式化驗證，形式化的規格在高可靠性領域一定大有用武之地。


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

-Advertisement-
Play Games
更多相關文章
  • 前端小玩意兒：用three.js開發的手機太空穿越VR游戲，特效非常猛
    hello，今天給大家用three.js開發了一個手機太空穿越VR游戲，確實不容易，小編的頭髮又少了一大截。Ok，廢話少說，先看效果。 效果圖 首頁index.html <!DOCTYPE html> <html lang="en" > <head> <meta charset="UTF-8"> < ...
  • layui table 行點擊事件與列點擊事件衝突
    問題描述： 工具欄的點擊事件，會冒泡到行點擊事件中，原打算阻止事件冒泡 ，結果失敗，阻止不了，索性不用layui官網的工具欄tool和行row監聽事件。 table： <table id="conManager" lay-filter="conManager" class="layui-table ...
  • 僅需 5 步，用 JavaScript 直接通過前端發送電子郵件
    小編提醒大家，一定要看到文章最後歐，有驚喜哦 你為什麼不通過發送電子郵件傳輸信息？ 不使用資料庫就能接收到傳入的消息，絕對是最佳選擇，也是最方便用戶的選擇。但問題來了—如何實現呢？你可能認為需要使用某種後端語言。 實際上，你不必使用任何如 php 或 python 這種後端語言，你甚至不需要用到 n ...
  • Java Web系列之使用Eclipse開發web項目(jsp項目)
    Java Web系列之使用Eclipse開發web項目(jsp項目) ...
  • 學習web前端方法心得，從基礎到深度，才能學的扎實
    web前端一定要這樣學，才會事半功倍！ 如果你是想要學習web前端的新人，那麼恭喜你，看完這篇文章，儘早的選擇好努力的方向和規劃好自己的學習路線，比別人多一點付出並且持之以恆，你就已經贏在了起跑線上。有道是，莫道君行早，更有早行人。 如果你已經學完了但是還沒找到工作，那麼就應該反省一下自己，到底哪些 ...
  • vue利用全局導航守衛作登錄後跳轉到未登錄前指定頁面
    有這樣一個場景：如果你在登錄之前輸入了http://localhost:8080/oauth2-mgm-app/#/userManage，想進入userManage頁面，但是由於沒有登錄，系統是不會讓你進入這個頁面，之後會被定向到login頁面。但是在登錄之後，認為你有這個許可權了，就需要重新定向到u ...
  • Java Web基本概念
    "TOC" JSP JSP:動態網頁 靜態和動態： 1. 不能和是否有“動感”混為一談 2. 是否隨著時間，地點，用戶操作而改變 動態網頁需要使用到服務端腳本語言（JSP） 架構 架構： 1. BS:網頁端 服務端 1. 如網頁版：京東、百度 2. 客戶端不需要升級 3. 維護方便 4. 不需要安裝 ...
  • 蒲公英 · JELLY技術周刊 Vol.07: EcmaScript 2020 -- 所有你想要知道的都在這
    「蒲公英」期刊，每周更新，我們專註於挖掘「 基礎技術 、 工程化 、 跨端框架技術 、 圖形編程 、 服務端開發 、 桌面開發 、 人工智慧 」等多個大方向的業界熱點，並加以專業的解讀；不僅如此，我們還精選凹凸技術文章，向大家呈現團隊內的研究技術方向。 抬頭仰望，蒲公英的種子會生根發芽，如夏花絢爛； ...
一周排行
    -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.數據驗證 在伺服器端進行嚴格的數據驗證，確保接收到的數據符合預期格 ...
所有分類