The following syntax is used for the text input of the Guarded Commands Code, starting with a command C.

C ::=

x := a | A[a] := a | skip | C; C | if GC fi | do GC od | continue | break

GC ::=

b -> C | GC [] GC

a ::=

n | s | x | A[a] | A# | a + a | a - a | a * a | a % a | a / a | -a | a ^ a | san(a) | (a)

b ::=

true | false | b & b | b | b | b && b | b || b | !b | a = a | a != a | a > a | a >= a | a < a | a <= a | (b)

Additional notes:

• && and || do short-circut evaluation (i.e. a minimal number of operands are evaluated left to right), the rest of the operators do eager evaluation (i.e. all operands are evaluted).
• A# indicates the number of elements in array A.
• Precedence and associativity rules:
  • Precedence is highest for - (unary minus), then ^, then *, % and /, and lowest for + and -.
  • Precedence is highest for !, then & and &&, and lowest for | and ||.
  • *, %, /, +, -, &, |, &&, and || associate left to right.
  • !, ^, - (unary minus), [], and ; associate right to left.
• Variables x and arrays A match the regular expression [a-zA-Z][a-zA-Z\d_]* and can not be any of the keywords. Furthermore the sets should be pair-wise disjoint, e.g. a variable identifier can not be used both as a variable and an array in the same program.
• Numbers n match the regular expression \d+ and are bound by 2⁵³-1 (JavaScript Number.MAX_SAFE_INTEGER). Negative numbers are passed as unary minus -n.
• Strings s match the regular expression ["][^"]*["]
• A whitespace matches the regular expression [ \u00A0\f\n\r\t\v], with a mandatory whitespace after if␣ and do␣; and before ␣fi and ␣od. Whitespaces are ignored anywhere else.