形式化方法

命题逻辑研究命题之间的逻辑关系（与、或、非、蕴含）。谓词逻辑引入量词（∀ 所有、∃ 存在）和谓词，表达能力更强，是程序验证的理论基础

模型检验自动验证系统是否满足给定规范——把系统建模为状态机，用时序逻辑（LTL/CTL）描述规范，穷举搜索所有状态检查是否违反规范

定理证明器把数学证明写成代码——计算机检查每一步逻辑推导是否严格正确。Curry-Howard 同构揭示"证明即程序，命题即类型"

Hoare Logic 用前置条件、程序、后置条件的三元组 {P} C {Q} 来推理程序的正确性。分离逻辑扩展了 Hoare Logic，能处理指针和堆操作