Axioms and inference rules allow us to prove that a triple is valid. The axioms and inference rules implicitly define the meaning of a program.

Assignment axiom

{ Q { V := E } and E is defined }
V := E
{ Q }

Whatever is true about E beforehand, is true about V afterwards.

In practice we work backwards. Start with the desired postcondition, then calculate the precondition by substitution.

Notation and vocab

$A \supset B$ (A implies B everywhere) means that any assignment of values to the variables that make A true will also make B true. We say that A is stronger than B, and B is weaker than A.

Example: $x > 0 \supset x \geq 0$.

P is stronger than true, because any assignment of variables makes true true!

Inference rules

Allow us to infer valid triples. Notation is $\frac{P}{Q}$, which means that if we know whatever is above the line is true, then we can conclude that everything below the line is true.

Strengthen the pre-condition, or weaken the post-condition to relate statements about truth.

Consider $\frac{P \supset Q, [Q] S [R]}{[P] S [R]}$. Since P is stronger than Q, and executing S results in a state satisfying R, we can infer the bottom line. This is strengthening the pre-condition.

Consider $\frac{P \supset R, [Q] S [P] }{[Q] S [R]}$. Since P is stronger than R, and executing S results in a state satisfying P, then we can infer the bottom line. This is weakening the post-condition.

Sequence rule

Transitivity $\rightarrow$ $\frac{[P] S0 [Q], [Q] S1 [R]}{[P] S0; S1 [R]}$

Logic variables

Relate the pre- and post-conditions with “logic variables”, e.g., X and Y can have an arbitrary value, but it does not change.

{ x = X and y = Y }
temp := x; 
{y = Y and temp = X}
x := y;
{ x = Y and temp = X }
y := temp; 
{ x = Y and y = X }

If statements

Suppose desired specification is {P} if B then S0 {Q}. Two cases- P is true and B is true and S0 is executed, or P is true and B is not true and nothing happens. In the latter case, we’ll have $(P \hspace{0.2cm} \text{and} \hspace{0.2cm} \neg B) \supset Q)$. Thus the rule becomes \(\frac{[P \hspace{0.2cm} \text{and} \hspace{0.2cm} B] S0 [Q], (P \hspace{0.2cm} \text{and} \hspace{0.2cm} \neg B) \supset Q)}{[P] \hspace{0.2cm} \text{if} \hspace{0.2cm} B \hspace{0.2cm} \text{then} \hspace{0.2cm} S0 \hspace{0.2cm} [Q]}\)

Develop programs to satisfy pre- and post-conditions

{x = X and y = Y} S {(x = X or x = Y) and x >= X and x >= Y}

i.e., x is set to the maximum of X and Y. To establish (x = X or x = Y) can do

  • x := x, or skip (establishes x = X)
  • x := y (establishes x = Y)

Ends up being a complicated application of the if-rule.