Search code examples
semantics

Understanding Operational semantics


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.


Solution

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