你写了一段自认为“天衣无缝”的程序，但如何确保它真的没有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();
}

验证过程：

1. 用SPIN编译：spin -a add.pml（生成验证代码）。
2. 编译C验证程序：gcc -o pan pan.c（生成可执行文件pan）。
3. 运行验证：./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工具更简单）：

1. 打开JSPIN，加载lottery.pml，点击Simulate→Guided。
2. SPIN会显示当前可执行的分支（比如第一次模拟可能选PRIZE1）。
3. 手动选择其他分支（通过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();
}

验证与轨迹查看：

1. 用spin -a sort.pml编译，gcc -o pan pan.c生成验证程序。
2. 运行./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会报错，并显示哪一步交换导致了逆序，帮你快速定位问题。

---

总结：验证的“三板斧”

1. 断言：在关键位置设“检查点”，强制程序满足条件。
2. SPIN自动验证：遍历所有可能路径，揪出隐藏bug。
3. 引导模拟+轨迹显示：手动覆盖分支，看清执行步骤，彻底理解程序行为。

现在，你已经掌握了用Promela和SPIN验证顺序程序的核心技能！下次写代码时，不妨先加几个断言，再用SPIN“体检”——程序的bug，再也无处可藏啦！