The if statement
If B1 ? S1
[] B2 ? S2
… [] Bn ? Sn
Each Bi ?Si is a guarded command and each Si may be any command e.g. skip, about, sequential composition etc.
If any guard Bi is not well defined in the state in which execution begins, abortion may occur. This is because nothing is assumed by the order of evaluation of the guards.
At least one guard must be true to avoid abortion.
If at least one guard Bi is true, then 1 guarded command Bi ?Si is chosen and Si is executed.