Verification: combining correctness statements

Question

The question is:

        P1 {C} Q1
-------------------------
   P1 && P2 {C} Q1||Q2

Is this rule valid?

How would I go about tackling something like this? All I can think of is to try to find an example where it would be false.

I've been trying to come up with it so that the combination of P1 && P2 make both Q1 and Q2 false but I cant think of any. So im leaning towards this being valid, but I dont know where to go about proving it... The text for this class is absolute rubbish and I can't find any resources online for combination of correctness statements...

Answer 1

I'm assuming these are Hoare triples, normally denoted {P} C {Q}; I also use Wikipedia as a reference.

So your rule:

      {P1} C {Q1}
-----------------------
{P1 && P2} C {Q1 || Q2}

is valid!

Intuitively it is quite clear if you unterstand the logic:

• {P1} C {Q1} means: Whenever P1 holds, Q1 will hold after executing command C.
• You know that if P1 && P2 holds, P1 holds.
• You know that if Q1 holds, Q1 || Q2 holds.

You can piece these statements together to see, why your rule must be valid: P1 && P2 implies P1, so when you execute C, you get by assumptionQ1, which implies Q1 || Q2.

Therefore {P1 && P2} C {Q1 || Q2}, whenever you assume {P1} C {Q1}, which is exactly what your rule states.

Formally you can use the following rule (excerpt from Wikipedia):

Consequence rule

P' -> P, {P} C {Q}, Q -> Q'
---------------------------
        {P'} C {Q'}

where you simply set P' as P1 && P2, P as P1, Q as Q1 and finally Q' as Q1 || Q2.