[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Comments on Michel's note
Dear colleague,
I send below some comments about the note by Michel on parametrized
specifications. At first, my vote for the name :
** my preference is for CASL, but FOCAL can be a good choice too.
Didier
=============================================================================
COMMENTS on the MICHEL's NOTE ON PARAMETRIZED SPECIFICATIONS
============================================================
>----------------------------------------------------------------------------
>I - A first simplified view of parametrized specifications:
>===========================================================
The development is clear and convincing. There is only a point which
should be clarified at the second paragraph of the final ``note'' :
>Moreover, when applying signature morphisms (TRANSLATION, DERIVATION) to
>parametrized specifications, the signature of the formal parameters should
>be left unchanged by these signature morphisms. And when combining a
>parametrized specification with other specifications (e.g. in ``F[X] + SP'',
>or in ``enrich F[X], SP by ...'') we have to check in particular that:
>* either SP is not a specification parameterized by X, and then the
>intersection of its signature with the signature of X should be empty
>* or SP is parameterized by X, hence of the form SP[...,X,...].
It seems that any ``specification expression'' appears in the context of a
specification heading. This specification heading (if generic) presents
(in the sense of theory presentation) the ``formal specifications'' in the
parameter part (PAR+ in the abstract syntax).
So, all the generic specifications used in that context must be
instantiated by ``well-formed specifications'' (optionally with a fitting
morphism), where well-formed specifications are :
either actual non generic specification names (e.g. Integer),
or formal specification names presented in the heading,
or (inductively) generic specifications actualized by well-formed
specifications,
or expressions (UNION,...) of well-formed specifications.
These various instantiation cases are detailed in section II.1 of the Michel's
Note. But, it seems that the conditions on the combination of such
instantiated generic specifications are too restrictive (cf. also the first
paragraph after the abstract syntax). Assume a specification:
spec ELEM-WITH-TWO-ORDERS =
enrich ELEM-WITH-ORDER renaming {< -> leq}
+ ELEM-WITH-ORDER renaming {< -> geq}
... there are one sort : Elem and two operators leq and geq
and inherited axiomatization.
endspec.
and now, we want to build a generic specification like the
COMPOUND-NAMES-ARE-NICE one:
generic spec GEN-COMPOUND-NAMES-ARE-NICE [ELEM-WITH-TWO-ORDERS]
LIST-WITH-SORT[ELEM-WITH-TWO-ORDERS for ELEM-WITH-ORDER where < -> leq]
% leads to a sort List[Elem],
% and a function symbol sort[leq]: List[Elem] -> List[Elem]
+
LIST-WITH-SORT[ELEM-WITH-TWO-ORDERS for ELEM-WITH-ORDER where < -> geq]
% leads to a sort List[Elem],
% and a function symbol sort[geq]: List[Elem] -> List[Elem]
endspec.
This specification does not seem to fulfill the well-formedness conditions.
[The intention was to allow that sort of specification. If the
wording of the well-formedness conditions is such that it seems not to
be allowed, the wording will have to be changed - and made more precise.
--PDM]
I think that all the operations on specifications should be defined in a
general way, for well-formed specifications in a generic context PAR+.
Maybe some restrictions can be applied for example on the target of the
fitting morphism of instantiations.
Example : Would this expression be valid ? :
GEN-SPEC-NAME [SPEC1[...] + SPEC2[...] for PAR where {.....}]
[As far as I can see, yes. --PDM]
>---------------------------------------------------------------------------
>II.1 - Various kinds of instantiations:
>---------------------------------------
The example :
>generic spec STACK[ELEM-WITH-ORDER] =
> STACK[ELEM-WITH-ORDER for ELEM]
>endspec.
should be read :
generic spec ORDERED-STACK[ELEM-WITH-ORDER] =
STACK[ELEM-WITH-ORDER for ELEM]
endspec.
because I think that overloading of specification names is not allowed
(even if this could be interesting in some cases).
[Right, thanks. In fact Michel corrected this rather soon after the
note was announced. --PDM]
>-------------------------------------------------------------------------
>II.2 - Distinction between formal parameter specifications and ordinary
>specifications:
>-----------------------------------------------------------------------
The need for a distinction between ``fixed'' and ``formal'' is clearly
explained. It is very sensible for a user and it was introduced in many
languages under various forms (ACT ONE/Lotos, for example).
But it would be better to base the difference on semantical reasons,
rather on syntactical ones. An old usage (OBJ, ACT ONE, LPG,...) was
formal <---> loose semantics
fixed <---> initial (free extension) semantics.
So, a formal specification is a ``type'' for fixed specifications (which
can be identified to classes of isomorphic algebras). This is also the view
of SPECTRAL, classes vs structures.
But possibly, the distinction above has no meaning at the level of
building a specification by assembly. This is a distinction for the
architectural level. Nevertheless, I should not like to write :
param TOTAL-ORDER = -- Why ``param'' = parameter here ?
...
endparam.
>-------------------------------------------------------------------------
>II.3 - Compound sorts:
>----------------------
Compound sort (or compound name) is a notation that allows one to
solve usual ambiguities when using instantiated generic specifications.
Moreover, this notation supports the sharing by name identity, very
well in the spirit of the X-CoFI language. The list of ``internal names''
is under the responsability of the user and does not provide any specific
meaning.
This is very different from compound names in LPG (as Michel quotes it),
even if many specifications will be similar in both notations.
===========================================================================
A last comment :
There are several references to ``implicit fitting morphism''.
This notion must be carefully designed to be sufficiently powerful.
The notion of ``by-default views'' of OBJ, for example, is not fully
satisfactory. My preference in that domain is in favour of a more explicit
notion of morphisms between specifications, but this idea is not included
in the common language.
===========================================================================
--
==============================================================================
Didier Bert http://www-lsr.imag.fr/users/Didier.Bert/
IMAG-LSR Tel: +33-76.82.72.16
BP 53 Fax: +33-76.82.72.87
F-38041 Grenoble Cedex 9
==============================================================================