Re: On architectural specifications

[Andrzej Tarlecki <tarlecki@mimuw.edu.pl>]

Dear Colleagues,

Repeating my excuses as in the previous message in reaction to
Michel's note: my apology for reacting so late to the note by Peter on
architectural specifications!  [The note [PDM-2] was only released on
18 October, and (for once :-) there was no stipulated deadline for
reactions.  Further comments are still welcome - although I'll be
asking Bernd to try and reach a conclusion on these issues by the end
of next week, i.e., 1 November, so the earlier the better...  BTW,
"Peter" has taken the liberty of inserting a few non-moderator reactions
below, to speed things up.  --PDM]

First, many thanks to Peter for putting his work and time into a
careful presentation of a nice example of architectural
specifications, and for motivating them so nicely. No criticism, and
only a lot of appreciation from me on what Peter spelled out in the
first part of the note (sect. 1 and 2).

Now, about the rest of the note (sect. 3 and 4):

The essence of the problem discussed is the way dependencies between
various parameters for the specified units are described.

As far as I understand these things, there are basically two ways to
handle such dependencies.  One goes back to Pebble, and is used in
SPECTRAL, where dependencies are build up using parametricity in a
heavy way, including true higher-order parametericity whenever
convenient (although this is often not necessary, and a lot can be
done without higher-order parameterisation). The other is the use of
SML sharing constraints in signatures (as also inherited from SML by
Extended ML). What Peter writes about is essentially the latter,
except that instead of explicit sharing constraints in signatures and
specifications, where algebra and structure names and then the dot
notation are used to indicate unambigously which realisations of
signatures (or specs) share, Peter relies on the ASL (same name, same
thing) convention to indicate sharing.

A problem with the example Peter uses is that it is incorrect...
[right - but see the correction cited below. --Peter]

Indeed, under the current semantics and the "ASL sharing rule", the
specification of a parameterised component
	BUNCH-DEL >< SET -> DELETE-SET
might (should?) be read as requiring that there is a sharing
constraint between the sorts (and operations) named in the same way in
BUNCH-DEL and in SET (under the semantics implicit so far, I guess,
these would be an inconsistent specification, as no function realising
it could be provided without these extra assumption about the
arguments). This is fine --- and I think we can agree on such an
interpretation. This imposes however an extra requirement on
the actual parameters for the component declared as
	decl D: BUNCH-DEL >< SET -> DELETE-SET
which in my view renders the composition
	compose D(B,S)
incorrect: since the declarations B: BUNCH-DEL and S: SET in no way
constrain the components B and S to be mutually related, and so they
in particular may realise the commonly names things in BUNCH-DEL and
SET in quite different ways.

To summarize: the notation for architectural specifications in CoFI
v0.93 is perfectly adequate for expressing extensions where common
parts of parameters have to agree. However, as far as I can see the
notation with the semantics as I understand it does not provide
sufficient means to correctly express some typical compositions built
by instantiation of so specifed extensions.  [It's not clear here just
which concrete example cannot be correctly expressed. --PDM]

The latter problem is attacked by Peter in sect.4 where he proposes
that the ASL sharing rule is extended to the context of an entire
architectural specification, so that apparently independently
specified components are required to share the same realisation of the
things (sorts, operations) names by the same names in their respective
specifications. I believe this might work, but at a price which I view
as severe. At least:

-- no multiple realisations of the same specification are allowed in
this way. If you want to deal with two, say, partial orders, then you
have to rename their specifications explicitly.  [But one may have to
do such a renaming even to express the requirements specification.
What I'd like to see is a realistic example of an architectural
specification that *necessarily* involves two independent
implementations of exactly the same requirements, i.e., where
essentially the same architectural design *cannot* be expressed by a
simple renaming or reorganization of the specification.  Unless such
examples exist, the price of this assumption is perhaps not so high!
--Peter]

-- there is no clear flow of dependencies, in the sense that some
rather accidental dependencies might occur, coming "in the middle of a
component specification".

-- realisation of the components of an architectural specification
cannot proceed independently from each other.

-- the real requirement on the components are not given explicitly in
its specification, but must be inferred from the environment.

-- it is not clear what happens when specifications are "nested", and
even less clear how such a rule (same name, same thing) would apply
to specifications of parameterised components.

Overall, i think that the proposal to deal with the issue of sharing
between realisations of various specifications by making the
dependency on specific algebras explicit is more elegant, makes some
of the above problems disappear and where they stay (like dependency
between realisations of components) at least they are made explicit
and a flow of dependencies may be easily determined.  For a possible
proposal in this direction see for instance my message sent on 15 Oct
(basically with comments on v0.93, but also with some suggestion of
building both parameterised specifications and specifications of
parameterised components around specifications parameterised by
algebras) or perhaps some messages from Bernd.

