Editing Guarded Command Language (section)

==[[Conditional (programming)|Selection]]: if==

The selection (often called the "conditional statement" or "if statement") is a list of guarded commands, of which one is chosen to execute. If more than one guard is true, one statement whose guard is true is arbitrarily chosen to be executed. If no guard is true, the result is undefined, that is, equivalent to '''abort'''. Because at least one of the guards must be true, the empty statement '''skip''' is often needed. The statement '''if fi''' has no guarded commands, so there is never a true guard. Hence, '''if fi''' is equivalent to '''abort'''.

===Syntax===
 '''if''' G0 → S0
  □ G1 → S1
 ...
  □ Gn → Sn
 '''fi'''

===Semantics===
Upon execution of a selection, the guards are evaluated. If none of the guards is ''true'', then the selection aborts, otherwise one of the clauses with a ''true'' guard is chosen arbitrarily and its statement is executed.

===Implementation===
GCL does not specify an implementation. Since guards cannot have [[Side effect (computer science)|side effects]] and the choice of clause is arbitrary, an implementation may evaluate the guards in any sequence and choose the first ''true'' clause, for example.

===Examples===
====Simple====
In [[pseudocode]]:
 if a < b then set c to True
 else set c to False

In guarded command language:
 '''if''' a > b → c := true
  □ a < b → c := false
 '''fi'''

====Use of skip====
In pseudocode:
 if error is True then set x to 0

In guarded command language:
 '''if''' error → x := 0
  □ {{not}}error → '''skip'''
 '''fi'''

If the second guard is omitted and error is False, the result is abort.

====More guards true====
 '''if''' a ≥ b → max := a
  □ b ≥ a → max := b
 '''fi'''

If a = b, either a or b is chosen as the new value for the maximum, with equal results. However, the [[implementation]] may find that one is easier or faster than the other. Since there is no difference to the programmer, any implementation will do.