Hoare逻辑

Hoare逻辑是一种用于程序验证的形式系统，由Tony Hoare在1969年提出。

基本形式

Hoare三元组：{P} C {Q}

• P：前置条件
• C：程序命令
• Q：后置条件

推理规则

• 空语句规则
• 赋值规则
• 顺序规则
• 条件规则
• 循环规则

应用场景

程序正确性验证、编译器优化证明、安全关键系统验证。