3 Proposal for static semantic checker annotaions

• Error messages
• For each specification, a list of directly inherited specifications and a signature fragment (including precedence annotations?). It is not feasible to store the whole signature for each specification. But the signature of the specification can then be computed by computing the signatures of the inherited specifications, and uniting the union of them with the signature fragment.

  However, note that in the case of modified inheritance, like renaming, it seems to be more efficient to generate an entirely new (renamed) specification instead of storing the original specification plus the symbol map.²

• For each operation symbol, predicate symbol and variable occurring in an axiom, its profile (or sort, in case of variables). Thus, from the original axiom, with the help of these annotations, one gets the corresponding fully-qualified sentence in SubPCFOL, the underlying institution of CASL.
• For each construct (like datatypes) that is defined in terms of some other constructs, the set of constructs generated by translating the original construct (note that some tools may want to work directly on the original constructs).
• For each construct with a dynamic (i.e. generally undecidable) well-formedness condition, the list of proof obligations that have to be discharged in order to guarantee well-formedness (e.g. compatibility for generic instantiations and views). A theorem prover may then be used to discharge these proof obligations.
• For each library-item, the set of referenced named specifications (only direct references).

Acknowledgements

I wish to thank the CoFI tools task group for the discussion in Bremen in January 1998 which directly motivated me to write this note. The note was revised according to the discussion at the tools group meeting in April 1998 in Lisbon.