[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[CoFI] Revised proposal for named morphisms in CASL (250 lines)
Dear all,
The following is a, necessarly biased, view :-) on the results of the
discussions about named morphisms for CASL by Peter, Didier, Till,
Don, Bernd, Andrzej and me. Note that it does not cover architectural
specifications.
[Many thanks to Hubert for providing this summary of the recent
intensive discussions! Although the deadline for comments on the
initial proposal (23 January) has now passed, this part of the CASL
design is still rather new, and the impact on the rest of the language
is limited, so comments and objections to this revised proposal are
welcome - as are suggestions for concrete syntax for views. Please
send these to cofi-language@brics.dk as soon as possible, and in any
case before
DEADLINE: MONDAY 23 FEBRUARY 1998!
Comments based on experience of using named morphisms/views in
other languages (OBJ3, LPG, SPECWARE) are particularly welcome!
--PDM]
1. Views
--------
VIEW-DEFN ::= view-defn VIEW-NAME VIEW-SPEC
VIEW-SPEC ::= view-spec SPEC-NAME SPEC-NAME SYMB-MAP*
VIEW ::= VIEW-NAME
VIEW-NAME ::= SIMPLE-ID
A view (VIEW) is a specification morphism from a named
specification (the source) to another named specification (the
target), given by SYMB-MAP*, together with the name of the source
and the name of the target. It is required that the reduct by the
specification morphism of each model of the target is a model of
the source.
1.1. Using views as fitting arguments
-------------------------------------
FITTING-ARG ::= fitting-arg SPEC SYMB-MAP*
| fitting-view VIEW
A view defines a fitting morphism and an actual parameter when
used to instantiate a formal parameter of a generic
specification. The FITTING-ARG is well-formed if the name of the
corresponding formal parameter is the same name as the source of
the view. The actual parameter specification is the target of the
view.
Note that checking if a view can be used as a fitting morphism
only depends on the names of the involved specificatons and thus
no semantic check is need to ensure the applicability of a view.
If the generic specification has an import declaration then the
fitting morphism is the union of the specification morphism given
by view and the identity on the import. The actual parameter is
the union of the target of the view and the import.
It would be possible to explicitly state the actual parameter of
the FITTING-ARG, as for example with (fitting-view view
SPEC-NAME). However this is redundant, because the actual
parameter is uniquely determined by the target of the view.
Having the semantics of views being specification morphisms
ensures that if an instantiation of a generic specification using
views is well-formed then the semantics is defined. Thus the
semantics need not check that the models of the actual parameter
are models of the formal parameter.
1.2. Implicit application of views
----------------------------------
FITTING-ARG ::= ... | fitting-spec SPEC-NAME
If the actual parameter and also the formal parameter are named
specifications and there exists a unique view definition in the
global environment with source name the same as the formal
parameter name and target name the same as the actual parameter
name then the fitting morphism is given as the specification
morphism of that view.
2. Generic Views
----------------
GEN-VIEW-DEFN ::= gen-view-defn GEN-VIEW-NAME GEN-VIEW
GEN-VIEW ::= gen-view SPEC-NAME GEN-SPEC-NAME SYMB-MAP*
GEN-VIEW-NAME ::= SIMPLE-ID
The generic view (GEN-VIEW) is a specification morphism from a
named specification to the body of a named generic specification
defined by SYMB-MAP* together with the names of the source
specification and target generic specification.
2.1. Instantiation of generic views
-----------------------------------
VIEW ::= ... | GEN-VIEW-INST
GEN-VIEW-INST ::= gen-view-inst GEN-VIEW-NAME FITTING-ARG+
The instantiation of a generic view yields a view whose source is
the source of the generic view and whose target is the result of
the instantiation of the target of the generic view wrt. the
fitting morphisms defined by FITTING-ARG+. The specification
morphism is the composition of the specification morphism of the
generic view with the morphism from the body of a generic
specification to the result of its instantiation induced by the
fitting morphisms.
2.2. Using instantiated generic views as fitting arguments
----------------------------------------------------------
Note that the source name of the instantiation of a generic view
is given by the source name of the generic view. Therefore we can
use the instantiation of a generic view as a fitting argument.
However, the instantiation has no target name associated with it,
because the target of the instantiation is the instantiation of a
generic specification.
Thus the instantiation cannot take part in the search for an
implicit view as described above, even if we could name the
instantiation of a generic view, which, in this proposal, we
cannot.
A proposal by Didier allows both, the source and the target of a
generic view, to be generic specifications. However, in this case
the source of an instantiated generic view would be an
instantiated generic specification and thus the applicability of
a view as a fitting morphism could not rely on the names of
specifications only.
2.3. Implicit application of generic views
------------------------------------------
If the actual parameter in the instantiation of a generic
specification is again the instantiation of a generic
specification and there exists a unique generic view from the
name of the formal parameter to the name of the generic
specification used in the actual parameter then the fitting
morphism is given by the instantiation of the generic view with
the same fitting morphism which was used in the instantiation of
the actual parameter.
If the semantics of SPEC is changed to include the way
specifications are built from named specifications and
instantiation of generic specifications we could use the abstract
syntax:
FITTING-ARG ::= fitting-arg SPEC SYMB-MAP*
and could check for the possibility of an implicit application of
views and generic views if SYMB-MAP* is empty.
However, without changing the current semantics of SPEC one can
use
FITTING-ARG ::= ... | fitting-gen-spec GEN-SPEC-NAME FITTING-ARG+
to achieve the same effect.
Consider Didier's example [without worrying about concrete syntax! --PDM]:
spec EQ =
BOOL then
sort t
ops eq : t*t -> bool
...
end
spec LIST [EQ] =
sort list[t]
ops nil : list[t];
...
__==__ : list[t]*list[t] -> bool;
...
end
view Eq-List [EQ] =
EQ --{ t |-> list[t], eq |-> __==__ }--> LIST [EQ]
view Eq-Nat =
EQ --{ t |-> nat, eq |-> __==__ }--> NAT
spec MY_LISTS =
LIST[LIST[NAT]] %% or LIST[Eq-List[Eq-Nat]]
then
ops ...
end
The abstract syntax for LIST[LIST[NAT]] is
(gen-spec-inst LIST (fitting-gen-spec LIST (fitting-spec NAT)))
In the global environment there is just one view morphism from EQ
to NAT and thus the fitting morphism determined by (fitting-spec
NAT) is Eq-Nat. Also in the global environment there is just one
generic view morphism from EQ to LIST, Eq-List[EQ]. Thus the
fitting morphism from EQ to LIST[NAT] is given by the
instantiation of Eq-List[EQ] with Eq-Nat.
3. Using views for purposes other than as fitting morphisms
-----------------------------------------------------------
Views for TRANSLATION and REDUCTION are useless since the result
would be the target or the source of a view, which are named
specifications and could be written directly instead of the
TRANSLATION and REDUCTION.
4. Remarks
----------
A problem with the implicit application of views and generic
views is noted by Don:
I am generally very wary of conventions whereby missing stuff is
automatically inferred on the grounds that only one thing of the
appropriate kind has been defined so far. The problem with this,
as I think I have discussed with Bernd back in the SPECTRAL days,
is that the well-formedness and/or meaning of phrases can change
when things that are not involved in any way in the phrase in
question are changed later. This is an undesirable property which
ML-style type inference does *not* possess.
For instance, suppose that we have ELEM-WITH-ORDER and a view of
NAT whereby order is mapped to <. Then SORT[NAT] will, under (c),
automatically refer to this view. But if we later decided that it
is useful to have another view as well in which order is mapped
to >, then SORT[NAT] becomes ill-formed. Of course sophisticated
tools can do lots of wonderful things including warning the user
when things like this happen and maybe helping him to fixing
them. I would rather have a sophisticated facility for filling in
things automatically when specs are input by adding things to
specs explicitly. Once they are explicit, the above problem
doesn't arise.
5. Abstract Syntax
------------------
The percent % below denotes the productions that would have to be
removed to eliminate implicit application of (generic) views,
cf. point 4 above.
VIEW-DEFN ::= view-defn VIEW-NAME VIEW-SPEC
VIEW-SPEC ::= view-spec SPEC-NAME SPEC-NAME SYMB-MAP*
VIEW ::= VIEW-NAME
VIEW-NAME ::= SIMPLE-ID
FITTING-ARG ::= fitting-arg SPEC SYMB-MAP*
| fitting-view VIEW
% FITTING-ARG ::= ... | fitting-spec SPEC-NAME
GEN-VIEW-DEFN ::= gen-view-defn GEN-VIEW-NAME GEN-VIEW
GEN-VIEW ::= gen-view SPEC-NAME GEN-SPEC-NAME SYMB-MAP*
GEN-VIEW-NAME ::= SIMPLE-ID
VIEW ::= ... | GEN-VIEW-INST
GEN-VIEW-INST ::= gen-view-inst GEN-VIEW-NAME FITTING-ARG+
% FITTING-ARG ::= ...| fitting-gen-spec GEN-SPEC-NAME FITTING-ARG+
--
Hubert Baumeister
MPI Informatik, Im Stadtwald, D-66123 Saarbr"ucken, Germany
Phone: (x49-681)9325-220 Fax: -299
e-mail: hubert@mpi-sb.mpg.de
WWW: http://www.mpi-sb.mpg.de/~hubert/