Go up to 5 Our Proposal More in Detail
Go forward to 5.2 Abstract Syntax
5.1 Parameter Typing
The properties we want to be able to express to qualify
the parameters are basically:
- the minimal syntax of the parameters in order to be able to write
down the body of the generic specification.
The syntactical elements can be distinguished in
- meta-variables, that are names for "generic" sorts, functions and
predicates that are intended to be instantiated on any actual element of
the syntax present in the actual parameter signatures.
For instance in the parameter ELEM for, say, an array generic
specification, the elem sort is intended to be a token for the
actual sort that will be used in the instantiation.
- meta-constants, that are names for sorts, functions and predicates
that are intended to belong to the actual parameter signatures in any
instantiation.
For instance in the parameter ELEM-WITH-COST the NAT part, used to
describe the target of the weight function, is supposed to be part
of the actual parameter.
- the properties required on the minimal syntax.
Therefore, the information needed to qualify a parameter consists of a
specification, where the symbol of the signature are classified into
generic (the meta-variables) and fixed (the meta-constants).
Obviously not any such classification is sensible. For instance, a
generic sort cannot appear in the profile of a fixed function.
>From methodological analysis, it appears that the fixed symbols
usually form, or better are imported from, the signature of already defined
specification(s) used to build the overall parametr type, like NAT,
BOOL and such.
This is basically the rationale behind the typing system we propose in
the sequel.
CoFI
Note: L-3 --DRAFT, Version 0.2-- 21 May 1997.
Comments to cerioli@disi.unige.it