你寫了一段自認為“天衣無縫”的程序，但如何確保它真的沒有bug？靠手動測試？可能漏掉邊界情況；靠直覺？更不靠譜！這時候，Promela + SPIN組合就像程序的“顯微鏡”——用形式化驗證技術，幫你揪出藏在代碼角落的小毛病。
本文結合SPIN工具，通過5個生動案例，帶你學會用**斷言（Assertions）**給程序“設關卡”，再用SPIN做“全面體檢”，徹底掌握順序程序的驗證方法！
2.1 斷言：程序的“自動質檢員”
斷言是程序里的“檢查點”，你可以用assert(condition)聲明“這里必須滿足某個條件”。SPIN驗證時會逐一檢查這些斷言，一旦不滿足，就會報錯并給出具體位置——就像給程序派了個24小時值班的“質檢員”。
案例1：簡單加法的“正確性考試”
假設你寫了個加法函數，想驗證它是否正確。用斷言直接“出題”：
proctype AddTest() {int a = 5, b = 3;int sum = a + b;assert(sum == 8); /* 斷言：5+3必須等于8 */printf("加法正確，sum=%d\n", sum);
}init {run AddTest();
}
驗證過程：
- 用SPIN編譯：
spin -a add.pml（生成驗證代碼）。 - 編譯C驗證程序：
gcc -o pan pan.c（生成可執行文件pan）。 - 運行驗證：
./pan -a。
結果：SPIN會輸出pan: no errors found（無錯誤），說明斷言成立。如果把sum == 8改成sum == 9，SPIN會立刻報錯：pan: assertion failed，并告訴你錯誤在第4行！
案例2：條件分支的“狀態跟蹤”
程序中經常有if-else分支，如何確保分支執行后變量狀態正確？用斷言“跟蹤”！
proctype BranchTest() {int score = 85;if:: score >= 60 -> int grade = 1; /* 及格 */assert(grade == 1); /* 斷言：及格時grade應為1 */:: else -> int grade = 0; /* 不及格 */assert(grade == 0); /* 斷言：不及格時grade應為0 */fi;
}init {run BranchTest();
}
關鍵點：
- 每個分支末尾都有斷言，強制檢查分支執行后的狀態。
- 如果把
score = 85改成50，SPIN會執行else分支，并檢查grade == 0是否成立——如果代碼寫錯（比如誤寫成grade = 2），斷言立刻報錯！
案例3：循環的“不變式守衛”
循環是bug的重災區（比如越界、累加錯誤）。用斷言守住循環的“不變式”（循環中始終成立的條件），能有效預防問題。
proctype LoopTest() {int sum = 0;for (int i=1; i<=5; i++) {sum += i;assert(sum == i*(i+1)/2); /* 斷言：前i項和等于i(i+1)/2 */}assert(sum == 15); /* 斷言：最終和為15 */
}init {run LoopTest();
}
白話解釋：
- 循環中每一步，
sum應該等于1+2+...+i，而數學公式i(i+1)/2正好是前i項和。用斷言守住這個“不變式”，即使循環內代碼寫錯（比如寫成sum += i*2），SPIN也會在第一次循環就報錯！ - 循環結束后，再斷言最終結果是否正確（1+2+3+4+5=15），雙重保險！
2.2 SPIN驗證：給程序做“全身檢查”
SPIN的核心功能是模型檢查——自動遍歷程序所有可能的執行路徑，檢查是否違反斷言或其他屬性（如死鎖）。接下來教你用SPIN完成“驗證三連”：編譯→驗證→分析。
2.2.1 引導模擬：手動“走查”程序路徑
有時候程序有多個分支（比如隨機選擇），SPIN默認隨機模擬可能漏掉某些路徑。這時候可以用引導模擬（Guided Simulation），手動選擇每一步的執行路徑，確保覆蓋所有可能。
案例4：隨機抽獎的“公平性驗證”
假設有個抽獎程序，隨機選1-3號獎品，用引導模擬確保每個獎品都能被選中。
mtype { PRIZE1, PRIZE2, PRIZE3 };proctype Lottery() {mtype prize = PRIZE1 + (rand() % 3); /* 隨機選1-3號獎品 */if:: prize == PRIZE1 -> printf("抽到1號獎品\n");:: prize == PRIZE2 -> printf("抽到2號獎品\n");:: prize == PRIZE3 -> printf("抽到3號獎品\n");fi;
}init {run Lottery();
}
引導模擬步驟（用JSPIN工具更簡單）：
- 打開JSPIN，加載
lottery.pml，點擊Simulate→Guided。 - SPIN會顯示當前可執行的分支（比如第一次模擬可能選
PRIZE1）。 - 手動選擇其他分支（通過
Next按鈕切換），直到覆蓋所有3種獎品。
結果：如果某個獎品從未被選中（比如代碼寫錯成rand() % 2），引導模擬會暴露這個問題——你會發現永遠抽不到3號獎品！
2.2.2 顯示計算路徑：看清程序的“每一步”
SPIN驗證出錯時，會生成一個錯誤軌跡（Error Trace），告訴你程序是如何一步步走到錯誤狀態的。通過查看這個軌跡，你可以像“倒放電影”一樣，找到問題根源。
案例5：冒泡排序的“正確性驗證”
寫一個冒泡排序程序，用SPIN驗證是否真的能排好序，并查看排序的具體步驟。
proctype BubbleSort() {int arr[5] = {3, 1, 4, 2, 5}; /* 待排序數組 */int n = 5;/* 冒泡排序核心邏輯 */for (int i=0; i<n-1; i++) {for (int j=0; j<n-i-1; j++) {if (arr[j] > arr[j+1]) {int temp = arr[j];arr[j] = arr[j+1];arr[j+1] = temp;}}}/* 斷言：數組已升序排列 */for (int k=0; k<4; k++) {assert(arr[k] <= arr[k+1]);}printf("排序成功！數組：%d,%d,%d,%d,%d\n", arr[0], arr[1], arr[2], arr[3], arr[4]);
}init {run BubbleSort();
}
驗證與軌跡查看：
- 用
spin -a sort.pml編譯，gcc -o pan pan.c生成驗證程序。 - 運行
./pan -t（-t參數顯示軌跡），SPIN會輸出排序的每一步：1: proc 0 (BubbleSort) line 3 "sort.pml" (state 1) /* 初始化數組 */ 2: proc 0 line 7 (state 2) i=0 /* 外層循環i=0 */ 3: proc 0 line 8 (state 3) j=0 /* 內層循環j=0 */ 4: proc 0 line 9 (state 4) arr[0]=3 > arr[1]=1 → 交換 /* 交換3和1 */ 5: proc 0 line 13 (state 5) j=1 /* 內層循環j=1 */ ...（后續步驟顯示所有交換） 最終：數組變為1,2,3,4,5，斷言通過！
如果排序錯誤（比如把arr[j] > arr[j+1]寫成<），SPIN會報錯，并顯示哪一步交換導致了逆序，幫你快速定位問題。
總結：驗證的“三板斧”
- 斷言：在關鍵位置設“檢查點”，強制程序滿足條件。
- SPIN自動驗證：遍歷所有可能路徑，揪出隱藏bug。
- 引導模擬+軌跡顯示：手動覆蓋分支，看清執行步驟，徹底理解程序行為。
現在，你已經掌握了用Promela和SPIN驗證順序程序的核心技能！下次寫代碼時，不妨先加幾個斷言，再用SPIN“體檢”——程序的bug，再也無處可藏啦！
)
