I have this derivation
(b,σ)→false (skip,σ)→σ
(if b then c;w else skip)→σ
(With the top line being the precondition and the bottom line the expression)
Does the expression mean:
If b is True, then do command c, else do w and skip,
or
If b is True, then do command c and command w, else skip.
The semi-colon in the middle is confusing me?!
Also, why don't I have to include c in the precondition?
Thanks.
Every operational semantics is different and the question specifies no context, so I can only guess at the answer.
I would parse if b then c; w else skip
as if b then {c; w} else skip
, that is, the second interpretation from the question. The derivation seems to be about the case that b
is false, so c
is not mentioned because if b
is false, c
is not executed. Instead, skip
is mentioned because it's executed.