[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Revised study note on architectural specifications [PDM-2]
[To all (especially those about to leave for Edinburgh):
I'm very sorry for the delay in releasing v0.94 - I too have been
suffering from a particularly busy period. Also, it has taken more
time than I'd allowed to condense the various new notes into the
revised design summary. But nearly there: definitely today, hopefully
around noon... --PDM]
Dear Peter,
o a small change leads to more conciseness and allows global composition
[please also consider the section on "A misunderstanding?" from my side]
o dependency/algebra parameters are motivated
o Generic architectural specifications are not considered urgent.
o A revised abstract syntax for architectural specifications is proposed.
with your revised note I much better understand your concerns and
intentions, also an occasional misunderstanding between us (it is a lengthy
process to make oneself understood, isn't it). I think I can now even
propose a simpler solution which is even closer to the intentions of
SPECTRAl etc. than the present one.
The major change (in methodological expressiveness) is minor in syntax:
in architectural specifications one should not only state the SPECs for the
units to be implemented, but also the SPEC for the whole product. This is
(I believe) precisely your intuition and intention in 4.1, i.e. to specify
I-BUNCH directly as
I-BUNCH: NAT >< ELEM -> BUNCH
is read as
I-BUNCH will, given (an implementation of) NAT and ELEM,
yield (an implementation of) BUNCH
[in my concrete syntax (completely ad hoc, of course :-), the fact that
I-BUNCH is an architectural specification is indicated by the very fact
that the result is an algebra of the specification BUNCH, whereas a
parametrized spec P-BUNCH would yield a specification, e.g.
P-BUNCH: NAT >< ELEM -> spec = [ ... ]
also
P-I-BUNCH: NAT >< ELEM -> P-BUNCH (NAT, ELEM) ]
A more wordy syntax as in your (second example in 4.1)
arc spec I-BUNCH =
NAT >< ELEM -> BUNCH
end spec
is of course possible.
Note that the need for a composition in the body is only needed in more
complex cases, e.g. assuming another globally available arch spec (in your
style of syntax here)
arc spec I-B-BUNCH-DEL =
BUNCH -> BUNCH-DEL
end spec
we can now compose
arc spec I-BUNCH-DEL =
decl N: NAT
decl E: ELEM
yields BUNCH-DEL -- result spec
compose I-B-BUNCH-DEL(I-BUNCH(N, E))
end spec
or alternatively
arc spec I-BUNCH-DEL =
N: NAT >< E: ELEM -> BUNCH-DEL
compose I-B-BUNCH-DEL(I-BUNCH(N, E))
end spec
Note that this now becomes possible *with global* arch specs (a local
version where these are all combined as in your 4th example in 4.1 is of
course also possible).
[in my syntax this would read as follows, for the separate global arch specs:
I-BUNCH: NAT >< ELEM -> BUNCH
I-B-BUNCH-DEL: BUNCH -> BUNCH-DEL
I-BUNCH-DEL: ( N: NAT >< E: ELEM ) -> BUNCH-DEL =
I-B-BUNCH-DEL(I-BUNCH(N, E)) ]
If the result spec is included, it also becomes much clearer that you
intend to deliver a SET in your example I-SET; in my syntax:
I-SET: (L: LIST >< S: LIST -> SET-AS-LIST) -> SET =
S(L) {renaming List to Set}{hiding nil, cons}
Most of your examples become much simpler now (as you, I guess, intended in
4.1):
I-PAIR: ELEM1 >< ELEM2 -> PAIR
Indeed, the example in 4.3 with explicit use of algebras becomes
DIFF-DELETE-SET: ( N: NAT >< E: ELEM >< B: BUNCH-DEL(N,E) >< S: SET(N,E) )
-> DELETE-SET(N,E,B,S)
(or an arc spec ... end spec around it)
Dependency/algebra parameters
-----------------------------
I do think that you misunderstand the dependency issue. It is emphatically
*not* an issue of having to see "code" or breaching the encapsulation
principle. The issue is to distinguish between potentially different
implementations to insist on the same implementation, *whatever they are*,
i.e. without knowing them. The issue with BUNCH-DEL(N,E) (and similar
examples) is that one has to have an implementation for every actual
instantiation of N and E, on the actual side, for these N and E *only*. It
is not required (as in the more general and more elegant example of having
a B: NAT >< ELEM -> BUNCH-DEL as a parameter) that a general implementation
exists (which might be difficult to implement). If such a general
I-BUNCH-DEL happens to exist, then the difference (on the actual side) is
between an instantiation I-BUNCH-DEL(Na, Ea) or passing I-BUNCH-DEL
directly.
(cf. also my notes / with Till)
Generic Architectural Specs
---------------------------
This is a true misunderstanding. What I meant is the above; what you
describe is an interesting combination that merits further thought because
of the generality, but is not of immediate necessity, for my taste.
A misunderstanding?
------------------
I do not see how an arch spec can be a spec.
[A reference to a named arch spec from a spec may be interpreted as a
reference to the requirements on the composed implementation. --Peter]
Perhaps this is my
misunderstanding since you then consider the class of functions and I only
the specification of one such function. However, in my case, composition is
obviously possible (see above) and one could always lift mine to a spec
with a corresponding {ASP} construct (see notes by Till).
Abstract Syntax
---------------
(I am sure you find better names}
SPEC ::= ... | lift ARC-SPEC-REF
LIBRARY-ITEM ::= ... | ARC-SPEC-DEFN
ARC-SPEC-DEFN ::= arc-spec-defn ARC-SPEC-NAME PAR* RESULT [BODY]
ARC-SPEC-NAME ::= SIMPLE-ID
PAR ::= spec-par-defn [PAR-NAME] SPEC
PAR-NAME ::= SIMPLE-ID
RESULT ::= SPEC
BODY ::= UNIT-TERM
UNIT-TERM ::= UNIT-NAME | UNIT-APPL | UNIT-REDUCT
UNIT-NAME ::= ARC-SPEC-NAME | PAR-NAME
UNIT-APPL ::= unit-appl UNIT-NAME UNIT-TERM*
UNIT-REDUCT ::= unit-reduct SIG-MORPH UNIT-TERM
___________________________________________________________________
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