1 Introduction

1. Tools working on CASL specifications as text strings, like text editors and parsers. Parsers check if a specification is covered by the CASL grammar and procude an annotated abstract syntax tree.
2. Tools that work on an abstract syntax tree corresponding to a syntactically correct specification that is however not necessarily well-formed according to static semantics. Structure editors, pretty printers and static semantic checkers fall into this category. Static semantics checkers check if a CASL specification (given by an abstract syntax tree) is well-formed due to the rules of static semantics. They enrich the abstract syntax tree with further annotations containing the static semantic information.
3. Tools working on an abstract syntax tree corrsponding to a well-formed specification. Examples are theorem provers, rewriters, transformation tools, translators to other languages (such as other specification formalism or sublanguages or kernel languages of CASL).

Some people may question the distinction between 1 and 2 because they want to do parsing and static semantic analysis in one step. Nevertheless, the distinction between 1/2 and 3 should be relevant to everybody.

We claim that there is a need to standardize annotations resulting from parsers and static semantic checkers (or, if you wish, from the combination of both). With such a standard, tools in category 3 may be written independently of the tools chosen in categories 1 and 2. Ideally, one would be able to combine any tool of category 3 with any front-end-tool for category 1 and 2. The standard annotations then serve as a uniform interface between tools. (And for those situations where a distinction between 1 and 2 is useful, an analogous argument applies here.)

The standard annotations should be extendible: Tools of all categories may of course use more specialized annotations that are not recognized by all other tools. But these should be recognizable as such, so they can safely be ignored by tools not supporting them. More specialized annotations such as translations to kernel languages, to other languages, rewrite rule orientation etc. could be standardized as well, by establishing some registration procedure. But the standard annotations contained in this note are regarded to be essential outcomes of parsing and static semantic checking, so any tool guaranteeing the well-formedness of a CASL specification will have to produce them. Moreover, all annotations that are necessary to guarantee correctness should be standard annotations (for examples, annotations for proof obligations and annotations expressing that a proof obligation has been successfully discharged).

Interchange formats should be checked how good they can represent the standard annotations. An argument in favour of A-terms is that they support extendible annotations. At the Lisbon meeting, it was decided to use some A-terms-based format as interchange format.

A further question is whether there is a distinction between user-specificied and tool-generated annotations. Clearly, there will be annotations that can only be user-specified (like precedence of operators), as well as annotations that will only be tool-generated (like the current signature). But there can also be annotations that are sometimes user-specified and sometimes tool-generated (for example, annoations for simplication orderings). The origin of an annotation (user or tool, and which tool) should be part of the annotation (but may be kept invisible to the user).