Re: Revised study note on architectural specifications [PDM-2]

[Michal.Walicki@ii.uib.no (Michal Walicki)]

Sorry for the late reaction - I just returned from a short trip.

[This arrived just after I promised to make Part III of v0.94
available later today...  I'll need more time now, it seems, and I
don't have any this evening: I'll see what I can do tomorrow
afternoon.  Those that are already leaving for Edinburgh tomorrow will
be able to get copies there.  --PDM]

1.
One thing which should be spelled more clearly concerns the semantics of
arc.specs. Peter's note focuses on the interpretation that, e.g., I-BUNCH
(p.7) specifies
a) a class of functions which take *arbitrary* algebras N, E implementing
NAT and ELEM and return an algebra B(N,E):BUNCH-DEL. 
[Actually BUNCH. --Peter]
It is not
b) a class of functions, each of which takes *some particular* algebras N,
E implementing NAT and ELEM and returns a BUNCH-DEL algebra B(N,E).

I prefer a) because I imagine that arc.specs appear at the stage of
development where one can assume that construction of this kind of
"genric/parameterized" implementations makes sense. It is perhaps a
methodological issue, but the consequences of b) are a bit unclear to me -
do we have to make separate implementations for each possible choice of N
and E, should we make just some/one, or else only for these N's and E's
which are otherwise present? This interpretation would also imply that the
implementation has to be serialized: first N and E, then B(N,E).

[This is also my main concern about specs param'ed by algebras. --Peter]

2.
Concerning sharing (the examples and "assumptions" on p.5).
a)
It looks to me (as usual, apologies for possible misunderstanding) that,
given the restriction 2 about "argument sharing", the specification
BAD-I-DELETE-SET is actually the same as I-DELETE-SET: since BUNCH-DEL and
SET share the subspecifications of NAT and ELEM, the restriction implies
that these will have common implementation.

[But there is no "feedback" of this to the specifications for the
implementations of BUNCH-DEL and SET, as pointed out by Andrzej. --Peter]

I understand that this restriction is meant to release one from writing
explicitly all the shared subparts and enforce them implicitly. (This is
consistent with sharing in req.specs - and I think such a consistency is a
good thing. As there, (possibly unintended) clashes can be signaled by the
tools.)

[I personally think one should be forced to write I-DELETE-SET, and
that BAD-... should be rejected.  --Peter]

b)
The unclear point here is what happens when some parameters SPi and SPj
share not the whole signatures but only their parts. It says "where any
common signature of SPi and SPj...". I guess this means that they have `the
same signature'?

[No, I really meant subsignature!  E.g., they might both be extensions
of NAT.  --Peter]

c)
However, this sharing interacts with the sharing in req.specs and the
restriction 1 "specification extension". If SPi and SPj have, say, only one
symbol F in common (but not the same signature), and this symbol occurs
only once in the (resulting) SP, then SPi and SPj will be implemented
independently but have to have the same implementation of F?

[That is exactly why I would like to reject arc specs like
BAD-I-DELETE-SET.  --PDM]

3.
I think of req.specs occurring in the arc.specs as 'types', in particular,
they should determine the signature of the arc spec.
The example I-SET of hiding (on p.6) does not convinve me. For the first,
it does not seem to conform to the restriction 1 "specification extension"
- what is the result here is a signature of SET (after hiding nil, cons),
and Sig(LIST) is not included in it.

[But the "specification extension" assumption was intended to be
concerned with the individual functions that get composed, not with
the entire arc spec.  --Peter]

For the second, I would prefer to be more precise in indicating the 'type'
of the result, i.e.:
        arc spec I-SET =
                L: LIST
                S: LIST -> SET-AS-LIST{hiding nil, cons}
                compose S(L)
        end spec

[Now the spec of S certainly would break the "specification extension"
assumption!  --Peter]

In any case, the restriction 1 needs a modification.

[...or at least some clarification, it seems - thanks!  --Peter]

(There is a typo on p.9: in "spec BUNCH(par ELEM)= enrich NAT by..." there
should be "enrich ELEM by..." instead.)

[No, I think it's correct as it stands.  --Peter]

        Michal