Hoare逻辑与分离逻辑：从程序验证到内存推理的演进

文章目录

- - 引言
  - - 一、Hoare逻辑基础：程序正确性的形式化验证
    - - 🌰 例子：简单赋值语句的Hoare逻辑验证
      - 🌰 例子：条件语句的Hoare逻辑验证
    - 二、分离逻辑：Hoare逻辑在内存管理中的扩展
    - - 🔍 分离逻辑的核心扩展点
      - 🌰 例子：内存分配的分离逻辑验证
      - 🌰 例子：链表节点操作的分离逻辑
    - 三、Hoare逻辑与分离逻辑的对比
    - 四、总结：分离逻辑如何扩展Hoare逻辑

引言

Rust 的形式化验证工具Prusti是基于 Viper 验证基础设施的工具，用于验证 Rust 程序的内存安全和功能正确性。它通过扩展 Viper 的分离逻辑能力，支持 Rust 特有的所有权系统、生命周期和并发模型验证。Prusti 的核心功能包括：

内存安全验证：自动检查 Rust 代码是否违反借用规则（如悬空指针、数据竞争）。
函数契约验证：通过前置条件（requires）和后置条件（ensures）验证函数行为。
不变式检查：验证结构体和循环的不变式属性（如链表无环、数组边界）。
并发正确性：利用分离逻辑的资源所有权模型，验证多线程程序的原子性和互斥性。

本文主要是对prusti的验证分离逻辑的基础知识进行介绍。

一、Hoare逻辑基础：程序正确性的形式化验证

Hoare逻辑由计算机科学家Tony Hoare于1969年提出，是一种通过前置条件、程序指令、后置条件三元组来验证程序正确性的形式化方法。其核心表示为：
{ P } C { Q }
其中：

P 是前置条件（Precondition），描述程序执行前的状态；
C 是程序指令或代码块；
Q 是后置条件（Postcondition），描述程序执行后的状态。

🌰 例子：简单赋值语句的Hoare逻辑验证

问题：验证赋值语句 x = x + 1 的正确性，假设初始时 x = 5。

Hoare三元组：
{ x = 5 } x = x + 1 { x = 6 }
验证逻辑：
- 前置条件 P：x = 5
- 程序指令 C：x = x + 1
- 后置条件 Q：x = 6
- 根据Hoare逻辑的赋值规则：若指令为 x = e，则前置条件需满足 P[e/x]（将表达式 e 代入 x 后的条件）。这里 e = x + 1，代入后前置条件应为 (x + 1) = 6，即 x = 5，与初始条件一致，故三元组成立。

🌰 例子：条件语句的Hoare逻辑验证

问题：验证条件语句 if (x > 0) x = x - 1 else x = x + 1，确保执行后 x ≥ 0。

Hoare三元组：
{ True } if (x > 0) x = x - 1 else x = x + 1 { x ≥ 0 }
验证逻辑：
- 当 x > 0 时，执行 x = x - 1，后置条件为 x - 1 ≥ 0（即 x ≥ 1）；
- 当 x ≤ 0 时，执行 x = x + 1，后置条件为 x + 1 ≥ 0（即 x ≥ -1，结合前置条件 x ≤ 0，得 x ≥ 0）；
- 无论哪种情况，最终 x ≥ 0 成立。

二、分离逻辑：Hoare逻辑在内存管理中的扩展

分离逻辑（Separation Logic）由John Reynolds等人于2002年提出，专门用于处理指针、动态内存分配和共享内存的程序验证。它在Hoare逻辑基础上引入了空间断言，解决了传统Hoare逻辑在处理内存时的局限性（如悬空指针、内存泄漏等）。

🔍 分离逻辑的核心扩展点

分离合取（*）：
若 A * B 为真，表示内存被划分为两个不相交的区域，A 描述一部分内存的状态，B 描述另一部分的状态。
空指针断言（emp）：
emp 表示空内存或无内存分配的状态。
指向关系（x ↦ v）：
x ↦ v 表示指针 x 指向值 v，且该内存地址有效。

🌰 例子：内存分配的分离逻辑验证

问题：验证动态分配内存并赋值的操作 p = malloc(sizeof(int)); *p = 10。

传统Hoare逻辑的局限性：
无法直接描述内存分配后的指针指向关系，前置条件和后置条件难以准确表达内存状态。
分离逻辑的表示：
- 前置条件：emp（无内存分配）
- 程序指令：p = malloc(sizeof(int)); *p = 10
- 后置条件：p ↦ 10（指针 p 指向值 10）
验证逻辑：
- 分配内存时，malloc 操作将 emp 转换为 p ↦ ?（? 表示未初始化值）；
- 赋值操作 *p = 10 将 p ↦ ? 转换为 p ↦ 10，后置条件成立。

🌰 例子：链表节点操作的分离逻辑

问题：验证创建两个链表节点并连接的操作：

struct Node { int data; struct Node* next; };
struct Node* a = malloc(sizeof(struct Node));
struct Node* b = malloc(sizeof(struct Node));
a->data = 1; b->data = 2;
a->next = b; b->next = NULL;

分离逻辑的空间断言：
- 初始状态：emp
- 分配 a 后：a ↦ {data: ?, next: ?}
- 分配 b 后：(a ↦ {data: ?, next: ?}) * (b ↦ {data: ?, next: ?})
- 赋值并连接后：(a ↦ {data: 1, next: b}) * (b ↦ {data: 2, next: NULL})
关键特性：
分离合取 * 确保 a 和 b 指向的内存区域不重叠，避免了传统Hoare逻辑无法处理内存分离的问题。

三、Hoare逻辑与分离逻辑的对比

特性	Hoare逻辑	分离逻辑
处理对象	顺序程序、基本变量操作	指针、动态内存、数据结构
内存模型	无显式内存表示，假设变量全局可见	显式描述内存分区，支持内存分离
核心断言	前置/后置条件（纯逻辑表达式）	空间断言（如 `x ↦ v`, `A * B`）
典型应用	算术运算、条件语句验证	链表、树结构、并发程序验证
解决的问题	程序功能正确性	内存安全（悬空指针、泄漏等）