Question about Theorem 7.4.11 (pc, vs soundness)

Both cases have to hold simultaneously.
I try to explain this part of the proof in other words:
We want to show that the Hoare triple holds with the computed precondition pc s Q.
That is, we can prove (using the Hoare rules) {pc s Q} s {Q} for any s and Q.
Note: We assume that all side conditions for while loops (vc) hold.

To show this, we perform a case distinction about the shape of s.
As some statements are composed of other statements, we need induction (as known from other basic courses like Programming 1).
One case is the condition If.
Our proof obligation now is to show:

\frac{vc~(if(e)~s_1~else~s_2)~Q}{\{pc~(if(e)~s_1~else~s_2)~Q\}~ (if(e)~s_1~else~s_2)~ \{Q\}}

By induction we know

\frac{vc~s_1~Q}{\{pc~s_1~Q\}~s_1~ \{Q\}}


\frac{vc~s_2~Q}{\{pc~s_2~Q\}~s_2~ \{Q\}}

We have (by definition of vc):
vc~(if(e)~s_1~else~s_2)~Q=(vc~s_1~Q) \cup(vc~s_2~Q)
Therefore, the conditions for the induction hypotheses are fulfilled.

To show

\{P\}~ (if(e)~s_1~else~s_2)~ \{Q\}

we can only apply the [Consequence] rule or [If] rule.
Lets try [If]:

\frac{\{e\land P\}~s_1~ \{Q\} \qquad \{\lnot e\land P\}~s_2~ \{Q\}}{\{P\}~ (if(e)~s_1~else~s_2)~ \{Q\}}

We want to show this with P=pc~(if(e)~s_1~else~s_2)~Q.

\frac{\{e\land pc~(if(e)~s_1~else~s_2)~Q\}~s_1~ \{Q\} \qquad \{\lnot e\land pc~(if(e)~s_1~else~s_2)~Q\}~s_2~ \{Q\}}{\{pc~(if(e)~s_1~else~s_2)~Q\}~ (if(e)~s_1~else~s_2)~ \{Q\}}

Therefore, after applying the [If] rule, we are left to prove
\{e\land pc~(if(e)~s_1~else~s_2)~Q\}~s_1~ \{Q\}
\{\lnot e\land pc~(if(e)~s_1~else~s_2)~Q\}~s_2~ \{Q\}
using our induction hypotheses.

The hypotheses (applied with the proof of the vc conditions) look like:
\{pc~s_1~Q\}~s_1~ \{Q\}
\{pc~s_2~Q\}~s_2~ \{Q\}.

So if we can show

e\land pc~(if(e)~s_1~else~s_2)~Q \Rightarrow pc~s_1~Q

we can apply the consequence rule and proof the obligation using the hypothesis.
Put together in a nice clean tree:

[Consequence]\dfrac{ e\land pc~(if(e)~s_1~else~s_2)~Q \Rightarrow pc~s_1~Q \qquad IH\frac{vc~s_1~Q}{ \{pc~s_1~Q\}~s_1~ \{Q\}} }{ \{e\land pc~(if(e)~s_1~else~s_2)~Q\}~s_1~ \{Q\} }

So how do we obtain the proof of the implication?
It follows directly from the definition:

pc~(if(e)~s_1~else~s_2)~Q := (e\land pc~s_1~Q) \lor (\lnot e\land pc~s_2~Q)
e\land ( (e\land pc~s_1~Q) \lor (\lnot e\land pc~s_2~Q) )\equiv e\land pc~s_1~Q \Rightarrow pc~s_1~Q
1 Like

Your explanation is clear to me, so thank you. However, I also want to point out the typo in theorem proof in the script. In particular, what is marked with yellow color in the next snippet, i.e. e ∧ pc **s1** Q and ¬e ∧ pc **s2** Q should be e ∧ pc **s** Q and ¬e ∧ pc **s2** Q.


Since, as you mentioned for the IfTrue case:

Moreover, there is also a tiny typo:

pc s Q is now defined such that e ∧ pc s Q = pc s1 Q and **e** ∧ pc s Q = pc s2 Q .

It should be instead:
pc s Q is now defined such that e ∧ pc s Q = pc s1 Q and **¬e** ∧ pc s Q = pc s2 Q .

Thanks. The typos are fixed now and will show up in the lecture notes soon.

1 Like