Meaning of square brackets in Alloy grammar spec

Question

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 paragraphs. 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?

Answer 1

question 1: what do square brackets indicate in the grammar?

You rightly pointed out that the use of square brackets is inconsistent in the grammar you referred to. I think that grammar was copied from the first edition of the "Software Abstractions" book; I'm not sure if the second edition of the book contains the same grammar.

Question 2: is the use of square brackets where some readers might expect parentheses a typo?

Exactly right.

Question 3: is this notation used by some parser generation tool? Which?

It is not. The Alloy Analyzer uses a grammar written in Cup. The .lex and .cup files (Alloy.lex and Alloy.cup) are included in the Alloy distribution jar file (located in "edu/mit/csail/sdg/alloy4compiler/parser/").

Answer 2

Thanks, Michael. The production for cmdDecl was indeed wrong in the book, so I've posted an erratum. Aleks has also updated the grammar on the Alloy website, which had a couple of other errors.