Go backward to 2 Proposal for parser standard annotations
Go up to Top
Go forward to Footnotes
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.2
- 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
- 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
(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).
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.
Note: T-6 -- Version: Version 1.1 -- 30 September 1998.
Comments to email@example.com