In the Alloy grammar spec on the Alloy Web site, I find myself confused by the use of square brackets.
In a production like the following, things seem clear.
specification ::= [module] open* paragraph*
I guess the square brackets indicate optionality and that the asterisks are Kleene closures, so that the rule just quoted means a specification consists of at most one module
statement, zero or more open
clauses, and zero or more paragraph
s. This makes sense to me (though I am gradually coming to use Wirth's EBNF notation wherever possible, so my notes show this as [module] {open} {paragraph}
).
In the following production, though, the brackets are confusing me.
cmdDecl ::= [name ":"] ["run"|"check"] [name|block] scope
It would surprise me a great deal if the keywords run
and check
were optional in commands, and ditto for the name of the predicate to be run, the name of the assertion to be checked, or the anonymous block to be run or checked. But that's what it looks as if this rule is saying.
So question 1: what do square brackets indicate in the grammar?
Question 2: is the use of square brackets where some readers might expect parentheses a typo? I.e. should this rule instead take the following form?
cmdDecl ::= [name ":"] ("run"|"check") (name|block) scope
Maybe I'm just not familiar enough with the variety of grammatical notations to be found in the wild; perhaps it would be helpful to indicate the tool, or point to a description of the notation.
Question 3: is this notation used by some parser generation tool? Which?