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...
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.P1 && P2 holds, P1 holds.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.