Hoare逻辑
Hoare逻辑是一种用于程序验证的形式系统，由Tony Hoare在1969年提出。 基本形式 Hoare三元组：{P} C {Q} - P：前置条件 - C：程序命令 - Q：后置条件 推理规则 - 空语句规则 - 赋值规则 - 顺序规则 - 条件规则 - 循环规则 应用场景 程序正确性验证、编译器优化证明、安全关键...
形状分析
形状分析是一种静态分析技术，用于推断堆内存中数据结构的形状。 核心问题 - 指针别名分析 - 堆结构推断 - 内存泄漏检测 常用方法 - 形状图（Shape Graphs） - 分离逻辑（Separation Logic） - 抽象解释 应用价值 内存安全验证、优化编译器、程序理解工具。
精化演算
精化演算是一种从规范逐步推导实现的形式化开发方法。 基本思想 从抽象规范出发，通过一系列精化步骤，逐步得到具体实现。 精化步骤 1. 数据精化：抽象数据类型 → 具体数据结构 2. 算法精化：非确定性规范 → 确定性算法 3. 代码精化：伪代码 → 目标语言 代表工具 - B方法 - Event-B - Z notat...
静态分析概述
静态分析是在不执行程序的情况下分析程序行为的技术。 主要应用 - 漏洞检测 - 代码质量检查 - 编译优化 常见技术 - 数据流分析 - 控制流分析 - 指针分析 - 抽象解释 权衡 精度与效率的平衡：更精确的分析通常需要更多计算资源。
循环不变式
循环不变式是程序验证中的核心概念，用于证明循环的正确性。 定义 在循环执行过程中始终保持为真的性质。 三个阶段 1. 初始化：循环开始前不变式成立 2. 保持性：每次迭代后不变式仍然成立 3. 终止性：循环结束时不变式结合终止条件可推出目标性质 生成方法 - 模板法 - 抽象解释 - 机器学习辅助
模型检测
模型检测是一种自动验证有限状态系统的技术。 核心思想 通过穷举系统所有可能状态，验证是否满足给定的时序逻辑性质。 输入 - 系统模型（有限状态机） - 性质规约（LTL/CTL） 主要挑战 - 状态爆炸问题 - 无限状态系统 解决方案 - 符号模型检测 - 有界模型检测 - 抽象精化