### Verification: combining correctness statements

1

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

2012-04-03 21:30
by kbirk

2

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

``````      {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 assumption`Q1`, 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`.

2012-04-03 22:27
by Anthales