| | | F Grammar |
In this appendix, we give the lexical and the syntactical grammar of the specification language and the prover commands. The syntax is given in the notation of the ANTLR parser generator [13] used for the implementation of the system. Non-determinism in the syntax is resolved by extra means provided by ANTLR (like semantic predicates) which are not shown in this presentation.
| | | F Grammar |