第7章程序验证 内容概述 程序逻辑：描述和论证程序行为的逻辑 Hoare逻辑 Dijkstra:最弱前条件演算 从程序到定理 -验证条件生成 从定理到证明 定理证明器 判定过程 循环不变式的推断 以George C.Necula教授的讲稿为主来介绍第7章 程序验证 内容概述 • 程序逻辑：描述和论证程序行为的逻辑 – Hoare逻辑 – Dijkstra最弱前条件演算 • 从程序到定理 – 验证条件生成 • 从定理到证明 – 定理证明器 – 判定过程 • 循环不变式的推断 • 以George C. Necula教授的讲稿为主来介绍