Revision

if$$(\alpha) \;$$then$$\; \{P_1\} \;$$else$$\; {P_2}$$

is a piece of code. It acts as expected on the state $x$: if $\alpha$ is true at $x$ then the output agrees with that of $P_1$, otherwise it agrees with $P_2$'s.

Also used is if-then without ``else'': if$(\alpha)\;$then$\;\{P_1\}$ is a piece of code which, if the input $x$ satisfies $\alpha$, gives the same output as $P_1$, otherwise the output is $x$ itself.

Note: the underlining in $x$ means its a vector