N.B. When a declared parameter is merely a SPEC-NAME, it refers
to an existing specification definition in the global
environment--it is not a local name for an argument
specification. A declared parameter, whatever its form, essentially
just specifies the signature and sentences that the body of the
generic specification may assume to be provided by the corresponding
argument specification that is supplied when referencing the generic
specification. Thus the parameter specification corresponds more to
the type of the argument than to a formal parameter.
A fitting argument FITTING-ARG fits the argument specification
SPEC to the corresponding parameter specification via a signature
morphism SIG-MORPH. An omitted SIG-MORPH construct is taken
to be the identity morphism.
When there is more than one parameter, the fitting argument morphisms
have to be compatible, with all of them extending to a single
morphism, including moreover any fitting morphism SIG-MORPH that
is specified as a component of the enclosing SPEC-INST. Thus any
common parts of declared parameters have to be instantiated in the
same way. It is pointless to declare the same parameter twice in a
generic specification. (Generic specifications that require two
similar but independent parameters can be expressed by using a
translation to distinguish between the symbols in the signatures of
the two parameters.)
The semantics of a well-formed instantiation SPEC-INST is the
same as that of the specification determined as follows: the fitting
morphisms are extended to a single morphism applicable to the
signature of the entire generic specification GEN-SPEC named by
the SPEC-NAME, any persistency and freeness requirements are
checked,
When such a compound identifier is used to name, e.g., a sort in the
body of a generic specification, the translation determined by fitting
arguments to parameters applies to the components ID+ of the
compound identifier as well. Thus instantiations with different
arguments generally give rise to different compound identifiers for
what would otherwise be the same sort, which avoids unintended
identifications when the instantiations are united.
E.g., a generic specification of sequences of arbitrary elements might
use the simple identifier Elem for a sort in the parameter, and a
compound identifier compound-id Seq Elem for the sort of
sequences in the body. Fitting various argument sorts to Elem in
different instantiations then results in distinct sorts of sequences.
Subsort embeddings between component sorts induce subsort embeddings
between the compound sorts. For example, when Nat is declared as
a subsort of Int, we get automatically (compound-id Seq Nat)
embedded as a subsort of (compound-id Seq Int) in signatures
containing all these sorts.
The details of the intended relationship between compound identifiers
and other constructs (such as translations and reductions) have still
to be decided.
A specification definition SPEC-DEFN provides a name
SPEC-NAME for a (possibly generic) specification GEN-SPEC.
SPEC-DEFN ::= spec-defn SPEC-NAME GEN-SPEC
SPEC-NAME ::= SIMPLE-ID
The abstract syntax of a generic specification GEN-SPEC is
similar to those of an EXTENSION: each declared parameter is an
OF-SPEC, so persistency may be required by use of a
PERSISTENT-SPEC, and freeness of the body SPEC may be
specified by use of a FREE-SPEC. The well-formedness and
semantics of GEN-SPEC are essentially as for the corresponding
EXTENSION, the only difference being that a fitting argument has
to be supplied for each declared parameter when referencing a
GEN-SPEC through its name, as explained below. A GEN-SPEC
with an empty OF-SPEC* list may be regarded as an ordinary,
non-generic specification.
GEN-SPEC ::= gen-spec OF-SPEC* SPEC
A specification instantiation SPEC-INST refers to the
possibly-generic specification named SPEC-NAME in the global
environment, providing a fitting argument FITTING-ARG for each
declared parameter (in the same order).
SPEC ::= ... | SPEC-INST
SPEC-INST ::= spec-inst SPEC-NAME FITTING-ARG* SIG-MORPH?
FITTING-ARG ::= fitting-arg SPEC SIG-MORPH?
[HB]
A SPEC-NAME is used to name either a generic-, unit-
or architectural specification. Therefore, any context that uses a
SPEC-NAME (these are SPEC-INST and UNIT-SPEC)
must handle each type of specification. So here in SPEC-INST we
must also handle the case where SPEC-NAME denotes a unit- or
architectural- instead of a generic specification. One can use
context conditions to avoid these problems or use an implicit
coercion. But I think a more elegant solution is to use the abstract
syntax by having non-terminals for the names of each type of
specifications (SPEC-NAME, UNIT-SPEC-NAME and
ARCH-SPEC-NAME), modifying productions that make use of
SPEC-NAME accordingly
and making explicit any coercion between the types of specifications.
See comment by AT in
a later
section.
Discharged:
The suggestion to have three categories of specification names
(SPEC-NAME, UNIT-SPEC-NAME and ARCH-SPEC-NAME)
is adopted.
An architectural specification may be used where a SPEC is
required; this coerces to the set of all resulting units obtainable
using the permissible realizations of the component units.
[AT]
The last phrase seems highly misleading and inappropriate
-- I think it should just be deleted. The persistency and freeness
requirements, if any, are a part of the GEN-SPEC, and "are
checked" when its semantics is determined. They have nothing to do
with the instantiation of a generic specification to an actual
argument.
Discharged:
Adjust presentation accordingly.
then the translation of it by this morphism is united with
all the argument specifications.
[TM]
The semantic domain of GEN-SPECs is unclear.
The above paragraph mixes up the syntactical construction
of a specification (the denotation of a SPEC-INST)
and model-theoretical issues ("any persistency and freeness
requirements are checked"). What are the model classes and the reduct
functors w.r.t. which the persistency and freeness requirements are
checked?
Discharged:
With a different presentation (see previous comment) this becomes
irrelevant.
This extension of the syntax of identifiers for sorts, functions, and
predicates is of relevance to generic specifications. In a compound
identifier COMPOUND-ID, the components may (but need not)
themselves identify sorts, functions, or predicates that are specified
in the declared parameters of a generic specification.
ID ::= ... | COMPOUND-ID
COMPOUND-ID ::= compound-id SIMPLE-ID ID+
[HB]
Is it possible to put these into the definition of
signature and signature morphism of the base institution? Otherwise,
the semantics of REDUCTION and TRANSLATION has to be
adjusted w.r.t. compound identifiers and signature morphisms
involving compound identifiers.
Discharged:
We don't automatically extend signature morphisms to compound
identifiers.
But we do extend fitting morphisms to compound identifiers in
the body. This is the only place where compound identifiers aren't
regarded as atomic.
[TM]
What happens if there are multiple components?
(If there are two compound sorts with multiple components, and the number
of components are the same, and each pair of corresponding components
either consist of two identical IDs or of two sorts in the
subsort relationship, then there also is a subsort embedding between
the compound sorts.)
Discharged:
The ordering isn't required to be extended to compound identifiers.
So we can have e.g. nat<int and
list(nat)/<list(int).
[PDM]
The interaction is unclear.
Discharged:
There is no interaction.
[TM]
Should the hiding of a component also hide the compound id?
(No, since the component id need not be a sort, function or predicate
name.)
Discharged:
This is right.
[AT]
See
ftp://ftp.brics.dk/Projects/CoFI/Notes/S-2.txt
for discussion and a proposal, wherein we
suggest not to extend the use of (compound or simple) identifiers in
SIG-MORPHs and reduction lists to compound identifiers they are
contained in at all. The only exception is in the semantics of
instatiation of generic specs, where something special is happening
-- and a mapping between (compound or simple) identifiers as given in
a fitting SIG-MORPH is extended to compound identifiers in the
obvious way.
Discharged:
This is what we do -- see comments above.
Higher-order extensions of CASL are expected to
provide a more semantic treatment of parametrized sorts, etc.
CoFI
Note: S-1 --Version 1.3-- 25 April 1997.
Comments to cofi-semantics@brics.dk