The Iterative Command
Do B ? S oD
- where B ? S is a guarded command. This is equivalent to a while loop.
- Do (x>=0) ? x:= x-1 oD
? while (x>=0) { x := x-1}
We can generalize in the guarded command language to:
Do B1 ? S1
[] B2 ? S2
…
[] Bn ? Sn
oD where n>=0, and Bi ? Si is a guarded command.
Note: Non Determinism is allowed.