17. Dafny Grammar {#sec-grammar-details}

The Dafny grammar has a traditional structure: a scanner tokenizes the textual input into a sequence of tokens; the parser consumes the tokens to produce an AST. The AST is then passed on for name and type resolution and further processing.

Dafny uses the Coco/R lexer and parser generator for its lexer and parser (http://www.ssw.uni-linz.ac.at/Research/Projects/Coco)[@Linz:Coco]. See the Coco/R Reference manual for details. The Dafny input file to Coco/R is the Dafny.atg file in the source tree.

The grammar is an attributed extended BNF grammar. The attributed adjective indicates that the BNF productions are parameterized by boolean parameters that control variations of the production rules, such as whether a particular alternative is permitted or not. Using such attributes allows combining non-terminals with quite similar production rules, making a simpler, more compact and more readable grammer.

The grammar rules presented here replicate those in the source code, but omit semantic actions, error recovery markers, and conflict resolution syntax. Some uses of the attribute parameters are described informally.

The names of character sets and tokens start with a lower case letter; the names of grammar non-terminals start with an upper-case letter.

17.1. Dafny Syntax

This section gives the definitions of Dafny tokens.

17.1.1. Classes of characters

These definitions define some names as representing subsets of the set of characters. Here,

double quotes enclose the set of characters constituting the class,
single quotes enclose a single character (perhaps an escaped representation using \),
the binary + indicates set union,
binary - indicates set difference, and
ANY indicates the set of all (unicode) characters.

letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz"

digit = "0123456789"
posDigit = "123456789"
posDigitFrom2 = "23456789"

hexdigit = "0123456789ABCDEFabcdef"

special = "'_?"

cr        = '\r'

lf        = '\n'

tab       = '\t'

space     = ' '

nondigitIdChar = letter + special

idchar = nondigitIdChar + digit

nonidchar = ANY - idchar

charChar = ANY - '\'' - '\\' - cr - lf

stringChar = ANY - '"' - '\\' - cr - lf

verbatimStringChar = ANY - '"'

A nonidchar is any character except those that can be used in an identifier. Here the scanner generator will interpret ANY as any unicode character. However, nonidchar is used only to mark the end of the !in token; in this context any character other than whitespace or printable ASCII will trigger a subsequent scanning or parsing error.

17.1.2. Definitions of tokens {#sec-g-tokens}

These definitions use

double-quotes to indicate a verbatim string (with no escaping of characters)
'"' to indicate a literal double-quote character
vertical bar to indicate alternatives
square brackets to indicate an optional part
curly braces to indicate 0-or-more repetitions
parentheses to indicate grouping
a - sign to indicate set difference: any character sequence matched by the left operand except character sequences matched by the right operand
a sequence of any of the above to indicate concatenation without whitespace

reservedword =
    "abstract" | "allocated" | "as" | "assert" | "assume" |
    "bool" | "break" | "by" |
    "calc" | "case" | "char" | "class" | "codatatype" |
    "const" | "constructor" | "continue" |
    "datatype" | "decreases" |
    "else" | "ensures" | "exists" | "expect" | "export" | "extends" |
    "false" | "for" | "forall" | "fresh" | "function" | "ghost" |
    "if" | "imap" | "import" | "in" | "include" |
    "int" | "invariant" | "is" | "iset" | "iterator" |
    "label" | "lemma" | "map" | "match" | "method" |
    "modifies" | "modify" | "module" | "multiset" |
    "nameonly" | "nat" | "new" | "newtype" | "null" |
    "object" | "object?" | "old" | "opaque" | "opened" | "ORDINAL"
    "predicate" | "print" | "provides" |
    "reads" | "real" | "refines" | "requires" | "return" |
    "returns" | "reveal" | "reveals" |
    "seq" | "set" | "static" | "string" |
    "then" | "this" | "trait" | "true" | "twostate" | "type" |
    "unchanged" | "var" | "while" | "witness" |
    "yield" | "yields" |
    arrayToken | bvToken

arrayToken = "array" [ posDigitFrom2 | posDigit digit { digit }]["?"]

bvToken = "bv" ( 0 | posDigit { digit } )

ident = nondigitIdChar { idchar } - charToken - reservedword

digits = digit {["_"] digit}

hexdigits = "0x" hexdigit {["_"] hexdigit}

decimaldigits = digit {["_"] digit} '.' digit {["_"] digit}

escapedChar =
    ( "\'" | "\"" | "\\" | "\0" | "\n" | "\r" | "\t"
      | "\u" hexdigit hexdigit hexdigit hexdigit
      | "\U{" hexdigit { hexdigit } "}"
    )

charToken = "'" ( charChar | escapedChar ) "'"

stringToken =
    '"' { stringChar | escapedChar }  '"'
  | "@" '"' { verbatimStringChar | '"' '"' } '"'

ellipsis = "..."

There are a few words that have a special meaning in certain contexts, but are not reserved words and can be used as identifiers outside of those contexts:

least and greatest are recognized as adjectives to the keyword predicate (cf. Section 12.4).
older is a modifier for parameters of non-extreme predicates (cf. Section 6.4.6).

The \uXXXX form of an escapedChar is only used when the option --unicode-char=false is set (which is the default for Dafny 3.x); the \U{XXXXXX} form of an escapedChar is only used when the option --unicode-char=true is set (which is the default for Dafny 4.x).

17.2. Dafny Grammar productions

The grammar productions are presented in the following Extended BNF syntax:

identifiers starting with a lower case letter denote terminal symbols (tokens) as defined in the previous subsection
identifiers starting with an upper case letter denote nonterminal symbols
strings (a sequence of characters enclosed by double quote characters) denote the sequence of enclosed characters
= separates the sides of a production, e.g. A = a b c
| separates alternatives, e.g. a b | c | d e means a b or c or d e
( ) groups alternatives, e.g. (a | b) c means a c or b c
[ ] option, e.g. [a] b means a b or b
{ } iteration (0 or more times), e.g. {a} b means b or a b or a a b or ...
We allow | inside [ ] and { }. So [a | b] is short for [(a | b)] and {a | b} is short for {(a | b)}.
// in a line introduces a comment that extends to the end-of-the line, but does not terminate the production
The first production defines the name of the grammar, in this case Dafny.

In addition to the Coco rules, for the sake of readability we have adopted these additional conventions.

We allow - to be used. a - b means it matches if it matches a but not b.
We omit the . that marks the end of a CoCo/R production.
we omit deprecated features.

To aid in explaining the grammar we have added some additional productions that are not present in the original grammar. We name these with a trailing underscore. Inlining these where they are referenced will reconstruct the original grammar.

Files

GrammarDetails.md

Latest commit

History

GrammarDetails.md

File metadata and controls

17. Dafny Grammar {#sec-grammar-details}

17.1. Dafny Syntax

17.1.1. Classes of characters

17.1.2. Definitions of tokens {#sec-g-tokens}

17.2. Dafny Grammar productions

17.2.1. Programs {#g-program}

17.2.1.1. Include directives {#g-include-directive}

17.2.1.2. Top-level declarations {#g-top-level-declaration}

17.2.1.3. Declaration modifiers {#g-declaration-modifier}

17.2.2. Modules {#g-module}

17.2.2.1. Module Definitions {#g-module-definition}

17.2.2.2. Module Imports {#g-module-import}

17.2.2.3. Module Export Definitions {#g-module-export}

17.2.3. Types {#g-type}

17.2.3.1. Basic types {#g-basic-type}

17.2.3.2. Generic instantiation {#g-generic-instantiation}

17.2.3.3. Type parameter {#g-type-parameter}

17.2.3.4. Collection types {#g-collection-type}

17.2.3.5. Type definitions {#g-type-definition}

17.2.3.6. Class type {#g-class-type}

17.2.3.7. Trait types {#g-trait-type}

17.2.3.8. Object type {#g-object-type}

17.2.3.9. Array types {#g-array-type}

17.2.3.10. Iterator types {#g-iterator-type}

17.2.3.11. Arrow types {#g-arrow-type}

17.2.3.12. Algebraic datatypes {#g-datatype}

17.2.4. Type member declarations {#g-member-declaration}

17.2.4.1. Fields {#g-field-declaration}

17.2.4.2. Constant fields {#g-const-declaration}

17.2.4.3. Method declarations {#g-method-declaration}

17.2.4.4. Function declarations {#g-function-declaration}

17.2.5. Specifications

17.2.5.1. Method specifications {#g-method-specification}

17.2.5.2. Function specifications {#g-function-specification}

17.2.5.3. Lambda function specifications {#g-lambda-specification}

17.2.5.4. Iterator specifications {#g-iterator-specification}

17.2.5.5. Loop specifications {#g-loop-specification}

17.2.5.6. Requires clauses {#g-requires-clause}

17.2.5.7. Ensures clauses {#g-ensures-clause}

17.2.5.8. Decreases clauses {#g-decreases-clause}

17.2.5.9. Modifies clauses {#g-modifies-clause}

17.2.5.10. Invariant clauses {#g-invariant-clause}

17.2.5.11. Reads clauses {#g-reads-clause}

17.2.5.12. Frame expressions {#g-frame-expression}

17.2.6. Statements {#g-statement}

17.2.6.1. Labeled statement {#g-labeled-statement}

17.2.6.2. Non-Labeled statement {#g-nonlabeled-statement}

17.2.6.3. Break and continue statements {#g-break-continue-statement}

17.2.6.4. Block statement {#g-block-statement}

17.2.6.5. Return statement {#g-return-statement}

17.2.6.6. Yield statement {#g-yield-statement}

17.2.6.7. Update and call statement {#g-update-and-call-statement}

17.2.6.8. Update with failure statement {#g-update-with-failure-statement}

17.2.6.9. Variable declaration statement {#g-variable-declaration-statement}

17.2.6.10. Guards {#g-guard}

17.2.6.11. Binding guards {#g-binding-guard}

17.2.6.12. If statement {#g-if-statement}

17.2.6.13. While Statement {#g-while-statement}

17.2.6.14. For statement {#g-for-statement}

17.2.6.15. Match statement {#g-match-statement}

17.2.6.16. Assert statement {#g-assert-statement}

17.2.6.17. Assume statement {#g-assume-statement}

17.2.6.18. Expect statement {#g-expect-statement}

17.2.6.19. Print statement {#g-print-statement}

17.2.6.20. Reveal statement {#g-reveal-statement}

17.2.6.21. Forall statement {#g-forall-statement}

17.2.6.22. Modify statement {#g-modify-statement}

17.2.6.23. Calc statement {#g-calc-statement}

17.2.6.24. Opaque block {#g-opaque-block}

17.2.7. Expressions

17.2.7.1. Top-level expression {#g-top-level-expression}

17.2.7.2. Equivalence expression {#g-equivalence-expression}

17.2.7.3. Implies expression {#g-implies-expression}

17.2.7.4. Logical expression {#g-logical-expression}