程序验证（Hoare Logic, 分离逻辑）

✅ “这个程序是对的”——能不能用数学证明？

“程序是对的”——你怎么证明？

测试：跑了 100 个用例，都对——“看起来是对的”。但第 101 个呢？

Hoare Logic 提供了一种用数学逻辑证明程序正确性的方法——不需要运行程序，只需要对代码进行逻辑推理。

🏪 **类比：做菜”

测试 = 你做了 10 盘鱼香肉丝——每盘味道都不错——“我会做这道菜了”。

Hoare Logic = 你写下菜谱（程序），并证明：

• 如果材料准备好(前置条件)
• 按菜谱做（程序）
• 最终一定会得到鱼香肉丝(后置条件)

这种”证明”不依赖具体试做多少次——从逻辑上保证。

---

📐 Hoare Triple——正确性的”三段论”

Hoare Logic 的核心是 Hoare 三元组（Hoare Triple）：

{P} C {Q}

P = 前置条件（Precondition）——程序运行前必须满足的条件
C = 命令（Command）——要执行的程序
Q = 后置条件（Postcondition）——程序运行后保证成立的条件

示例：
{x = 0} x := x + 1 {x = 1}
如果运行前 x=0——执行 x:=x+1——运行后 x=1

# Python 中的 Hoare Triple 思维
# {x >= 0}                   ← 前置条件：x 是非负数
y = sqrt(x)
# {y * y == x}               ← 后置条件：y 的平方等于 x

# 不是"测试几个用例发现 sqrt 的结果平方等于 x"
# 而是"如果前置条件成立，数学上保证后置条件成立"

---

🔧 Hoare Logic 的推理规则

赋值规则

{Q[E/x]} x := E {Q}

把 Q 中所有 x 替换为 E——就是前置条件
例子：
{x+1 = 2} x := x+1 {x = 2}
→ 如果 x+1=2（即 x=1），执行 x:=x+1，则 x=2 ✅

顺序规则

{P} C1 {R}, {R} C2 {Q}
────────────────────
{P} C1; C2 {Q}

如果 C1 从 P 到 R，C2 从 R 到 Q——那么执行 C1; C2 从 P 到 Q

条件规则

{P ∧ B} C1 {Q}, {P ∧ ¬B} C2 {Q}
────────────────────────────
{P} if B then C1 else C2 {Q}

循环规则——最难的部分

{I ∧ B} C {I}
──────────────────
{I} while B do C {I ∧ ¬B}

I 是循环不变式（Loop Invariant）——每次循环开始都成立的条件

找循环不变式是 Hoare Logic 中最有挑战的部分

# 循环不变式的例子：计算阶乘

# {n >= 0}                    ← 前置条件
# i = 1
# fact = 1
# while i <= n:              ← I: fact == (i-1)! 且 i <= n+1（不变式）
#     fact = fact * i
#     i = i + 1
# {fact == n!}               ← 后置条件

# 证明循环正确性时需要：
# 1. 初始时不变式成立（i=1, fact=1=0! ✅）
# 2. 每次迭代——如果 I 且条件成立，执行循环体后 I 仍然成立
# 3. 循环结束时——I 且 ¬(i<=n) → fact == n! ✅

---

🧩 分离逻辑——处理指针和堆

Hoare Logic 只能处理简单的变量——不能处理指针、共享内存、数据结构。

分离逻辑（Separation Logic） 的扩展：

{P} C {Q} 时——P 和 Q 描述的是"堆的状态"

关键操作：
P * Q        → P 和 Q 描述的是不相交的堆区域
x ↦ v       → 指针 x 指向的值是 v

例子：
{x ↦ 5} y := x; y := 10 {x ↦ 5 * y ↦ 10}
"x 原来的堆区域没变，y 现在指向了新区域"

分离逻辑允许局部推理——你可以只关注程序涉及的堆区域，不需要考虑整个内存——大大简化了指针程序的验证。

---

📝 小结

概念	一句话
Hoare Triple	{P} C {Q}——程序正确性的数学规范
前置条件（P）	程序运行前必须满足的条件
后置条件（Q）	程序运行后保证成立的条件
循环不变式	循环开始前每次都成立的断言——最难找
分离逻辑	处理指针和堆——解决”别名问题”
意义	不运行程序就能证明程序正确

🎯 思考题：一个程序在所有测试用例上通过——和用 Hoare Logic 证明正确——有什么区别？前者能保证”没有 Bug”吗？后者能保证吗？

为什么先学这个？ 形式化方法板块到此全部结束。它代表了”计算机科学的数学根基”——从逻辑到验证，每一步都追求”无漏洞”的精确。