[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Named parameters in generic specifications
[N.B. If anyone supports the changes proposed below (apart from Gianna
and Maura, of course :-) they should indicate this STRAIGHT AWAY! -
otherwise I do not see how they can be incorporated in v0.95... -PDM]
Named parameters in generic specifications
****
We want to raise again the point of the ``style'' of generic specifications
in CASL at this moment of the schedule, even if we know very well that
things seem already setted and that this can be the beginning of a messy
discussion (this is also the reason for initially keeping the debate
limited to a small group), because of the following fact.
In our departement there is a group working in geometric modelling
which has shown some interest to use algebraic specifications for some
data structures and related algoritms (previous attempts by other
groups are present in the litterature).
Clearly, we are planning to use CASL as specification language, and so
we are organizing the material to explain to them how to use such language
and we having problems with the section on this ``strange'' (at least for them)
form of parametrization.
Thus we have thought that can be valuable to investigate if we can find
another ``sound and coherent'' proposal, more intuitive and similar to
the usual stuff.
Notice that looking at the existing works on the use of algebraic
specifications in the field of geometric modelling I (Gianna) have found
several imprecisions/small errors in the written specifications,
meaning that a lot of effort has to be put in the presentation of
the language to ``normal users''.
****
The main problem, in our opinion is the lack of name for the
parameters (as first noted by Berndt).
We agree that named parameters are not needed in the current proposal
and that such proposal is sound and coherent, but we also find it not
as convenient to use, and especially to explain to non-experts, as
more standard approaches would be.
Indeed, even if names would not be needed at all, we believe that it
would be convenient to have them, in order to have a syntax closer to
the standard ones in programming languages (as well as in mathematical
theories).
This, in our experience, proves to be a great improvement for
acceptance of formal methods by practitioners.
Moreover, we are not fully convinced that names are not needed.
Indeed, the name of the formal parameter can be omitted only if
such parameter is used in a silent and fixed way in the body of the
specification, that is, as in the current proposal, it is implicitly
extended.
This restriction does not include all the cases in which the body is
expressed in terms of instantiations of other generic specifications on
(expressions using) the formal parameter.
Indeed, consider for instance a generic specification like
SET[X:ELEM]= enrich LIST[X] by {usual stuff}
To write such a SET in the current proposal you have to write either:
SET[ELEM] = enrich LIST[ELEM] by @@@@
where the second ELEM has no connection with the actual parameter, but
it is just the name of a specification present in the global environment
(this was the reason for speaking about ``formal instantiation'' in
Michel's notes)
or
SET[LIST[ELEM]] = @@@@
This is methodologically unacceptable, since it corresponds to require
that to use SET one has to know that SET is based on LIST.
Indeed, to write ''SET applied to NAT'' one has to write SET[LIST[NAT]] and
cannot at all write SET[NAT].
An extreme case is when ELEM is not a specification name but a
specification expression as ``sort elem op A: elem -> elem''
F[sort elem op A: elem -> elem] =
enrich G[sort elem] by @@@@
in this case it is very hard to understand that the actual parameter has to
replace the argument of G, and actually the desired semantics is obtained
not by an instantiation but as a consequence of the semantics of overloaded
names in unions (if we correctly understood the summary).
Another methodological point is that in most examples the parameters have
sorts (and functions an predicates) that are just place holders, in the
sense that they are expected to be replaced by many different actual
structures, like the sort elem in the parameters for list, set...
Thus, such signature elements do not have a "reasonable name" and any
naming discipline would suggest to have a uniform notation for them; this
situation is the same as for indexes of loops in programming languages,
that should have meaningless names, exactly to suggest their nature.
For instance, all such sorts could be called srt(_n with progressive
n's, if there are many in the same parameter) to help the user to remember
that they may be any sort.
But, if there are several parameters this criterion leads to the sharing
of the symbols that happen to have the same name (due to the uniformity
of naming) in different parameters, while intuitively they are not at all
related.
Notice the difference between this situation and the corresponding concept
for architectural specifications. Indeed, in the case of architectural
specs, the units (parameters) are expected to represent subsystems and hence
names in their signatures are not place holders, but "concrete" objects, that
must satisfy the ``same name = same thing'' principle.
On the contrary, in generic specifications the same principle is misleading,
and force the users to remember the otherwise uninteresting names used to
represent generic objects, in order to avoid clashes.
A last remark is that, though having two parameters of the same kind maybe
not so usual (but for instance it happens for pairs, relations, maps.
records...), in such cases the parameter type has to be duplicated in order
to be used.
********** Our Proposal *******************************************
We propose a lambda-calculus style definition of generic
specifications,
enhanced by a more sophisticated parameter-passing mechanism, that is
fitting morphisms are allowed.
Therefore, the first step is the definition of a type system for
parameters. 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, a list 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 WEIGHTED-ELEM the NAT part, used to
describe the target of the weight function, is supposed to be part
of the actual parameter.
- the minimal properties satisfied by the required 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), like in the WEIGHTED-ELEM for the NAT part.
This is basically the rationale behind the typing system we propose in
the sequel.
------- Abstract syntax ---------------
Here, we refer to the summary version 0.95 and prefix a "|" to
changes.
| GEN-SPEC ::= gen-spec PAR* SPEC
| PAR ::= par SPEC-NAME+ PAR-TYPE
| PAR-TYPE ::= par-type SPEC FIXED-SIG?
| FIXED-SIG ::= fixed SPEC+
SPEC ::= ...| SPEC-INST
SPEC-INST::= spec-inst SPEC-NAME FITTING-ARG*
FITTING-ARG ::= fitting-arg SPEC SIG-MORPH?
------- Static Semantics ---------------
The condition for static semantics are more or less the standard ones.
For the definition we have the following two requirements.
1 PAR-TYPE
The SPEC part of a PAR-TYPE may be any well-defined expression
of type SPEC.
The signature of the fixed part is required to be a subsignature of
the SPEC part of the PAR-TYPE.
Symbols in the "generic" part of the signature of a parameter (that is
signature elements of the SPEC part of a PAR-TYPE that do not appear in
the optional FIXED-SIG part) cannot belong to the fixed
part of other parameters.
Notice that the signatures of different parameters are not required
to be disjoint; indeed the intersection of the generic parts of the
signatures of different parameters may be non-empty, as well as the
intersection of their fixed parts.
In particular, several parameters with the same PAR-TYPE
are allowed.
Each parameter name can occur at the most once in the list of formal
parameters of a generic spec, as usual.
2 BODY
The body of a generic spec has to be well formed in the current
environment enriched by the parameter names, that are assumed to
have the signatures described by the corresponding qualifying specs.
Symbols in the "generic" part of the signature of a parameter cannot be
redeclared in the body.
Notice that if the parameters have to be (persistently) enriched,
then this has to be explicitly stated in the body.
Moreover, the body must be unambiguous. Following the principle that
"generic" symbols are just place holders, such symbols
cannot be confused with "generic" symbols declared (with the same profile,
if it is a function or a predicate) in the qualifying specification
of some other parameter.
Thus, if a symbol name is declared (with the same profile,
if it is a function or a predicate) in the varying part of the qualifying
specifications of two (or more) parameters, then it
must be referred to using its source as well as its name.
This requires the following changes to the abstract syntax as well
| SORT ::= ... | referenced-sort SORT-NAME SPEC-NAME
| FUN-NAME ::= ... | referenced-fun FUN-NAME SPEC-NAME
| PRED-NAME ::= ... | referenced-pred PRED-NAME SPEC-NAME
where the *referenced* constructs can be built only with the SPEC-NAME part
corresponding to the name of (one of) the formal parameters, whose signature
includes in its varying part that symbol name.
An instantiation is statically correct if acceptable fitting
parameters are provided for all formal parameters, where an acceptable
fitting parameter consists of a specification SP (the actual parameter)
and, possibly, of a signature morphism from the signature of the formal
parameter (as given by the corresponding PAR-TYPE) to the signature of
SP, that is the identity on the fixed part(s), if any.
(What we really need is a mapping from the disjoint union of all formal names
to names, which is coherent, i.e. that can be extended to a morphism).
------- Semantics ---------------
The semantics of a correct SPEC-DEFN is a partial function, expecting
classes of models as arguments and resulting a class of models, if the
application is correct, or better expecting
classes of models and sort/function/predicate names as arguments.
The latter are those needed to instantiate the formal names
appearing in the varying parts of the specifications qualifying the
parameters and are explicitly provided by the fitting morphisms.
The result of an application to acceptable fitting parameters is
defined iff
the translation along the fitting morphisms of the actual parameter
model classes are included into the corresponding formal parameter model
classes.
Notice that this, in particular, requires that the semantics of the
fixed part of an actual parameter, if any, is a subspecification of the
fixed part of the corresponding formal parameter.
If such result is defined, then it is the evaluation of the body,
where each "generic" meta-symbol has been replaced by a symbol
(determined by the fitting morphisms, where no ambiguities arise due to the
use of referenced names and the restriction on the redeclaration of "generic"
as "fixed" symbols) and then evaluated in the
current environment updated by the associations of the actual with the
formal parameters.
If a less syntax-based definition is preferred, the semantics of a generic
specification is given, as usual, by evaluating its body in the current
environment updated by the association of actual to formal parameters,
where also the "generic" symbols are regarded as parameters, provided by
the fitting morphisms.
This requires a notion of environment associating spec-names with classes of
models as well as "generic" signature symbols with actual names.
Thus, the result is the result of the evaluation of the body in the current
environment updated by
- the associations of all formal names introduced
by the qualifying spec of the parameters (referenced in cases of
possible ambiguities) with the names determined by the fitting morphisms
- the associations of the actual with the formal parameters.
********************************
Some examples
********************************
(using, as usual, a provisional reasonable concrete syntax)
spec BIN_OP = sort elem' op _ &' _: elem' elem' -> elem'
generic spec MAKE_COM [ X: BIN_OP] =
enrich X by axiom a &' b = b &' a
then an instantiation
COM-MINUS = MAKE_COM[NAT {elem' |-> nat, &' |-> Minus }]
will return a specification equivalent to
enrich NAT by
axiom a Minus b = b Minus a
generic spec DOUBLE [ X: BIN_OP] =
enrich persistently X by
op Double: elem' -> elem'
axiom Double(a) = a &' a
(if the parametrized specification (conservatively) extends the
actual parameter, then this condition has to be explicitly written in
its body)
then an instantiation
Q-NAT = DOUBLE[NAT {elem' |-> nat, &' |-> * }]
will return a specification equivalent to
enrich persistently NAT by
op Double: nat -> nat
axiom Double(a) = a * a
On the other hand, since we don't assume that the parameters are
exclusively extended, we can also write parametrized specifications
modifying the syntax of their parameters, as the following ones:
spec HAS_NAT = sort nat fixed sort nat;
generic spec HIDE_NAT [ X: HAS_NAT ] = hide sort nat from X;
generic spec CHANGE_NAT [ X: HAS_NAT ] =
rename sort nat to natural_numbers in X;
Notice that these last two specifications cannot be expressed (as far
as we can see) within the current version of the language.
A last example to see the "sharing" at work.
Recall the pair specification.
spec ELEM = sort elem';
generic spec PAIR[X, Y: ELEM] =
enrich X, Y by
sort pair
op < _, _> : elem'-from-X elem'-from-Y -> pair
Then the instantiation
PAIR[NAT {elem' |-> nat}; BOOL {elem' |-> bool}]
where
spec NAT = sort nat .....standard stuff...
spec BOOL = sort bool .....standard stuff...
has the same semantics as
enrich sort nat .....standard stuff...and
sort bool .....standard stuff...
by
sort pair
op < _, _> : nat bool -> pair
Therefore the instantiations of the two copies of elem have
absolutely unrelated semantics.
Analogously
PAIR[NAT {elem' |-> nat}; NAT {elem' |-> nat}]
has the same semantics as
enrich sort nat .....standard stuff... and
sort nat .....standard stuff...
by
sort pair
op < _, _> : nat nat -> pair
and hence the instantiations of two copies of elem have the same
semantics.
********************************
ADVANTAGES OF OUR PROPOSAL
(from our viewpoint, of course)
********************************
1) The construct for generic specifications is similar to what
people is used to for ``generic stuff'', and so it is simpler to be
explained, and perhaps easier to be used.
2) The presentation of parametrized specifications, at whatever level
(methodological, intuitive/informal, static correctness, semantics) is
(imho) shorter and simpler.
The part on the static correctness of parametrized specifications
could just be presented as the usual rules about the scope of an
identifier.
In the declaration
generic spec GS [ X: ..] = BODY
the scope of X is BODY
and so, if X does not belong to the current environment
generic spec WRONG-SPEC [ Y: ..] = enrich X by ...
is wrong, in the same way that in the sublanguage without parametrized
specification the following declaration is wrong
spec C = enrich X by ...
if X does not belong to the current environment.
3) Presenting parametrized specifications in the proposed way, the
need of having in the language a construct for par-type
(qualifying-specifications) different by the normal specifications is
intuitive.
Regarding this point, notice that in some cases the kind of
specifications used to qualify the parameters may be very different
from the normal specifications. For example in OBJ, the specifications
are conditional equational, while the par-specs (called there
theories) are first-order.
********************************
DISADVANTAGE OF OUR PROPOSAL
(from our viewpoint, of course)
********************************
1 If you want to write a parametrized specification which just extends
the actual parameter you have to write it explicitly.
Though in most case, it requires just one extra line for each
generic specification, if this need is regarded as too vexatory, we can
modify this approch, accordingly with the current proposal, as follows
| PAR ::= PAR-NAME+ QUAL-SPEC
| PAR-NAME ::= PASS-MODE SPEC-NAME
| PASS-MODE ::= par | ext | persistent-ext
and the "actual" body is build prefixing to the body a (persistent)
extension of each parameter with PASS-MODE ext (persistent-ext).
Then, if after analazying concrete case-studies ext is found to be
the most common use, in the concrete syntax the "no-keyword" case can be
reserved for it.
2 The syntax for sorts, function and predicate names has to be
extended to allow referenced uses.
This problem disappears if, as in the current proposal, each symbol
belonging to the signatures of the qualifying specification(s) of
two or more parameters is expected to be interpreted by the same
"semantic object" during the instantiation, corresponding, technically,
to the compatibility conditions for the fitting morphisms.
Under this restriction IF all the parameters have PASS-MODE ext or
persistent-ext AND the parameters do not appear in the SPEC part of
the generic-spec definition (that is the unique use of the parameters is
the implicit extension), then the names of the specifications are
superfluous.
Gianna and Maura