H.  Grammars

In this appendix, we describe the concrete syntax of the programming language and of the specification language. The grammars are given in the notation of the parser generator ANTLR v3 [1] used for the implementation of the parser and of the lexical analyzer. Non-determinism in grammatical rules is resolved by extra means provided by ANTLR (in particular semantic predicates) which are omitted from this presentation. On the level of the programming language described in Section H.1, every specification annotation is lexically parsed as a comment yielding the token ANNOTATION; the actual grammar of the various kinds of annotations is described in Section H.2 under the header “specifications” by the syntactic domains unitspec, methodspec, loopspec, and statementspec. The grammar of theory declarations is specified there by the syntactic domain theorydecl.

H.1 Programming Language
H.2 Specification Language