alloy - 合金语法规范中方括号的含义

Question

在 the Alloy grammar spec在 Alloy 网站上，我发现自己对方括号的使用感到困惑。

在如下所示的制作中，事情似乎很清楚。

specification ::= [module] open* paragraph*

我猜方括号表示可选性，星号是 Kleene 闭包，因此刚才引用的规则意味着规范最多包含一个 module 语句、零个或多个 open 子句，以及零个或多个段落。这对我来说很有意义(尽管我逐渐开始尽可能使用 Wirth 的 EBNF 表示法，因此我的笔记将其显示为 [module] {open} {paragraph})。

但是，在下面的制作中，括号让我感到困惑。

cmdDecl ::= [name ":"] ["run"|"check"] [name|block] scope

如果关键字 run 和 check 在命令中是可选的，我会感到非常惊讶，并且要运行的谓词的名称、要检查的断言，或者要运行或检查的匿名 block 。但这似乎就是这条规则所说的。

问题 1:方括号在语法中表示什么？

问题 2:在某些读者可能认为括号的地方使用方括号是否是拼写错误？ IE。该规则应该采用以下形式吗？

cmdDecl ::= [name ":"] ("run"|"check") (name|block) scope

也许我只是对野外发现的各种语法符号不够熟悉；也许指出该工具或指出符号的描述会有所帮助。

问题 3:某些解析器生成工具是否使用此表示法？哪个？

Answer 1

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?

完全正确。

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

事实并非如此。合金分析器使用用 Cup 编写的语法。 .lex 和 .cup 文件(Alloy.lex 和 Alloy.cup)包含在 Alloy 分发 jar 文件中(位于“edu/mit/csail/sdg/Alloy4编译器/解析器/")。