Hoare Logic，一种用于形式化验证计算机程序正确性的系统，也被称为霍尔三元组（Hoare Triple）。它基于先前条件、后置条件以及程序语句来判定程序部分的正确性。
一个霍尔三元组可以表示为
(P) C (Q)P是前置条件，描述了程序执行前的条件
C是程序代码或命令
Q是后置条件，描述了程序执行后应该满足的条件
如果先前条件
P 成立，并且程序 C 被执行，那么在 C 执行结束后，后置条件 Q 也将成立。Example
- 两数交换
- 证明 的正确性？
- 赋值操作 ，后置条件
- 将 x = x+5 带入后置条件得到 x+5>10，化简得到先决条件 x>5
⇒ 说明这段程序是正确的
Exercise
Lab 5Fill in the question marks in the following Hoare triples to provide the weakest precondition. Simplify the formulas you obtain.
{?}
{𝑦 − 𝑥 == 3}
需要确定一个前置条件，使得执行赋值
x, y = x + 1, 2 * x 后，能够确保后置条件 y - x == 3 成立，即把赋值后的参数代入后置条件，来反推前置条件which simplifies to