Re: COMMENTS on Tentative Design Summary v0.92

[Don Sannella <dts@dcs.ed.ac.uk>]

Peter,

Here's some responses to specific points in your message.

Cheers, Don

----------------------------------------------------------------

> ***  Linked sections of libraries: 
> 
> DTS> If it gives what you want, fine.  This
> DTS> isn't at all clear to me, because I haven't seen an example.  I
> DTS> wouldn't mind leaving it out.  Maybe there should be some parts of the
> DTS> design that are more tentative than others, and this should be such a
> DTS> part; I can't (for example) see the point in thinking about the
> DTS> semantics of this feature until there's more confidence that it makes
> DTS> sense with respect to the needs that have been expressed.
> 
> (Surprisingly) in Munich I found I wasn't the only one in favour of
> them.  Exercise: try to linearize the modules used to specify a window
> system by Guttag and Horning in "Formal Specification as a Design
> Tool", Proc. POPL'80, pp. 251-261.

I know that there are examples in which modules appear to require
reference to each other.  The question is whether or not what you are
proposing is going to give you what you need, or anything close.  I
think somebody needs to work through at least one example to check
this.  The full version of my 1983 ASL paper with Martin Wirsing has
an example of a recursive parameterized specification of sets but it
wasn't easy to get the example right (i.e. to give what one would
expect from a specification of sets) and the parameterization
mechanism had to be adapted from our original design to allow the
fitting morphism to be passed to the body.  I don't know if another
look at this now would give something better, and maybe Martin has
even looked at this issue in the meantime.  What I do know is that it
is necessary to proceed with care, and that the obvious thing doesn't
necessarily give you what you want.

> ***  Decompositional specs
> 
> MWa> It surprised me that DECOMPOSITION and SPEC are disjoint. In particular, if
> MWa> a specification contains at least one DECOMPOSITION unit, it is itself a
> MWa> DECOMPOSITION and not SPEC.
> MWa> As far as I understand the sparse Part III, one cannot make a decomposition
> MWa> unit U and write a specification 'extend U  by XX'. I imagine that such a
> MWa> specification would make sense - it requires a (separate)  implementation
> MWa> of U but allows one to extend it non-functionally by XX (it would be
> MWa> something like the function from algebras for U to the classes of algebras
> MWa> for XX (extending U).) Similarly, a parameterized specification could have
> MWa> some parameters which are DECOMPOSITION units while others not (or not
> MWa> yet). I imagine that this kind of mixtures of decomposition and other
> MWa> (structured) specs do arise in the development  when various components are
> MWa> refined independently.
> 
> Don? Andrzej?

In my (our) understanding of the semantics of extend and of
decompositional specifications,
	extend <decompositional spec> by ...
makes no sense because extend operates on specifications (classes of
models) and a decompositional spec denotes a class of functions.  Of
course, this doesn't say that it wouldn't be possible to give it a
semantics.  It sounds like what you want is to write (forgive my use
of a different notation)
	extend (Pi X.SP[X]) by ABC
instead of
	Pi X. (extend SP[X] by ABC)

A different question is how much to allow decompositional
specifications to mix with ordinary specifications.  In ASL+
(described near the end of our "parameterisation revisited" paper
without giving it that name), lots of mixing is allowed.  So you get
requirements specifications parameterised by algebras, decompositional
specifications parameterised by requirements specifications, etc., and
so on including higher-order parameterisation.  Going this far seems
wrong for the audience we are trying to reach.  Maybe there is
something in between that would be okay, but I don't know what it is
-- we were unsuccessful in selling even very mild extensions of what
is there now.

> *** BASIC SPECIFICATIONS
> 
> *** 1:
>  
> DTS> Constraints can be regarded as special sentences.
> 
> But not in this institution, I thought?

What I meant was that the definition of Sen(Sigma) could be changed as
follows:
	Sen(Sigma) = Sen(Sigma) as in 0.92
		     union
		     constraints over Sigma
where a constraint over Sigma is a 4-tuple (S,TF,PF,sigma) such that
sigma:Sigma'->Sigma is a signature morphism and (S,TF,PF) is a
constraint as in 0.92 over the signature Sigma', i.e. S,TF,PF are all
from Sigma'.  The idea is that (S,TF,PF) is as before and sigma is
responsible for adapting the constraint to a different signature as
required e.g. when building big structured specs from smaller specs
containing constraints.  Satisfaction is defined by
	M |= (S,TF,PF,sigma)
	iff
	Mod(sigma)(M) |= (S,TF,PF) according to 0.92
and translation of constraints along signature morphisms is defined by
	Sen(sigma')(S,TF,PF,sigma) = (S, TF, PF, sigma;sigma')
where sigma;sigma' is composition in diagrammatic order.  This is the
usual way to handle constraints in an institution.  You are of course
right that constraints are not in general expressible using the other
sentences.

[OK, I'll try to incorporate that change.  --PDM]

> *** 4.3:
> 
> DTS> ... It seems to me that we can
> DTS> always use total instantiation:
> DTS>         fun F(X) = G(A,X)
> DTS> rather than
> DTS>         spec/fun? F = G(A)
> 
> Michel's proposal was (I think) to write e.g.
> 
>   fun G(X,Y) = ...
>   fun F(X)   = ...G(B for Y)...
>   fun H(Y)   = ...G(A for X)...
> 
> allowing the partially-instantiated G to be extended etc., but
> insisting on the remaining parameter(s) being mentioned in the
> declarations of F and H.  
> 
> With positional parameters one writes instead of the above:
> 
>   fun G(X,Y) = ...
>   fun F(X)   = ...G(X,B)...
>   fun H(Y)   = ...G(A,Y)...
> 
> The difference doesn't seem that big.  Positional parameters seem to
> have a simpler syntax and semantics, but have pragmatic drawbacks
> (e.g., when one realizes that a further parameter should be abstracted
> from an existing function body).

If I understand correctly: I think the pragmatic drawbacks you mention
are outweighed by the pragmatic advantages of having things explicit
rather than implicit and the fact that what I am suggesting is simple
and familiar to any programmer while what Michel is suggesting is a
little unusual.

[I'm inclined to agree with you - but Michel will not be able to
comment for at least another week, so let's wait with trying to reach
a consensus on the issues concerning parametrization until then. --PDM]


> DTS> Finally, what about local or let declarations?  E.g. (concrete syntax)
> DTS>     SPEC ::= ... | let LIBRARY in SPEC
> DTS> (and similarly for SPEC-FUN and DECOMPOSITION) and/or
> DTS>     LIBRARY-SECTION ::= ... | local LIBRARY in LIBRARY-SECTION
> 
> I'd expect libraries to be implemented as separately-parsed text
> files.  Allowing libraries nested in SPEC etc. might hinder this.
> What other languages allow this? - apart from ML, of course... :-)

"Library" is our name for a sequence of declarations.  A real library
would normally be in a file somewhere.  A single local declaration or
short sequence of such declarations is also a library in our sense,

[Thanks, that was the confusion.  --PDM]

but importing it from a file would have little point.  I'm thinking of
things like

	let SP = something
	in <expression containing SP more than once>

All reasonable languages allow this, including ML.

[Are there any other reasonable languages?  :-)  --PDM]