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

2

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

.