Prev Up Next
Go backward to 2 Annotations to be handled uniformly
Go up to Top
Go forward to 4 Solution adopted for the INKA frontend

3 Comments and special purpose annotations

According to the language summary, `[c]omments may be inserted anywhere (between other lexical symbols)' [CoF98, C-10]. Using flex and bison this is typically achieved by not including the comments in the sequence of lexemes. Given the assumptions of Sec. 1 this effectively prevents comments from being represented in the AST. For some tools this might be acceptable, for others it might not. This also applies to special purpose annotations added for the convenience of certain tools but not defined by the language specification if only these annotations have a uniform syntax: they can be excluded from the lexeme sequence by tools that do not use the annotations.

As an example, a theorem prover might operate on rewrite rules derived from axioms of the specification but might not use the comments for the axioms. On the other hand a pretty printer will want to print the axioms together with their comments.

Alternatively, there is of course the possibility of also including comments and special purpose annotations explicitly in the concrete syntax of CASL. This is hard, however: allowing these in too few places restricts the specification writer to a narrow range of possible documentation and annotation styles; allowing them in too many places makes the grammar awkward (as can be seen from the short example in the preceding section) and very probably ambiguous.


CoFI Note: T-7 -- Version: 1 -- 28 April 1999.
Comments to schairer@dfki.de

Prev Up Next