PLP: Lecture 32
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.