Hoare triples
The line of code never tells you the result by itself. The precondition does.
A predicate is a true-or-false claim about the program’s state. In this course it wears square brackets: \([x > 0]\). Code wears braces: \(\{\texttt{x = x + 1;}\}\). A Hoare triple is the whole sandwich:
\[ [\text{precondition}] \quad \{\text{statements}\} \quad [\text{postcondition}]. \]
Read it as a promise. If the precondition is true and the statements run to completion, the postcondition is true.
Thanos can snap only because six stones are already in the gauntlet. Iron Man later runs a statement with the same shape and a different precondition, and the postcondition is a different army. Same verb, different ingredients, different result.
The subscript-zero snapshot
\(x_0\) is not a variable the program updates. It is a name for whatever \(x\) was at a chosen instant. After x = x + 1 you want \([x = x_0 + 1]\), not the limp \([x > x_0]\). The second one is true and too weak: it also allows \(x = x_0 + 40\).
The postcondition of one line is the precondition of the next.
\([a = a_0]\{\texttt{a = a + 1;}\}[a = a_0 + 1]\{\texttt{a = a * 2;}\}[a = 2a_0 + 2].\)
Writing \([a = 2a]\) is nonsense. \(a\) cannot appear on both sides as if it had two values.
Branches join with or
Exactly one branch runs. Prove each branch with its test folded in, then combine with \(\lor\), never \(\land\).
if (x > 7)
y = x;
else
y = 0;
The two landings are \([x > 7 \land y = x]\) and \([x \le 7 \land y = 0]\). The postcondition is their disjunction. Using \(\land\) would claim both branches ran.
Forward is strongest, backward is weakest
If \(P \Rightarrow Q\), then \(P\) is stronger. It rules out more worlds. \([x = 3]\) is stronger than \([x > 0]\).
- You are given a start and a statement, and asked what you know afterward. That is the strongest postcondition. Reason forward.
- You are given a statement and a goal, and asked what must have been true beforehand. That is the weakest precondition. Reason backward. “Weakest” means the most generous start that still forces the goal.
Weakest precondition of \(\{\texttt{x = x + 1;}\}\) for the goal \([x \le 10]\) is \([x \le 9]\). Asking for \([x \le 8]\) also works, and it rejects a start that would have been fine.
A branch, backward
Goal: \([q > 6]\) after
if (p < 10) q = p + 1; else q = p - 10;
True branch: \(5 < p < 10\). False branch: \(p > 16\). Join them:
\[ (5 < p < 10) \lor (p > 16). \]
Check the boundary. If \(p = 5\), the true branch sets \(q = 6\), and \(6 > 6\) is false. If \(p = 16\), the false branch also sets \(q = 6\). If \(p = 10\), you take the else and \(q = 0\). The gap is real.
From \([x = x_0]\), after x = x + 1, the strongest postcondition is \([x = x_0 + 1]\). \([x \ge x_0]\) is true and it is not the strongest.