|Portability||mostly portable (deriving extensions)|
A language with guarded commands, heavily based on:
- Edsger W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18, 8 (August 1975), 453–457. DOI=10.1145/360933.360975
With regards to the above source, the following assumptions were made:
- Guarded command sets may be empty, and __skip__ and __abort__ are keywords.
- The __while__ guard __do__ stmts... __od__ notation used on page 457 is allowed and is syntactic sugar for __do__ guard __→__stmts... __od__.
Furthermore, the language is extended so that the blocks denoted by __do__ ... __od__ may be preceded by zero or more loop invariants (written: __invariant__ guard).
- data GCL stmt guard
- data GC stmt guard = GC guard [GCL stmt guard]
- pGCL :: TokenParsing m => m stmt -> m guard -> m (GCL stmt guard)
- pGuardedCommandSet :: TokenParsing m => m guard -> m (GCL stmt guard) -> m [GC stmt guard]
- pGuardedCommand :: TokenParsing m => m guard -> m (GCL stmt guard) -> m (GC stmt guard)
- pGuardedList :: TokenParsing m => m (GCL stmt guard) -> m [GCL stmt guard]
|Alternative [GC stmt guard]|
Alternative statement. If none of the guards is true, the command diverges; otherwise, an arbitrary guarded list with a true guard is executed.
|Repetitive [guard] [GC stmt guard]|
Repetitive statement. If none of the guards is true, the command terminates; otherwise, an arbitrary guarded list with a true guard is executed (the 'iteration'), after which the entire repetitive statement is executed again. Before and after every iteration, all loop invariants must hold.
Some user-defined statement.
Parsers based on the
the keywords (
words "⫾ → if fi do od abort skip invariant while ")
may take on different forms or even be forbidden.
Parse a guarded statement, given parsers for user-defined statments and for guards.
Parse a guarded command set, given parsers for guards and guarded statements.
The guarded commands are separated by a 'white vertical bar' (U+2AFE) symbol, a.k.a. 'Dijkstra choice'.
Parse a guarded command, given parsers for guards and guarded statements.
The guard and the guarded list are separated by a 'rightwards arrow' (U+2192) symbol.