However, in a private correspondence earlier Peter suggests another
obvious way to cope with the incorrectness of the architectural
specification mentioned above. Namely, this can be achieved by the use
of parameterised components, making the specification more modular,
with an explicit flow of dependencies:

arc spec BETTER-DELETE-SET = 
  decl E:ELEM
  decl B:ELEM->BUNCH-DEL
  decl S:ELEM->SET
  decl D:BUNCH-DEL >< SET -> DELETE-SET
  compose D(B(E),S(E))
end spec

(this disregards dependencies on NAT, which can --- or cannot :-) ---
be dealt with similarly as dependencies on ELEM, so I will stick to
this oversimplified version) [OK, although I had previously sent you
also the corrected version with dependency on N:NAT.  Let it be an
exercise for the reader to patch the above arc spec accordingly... :-)
--Peter]

This is fine, and in fact this is exactly the way I would proceed
here.

However, it should be pointed out that this is a different design,
leading to a different class of possible realisations than what I
think was the intention behind Peter's original architectural spec,
[Sorry, but what I intended was in fact the BETTER-DELETE-SET
version... --Peter] which within the proposal I suggested earlier could
be written more or less as follows: [I've added the prefix `DIFF-' to
the name of your spec below, to avoid too much overloading. --PDM]

arc spec DIFF-DELETE-SET = 
  decl E: ELEM
  decl B: BUNCH-DEL(E)
  decl S: SET(E)
  decl D: E: ELEM >< B: BUNCH-DEL(E) >< S: SET(E) -> DELETE-SET(E,B,S)
  compose D(E,B,S)
end spec

(where BUNCH-DEL and SET would have to be turned into specifications
parameterised by algebras in an obvious way, and DELETE-SET could be
modified in the same way or provided here explicitly from scratch).

Rather informally, the difference is that DIFF-DELETE-SET asks for one
implementation E of ELEM, and then for one non-parameterised component
S implementing SET(E) for this very E provided above, and the same for
B implementing BUNCH-DEL(E). However, this means that the construction
of B and of S may proceed only after E is given (since only once it is
given the initial specifications of B and S become clear).  On the
other hand, BETTER-DELETE-SET asks for one implementation E of ELEM
again, but then for an implementation S of ELEM->SET, parameterised by
possible implementations of ELEM, so that it would work for all
possible implementations of ELEM, not only for this specific E.
Similarly for a parameterised implementation B of ELEM->BUNCH-DEL.
Clearly, the advantage of BETTER-DELETE-SET over DIFF-DELETE-SET is
that implementation of each of the components may proceed at once,
independently from the implementation of the others. However, the
implementors have more work to do, since they have to produce B's and
S's that work not for just one E, but for all the possible E's.
Another consequence would be that some "optimizations" possible for
the specific E chosen in an implementation of DIFF-DELETE-SET may not
be possible for other E's, and so such "optimizing implementations"
might be used uder the design spelled out by DIFF-DELETE-SET but must
not be used under the design spelled out by BETTER-DELETE-SET.

[Thanks for this example and explanation, which illustrate the usage
of your proposal nicely, pinpointing the methodological consequences
of letting requirements specs be parametrized by algebras, as in
BUNCH-DEL(E) and SET(E).  Sorry that I hadn't previously understood
that you want to use architectural specs to (partially) serialize
implementation tasks. I'll update [PDM-2] to address this point
(sometime...).  --Peter]

Overall:

I still think that some way of introducing specifications
parameterised by algebras could be useful. On the other hand, the
examples I have in mind may be rewritten perhaps even a bit more
elegantly, but with some loss of "efficiency", using what we already
have in the architectural specifications (which is the reason for all
the caveats in my message containing some proposal for specifications
parameterised by algebras).

[As I see it, the issues have become a lot clearer (thanks to Andrzej!)
and the remaining questions concerning the v0.93 form of architectural
specifications and Andrzej's proposal are:

* Can the (partial) serialization of implementations be expressed at all
  using the v0.93 constructs --- perhaps using several arc specs?
  (Andrzej's DIFF-DELETE-SET is a good example to try!)  If so, the only
  thing left to decide (IMHO) is whether it looks sufficiently natural.

* Should it be a requirement for the CoFI language that it can express
  (partial) serialization of implementation tasks, or only their
  independence?  My reading of Andrzej's caveats is that although he
  regards the former as useful, he doesn't propose that it should be a
  requirement to cater for them (at least in the basic CoFI language).

- plus the question posed earlier above, concerning the need or not for
multiple implementations of the same requirements spec, which only
seems to affect whether names for implementations are really needed at
all.  --PDM]

Best regards,

Andrzej