[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
parametrized specification issues [400 lines]
These comments are w.r.t. some issues on my mind regarding parametrized
specifications and parametrized architectural constructs, and in response
to Michels note and Andrzejs comments.
[Note from the moderator: Please send all reactions as soon as
possible to cofi-language@brics.dk, indicating at the beginning which
of the following issues are addressed:
* parametrized specs: fixed parts of parameters
* parametrized specs: dependent parameters
* parametrized specs: compound ids
* architectural specs and their relation to structured specs
To avoid excessively-long follow-ups, one should try not to cite more
of the original message than is strictly necessary for establishing
the context of the remarks, as the originals of messages are
permanently available via the mailing list archives. --PDM]
[Note that the original of this message contains some side remarks
enclosed in [...]. The remarks inserted by the moderator, also
enclosed in [...], are distinguished by ending thus: --PDM]
(1) fixed parts, "formal specifications" etc.
---------------------------------------------
It is somewhat unclear to me whether the present proposal still contains
fixed parts; but here are my comments nontheless.
The problem Michel wants to solve is deeper than the use of "fixed parts"
in formal parts (of parametrized specifications). What Michel wants
[Presumably Bernd intended an implicit "it seems to me" here, as it is
conceivable that Michel will not agree with Bernd's interpretation of
his proposal... Please let us follow normal netiquette on this mailing
list, taking care to distinguish between facts and opinions, and to
avoid unnecessarily-provocative :-) formulations. --PDM]
is to
"use" some specifications (e.g. NATURALS) somewhat silently, much in the
sense of an "import" in other languages. If N is used in X, and X is later
combined with some other spec Y ("applied occurrence" of X), then N should
already be available ("visible") in the context of Y. An alternative view
is, that N is a (persistent?) formal parameter of X which is always
instantiated with (the same) N in any "applied occurrence" of X; in fact, N
is a kind of implicit parameter. This is in fact one semantics of "import";
another would be that the "implicit parameter" is always carried along,
even if it is NOT visible at the "applied occurrence" of X; some call this
"transitive visibility".
In any case, my conjecture is that we might want this as another concept
for structuring specifications, not restricted to those that can be used in
formal parts (for more on this see below), in other words as another
extension or parametrization operator. Let me try an abstract example first
and then Michels concrete one: "=>" shall denote the function arrow for
implicit parameter.
Then let
X: N => spec = [...]
Y: N => spec = [...]
be given. Then
X ++ Y
where "++" denotes the (new) extension of some structuring operator "+"
(like union), corresponds to a Z such that
Z: N => spec = X(N) + Y(N)
and for
S: spec = N + [...]
now X ++ S
corresponds to R such that
R: N => spec = X(N) + S
Then (Michels concrete example in slightly different syntax):
NAMED_ELEM: NAME => spec =
[Elem: sort
Name_of: Elem _> Name
... ]
STACK2: NAMED_ELEM -> spec =
STACK (NAMED_ELEM)
+ [ ... ]
actually means (implicitly)
STACK2: NAME => NAMED_ELEM(NAME) -> spec =
STACK (NAMED_ELEM(NAME))
+ [ ... ]
What is the point I am trying to make?
First of all, there is a semantics for this (I hope; others will explain it
better; at least Till agrees); obviously we do not want to explain it this
way to the user! Once we have higher order parametrization, it is even
easier to explain.
Secondly, it makes perfect sense to treat such specs as other specs, not
only in the context of "formal parts". This I find most important from a
pragmatic point of view. I would indeed very much like NOT to have Michels
proposed distinction between normal and formal specs. For example, I would
want to specify partial order (as an ordinary spec), combine it with others
etc. without having to declare it as a "formal" spec since I might want to
use it (among others) in that context later.
Thus the only change in the language would be the introduction of another
specification building operator (call it e.g. BASED-SPEC or so), without
having to restrict its use to formal parts, e.g.
BASED-SPEC ::= based-spec SPEC+ BY-SPEC
(assuming this could also be used in a PARAM) such that
spec-defn S based-spec SPB SP
would have my concrete syntax
S: SPB => spec = SP
in the above example [or some other concrete syntax, of course].
(2) Several formal parameters
-----------------------------
In contrast to Michel, I can see very good uses for dependent parameters.
In other words, for
F: X -> Y -> Z -> spec = ...
or a more first order way of writing
F: (X, Y, Z) -> spec = ...
and an instantiation
F (A, B, C)
I would expect the instantiations to be perfomed sequentially; thus it
yould be possible to write
F: (X, LIST(X), QUEUE(X)) -> spec = ...
and an instantiation
F (INT, LISTINT, QUEUEINT)
(3) compound ids
----------------
As I wrote earlier "compound identifiers are too close to parametrized types and
polymorphic functions to be introduced as such". You may consider my major
worry (apart from certain problems in Larch)
[Bernd, please clarify just what these problems in Larch are. Jim
Horning in his Oslo paper [LNCS 1130, p.64] refers to some problems
that structured sort names did not solve, and suggests [ibid, p.68]
that structured operator names might help; is that what you have in
mind? --PDM]
to be a result from (already)
studying the possible problems of extensions. Let me elaborate on this.
My first problem is even before extensions: the interaction with subsorts.
In a context where we instantiate STACK (of Michels example) twice by specs
that introduce subsort-relations, we might have:
STACK (NAT) + STACK (INT)
and can thus talk about
stack[int] and stack[nat]
where one might expect some sort of induced subsort relation; but it is not
there! This is another indication that what one really wants are
parametrized types where such an induced subsort relation could be defined
in general.
Another problem of the interaction with subsorts (noted by Till) is the
need for additional restrictions that make the design more complicated. For
example, one should not be allowed to define (even as an accidental
omission) a non-compound sortid as a subsort of a compound sort (possibly
also vice-versa), as e.g. in
Stack[Elem]: sort
NeStack: sort < Stack[Elem]
whereas
EmptyStack: sort < Stack[Elem], or
EmptyStack[Elem]: sort < Stack[Elem]
both make sense; complicated! Also, for compound subsortids, there must
obviously be some compatibility rules as to the "parameters"; as an
example: can I say (in an instantiation context)
Stack[Nat]: sort < Stack[Int]
or, worse (in the definition)
Stack[Nat]: sort < Stack[Elem]
In fact, one either has no rules leading to rubbish in some cases, or one
has to introduce rules that effectively define the semantics for proper
parametrized types.
Let me also note that the example of sort(leq), sort(geq) is a typical
example of a higher-order function and should be treated as such.
Moreover, parametrized specs are fine but do not solve all problems, as
opposed to parametrized types and true polymorphic functions. Consider the
typical case of a specification of map (sorry, this is HO, but the first
that comes to my mind; a and b are type variables)
map: (a->b) -> List a -> List b
[or map: (a, b: sort) => (a->b) -> List a -> List b
where the type variables are stated as implicit type parameters]
where one would want to have axioms like
map f (map g x) = map (f o g) x
(where o denotes functional composition).
Such a declaration involves two and the axiom involves three different
instantiations of List. This is impossible to do in the same parametrized
spec; it can be done in a separate spec, but is very cumbersome to
instantiate explicitly each time!
To conclude this point: let us delete compound names in X; Michel already
states that explicit renaming solves the problem
[Please cite other work accurately. In fact Michel wrote in his note:
... In a nutshell, the
specification STACK-OF-INT is equivalent (same signature, same model class)
to the specification (rename STACK-OF-ELEM by H) + INTEGER.
This may be used as an argument to claim that parametrized specifications
are not very useful (in the sense that the same effect could be obtained
with other specification-building primitives). This is true if one is
mainly concerned with semantical issues, but from a methodological point of
view it is however essential for the specifier to be able to identify and
clearly distinguish, in a specification, the subspecifications that are
enriched/extended/reused/refined, from the parts that are intended to
play the role of formal parameter specifications.
--PDM]
(otherwise let us look for
a different solution there); and many peopple will not have those problems
any more when moving to parametrized types and polymorphic functions ( this
does NOT necessarily entail HO!).
(4) Architectural Specs and their interrelation with Structured Specs
---------------------------------------------------------------------
(a) Names for formal parameters are needed
------------------------------------------
Let us consider my standard example of a parametrized architectural spec,
first written without formal parameter names (for the algebras) in the
style advocated in Peters note [PDM-2] (although not with his syntax):
SetAsList: (ELEM, LIST(ELEM) ) -> SET(ELEM)
where ELEM, LIST and SET are (parametrized) *structured* specs. [Peter:
note: normal SET, not SET-AS-LIST].
The semantics of F should be a function from algebras to algebras (see
notes on semantics below). Peter claims that names for formal parameters
are not needed. Before I provide a counter example,
[Bernd, again, please take more care when citing. "Peter" wrote:
There is just one assumption: that implementations resulting from
applying functional modules always extend their parameters - any
hiding or renaming to be done is left to when implementations are
composed. If you think that this is an unreasonable assumption, or
has unfortunate methodological or semantic implications, please react
(with examples of the problems); without it, I wouldn't know how to
proceed.
It seems that the "counter-example" below violates that assumption...
--PDM]
let me rewrite my
example *with* formal parameter names for the algebras in my favored style:
SetAsList: (X: ELEM, LX: LIST(X) ) -> SET(X)
[Peter: note: normal SET, not SET-AS-LIST] Now the question is, what LIST X
means since X is an *algebra* and not a spec? Here X is in fact *coerced*
to a spec corresponding to the model class {X} consisting just of X; this
coercion that I asked for (and Andrzej confirmed) has been worked out with
Till in the notes on semantics below.
Now why formal parameter names (for the algebras)? The first example is
F: (X, Y: ELEM, LX: LIST(X), LY: LIST(Y) ) -> SP(X, Y, LX, LY)
Note that we need to refer to the two different "implementations" of ELEM
explicitly since we must distinguish between LIST(X) and LIST(Y) being two
different and specific instantiations of LIST (just assume Int and ListBool
as actual parameters for X and Y), and between LX, LY as (possibly)
completely unrelated implementations.
[As a note in passing, this is different from the higher-order example (for
an extension) where one insists on the same generic implementation of a
list:
SetAsListHO: (X: ELEM, L: (ELEM->LIST(ELEM)) ) -> SET(X)
F2: (X, Y: ELEM, L: (ELEM->LIST(ELEM) ) -> SP(X, Y, L(X), L(Y) )
end side note]
(b) We must have generic specs, and names for them
--------------------------------------------------
Let me also emphasize that we do need *generic*, i.e. *parametrized*
architectural specs. To assume that only one instantiation is needed (as
seems to be the case in Peters note and mail) means Modula and not Ada (or
more).
Moreover, as a response to Peters question whether we need to name
UNIT-FUN-SPECs, consider a globally (i.e. at the library level) available
(generic) implementation of LIST
List: ELEM->LIST(ELEM)
It must be named since we may want to use it in several different
instantiations, e.g. as a first order example of the above HO one:
F3: (X, Y: ELEM) -> SP(X, Y, List(X), List(Y) )
(c) Only 2 kinds of specs (plus coercions) are needed
-----------------------------------------------------
[semantic note by Till and Bernd]
Andrzejs proposal distinguishes 3 kinds of (parametrized) specs:
1. Specifications parameterized by specs
2. specifications parameterized by algebras.
3. Architectural specs, i.e. specifications of (algebras parameterized by
algebras).
but in X, we only have 1. and 3.
The following is much in the spirit of Andrzej's suggestion (see also [SST
92]), but tries
to simplify things by considering 2. as a notion which may be derived from 1.
For simplicity, let us assume that 1. and 2. are written in the form
PSPEC : SP1 ... SPn SPEC
(ignoring the fact that 1. also allows a BY-SPEC instead of SPEC, which
should be replaced by the union of BY-SPEC with the SPi to
be able to apply the following).
The semantics of
PSPEC : SP1 ... SPn SPEC
due to 1. is a function
P:Pow(Alg(SP1)) >< ... >< Pow(Alg(Spn)) -> Pow(Alg(SPEC))
mapping (denotations of) specifications to (denotations of) specifications
given by
P(C1,...,Cn) = {A in Alg(Spec) | A|'SPi in Ci for i=1..n}
for Ci \subset Alg(SPi)
In case of persistency, this also interacts smoothly with
the pushout textual substitution semantics (as Andrzej mentioned).
(Pow means powerset.)
Now in the example
SetAsList: (X: ELEM, LX: LIST(X) ) -> SET(X)
we also need
2. specifications parameterized by algebras.
Thus the semantics of
PSPEC : SP1 ... SPn SPEC
due to 2. is the function
G : Alg(SP1) >< ... >< Alg(Spn) -> Pow(Alg(SPEC))
mapping algebras to (denotations of) specifications given by
G(A_1,...,A_n) = {A in Alg(SPEC) | A|'SPi = Ai for i=1..n}
But we do not need to introduce 2. as an own concept, since there
is a coercion from 1. to 2.:
Given any P as under 2., let
P*(A_1,...,A_n) = P({A_1},...,{A_n})
Then with this coercion, we can get the semantics of
PSPEC : SP1 ... SPn SPEC
defined under 2.
by just taking its semantics given under 1. and coercing it to 2.
Thus, we can use a parameterized spec
LIST[ELEM]
defined in sense 1.
and use it in a 2.-context:
SetAsList: (X: ELEM, LX: LIST(X) ) -> SET(X)
Then the semantics of
UNITFUNDECL : X1:SP1 ... Xn:SPn SPEC
due to 3. is the set
Q = {F: (A1:SP1) >< (A2:SP1(A1)) ... >< (An:SPn(A1,...,/An-1))
-> (A:SPEC(A1,...,An))
| A|'SPi = Ai for i=1..n }
of parameterized algebras F (mapping algebras to algebras),
where
(Ai:SPi(A1,...,Ai-1))
means that SPi is a parameterized spec (due to 1., but coerced to 2.)
which is applied to A1,..Ai-1, and Ai is a member of the resulting
class of algebras.
The semantics of
UNITFUNDEFN : X1:SP1 ... Xn:SPn = COMP
due to 3. is the parameterized algebra mapping A1,...,An as above
to the semantics of COMP under the substitution [X1/A1,...Xn/An].
Note that in a COMP, the Xi can be used just as UNIT-NAMEs.
(d) do we need to refer to arch specs in struct specs?
------------------------------------------------------
It is not strictly necessary to be able to refer to arch specs in struct
specs. However, if the "coercion operator", call it {_}, is provided
explicitly, one could insist that *one* model (algebra, implementation) is
used consistently throughout. With
AS: S ...
ONLY_AS: spec = {AS}
we don't know *which* model, but only this one will be used. AS might be a
specific implementation of integers (or the like) or a result of a complex
composition of architectural specs.
___________________________________________________________________
Prof. Dr. Bernd Krieg-Brueckner courier mail only:
FB3 Mathematik und Informatik MZH 8071, FB3
Universitaet Bremen Universitaet Bremen
Postfach 330 440 Bibliothekstr. 1
D-28334 Bremen D-28359 Bremen
Telefon: (+49) 421-218-3660 telefax: (+49) 421-218-3054
bkb@Informatik.Uni-Bremen.DE privat: (+49) 421-25-1024
NEW: http://www.informatik.uni-bremen.de/~bkb