C Concrete Syntax

[DELETED]The relationship between the concrete syntax and the corresponding abstract syntax  [DELETED]is rather straightforward--except that mapping the use of mixfix notation in a concrete ATOM to an abstract ATOM depends on the declared operation and predicate symbols (although not on their profiles). Currently, the relationship is merely suggested by the use of the same nonterminal symbols in the concrete and abstract grammars.

Examples of specifications illustrating the proposed concrete syntax are given in Appendix E. Readers are encouraged to test the proposal on their own specifications. Some prototype parsers for CASL have been implemented:

• Mark van den Brand and Bjarke Wedemeijer have developed a grammar from which the ASF+SDF system can generate a (nondeterministic bottom-up) parser.
• [CHANGED:] Kolyang and Till Mossakowski have implemented a parser, a well-formedness checker, and an encoding into the Isabelle/HOL proof system (currently only for basic specifications). []
• Christophe Tronche has developed a top-down, LL(2) parser.
• Frédéric Voisin has developed a bottom-up, LALR(1) parser.