Search code examples
assertverificationproofcorrectness

Verification: combining correctness statements

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...

Solution

  • 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.