Comments on v0.95 FINAL DRAFT - App. C

[pdmosses@brics.dk (Peter D. Mosses)]

Comments on v0.95 FINAL DRAFT, App. C

[REMINDER: the DEADLINE FOR COMMENTS on the FINAL DRAFT is TODAY! 
--PDM]

Contents: 
- Attributions 
- Downloading 
- Local definitions and declarations

[This message expresses PDM's personal opinions, which do not
necessarily reflect those of the other Language Design task group
participants. --PDM]

*** Basic Constructs: Attributions

The attribution of properties to functions, as proposed in App. C, is
of purely pragmatic signficance, in connection with tools and
methodology: semantically, an attribution merely abbreviates some
axioms that could have been spelled out directly, using other
constructs.  One might also let attibutions of properties such as
associativity and commutativity have implications for parsing of
concrete syntax, but such aspects are not covered by the current
proposal.  [Issues related to concrete syntax are to be studied by
Language Design and Tools task groups early in 1997.  --PDM]

What are the alternatives to the current proposal for adding the
ATTRIBUTION construct to CASL?

(i) One might decide that the axioms for associativity, commutativity,
etc., should not be abbreviated at all.  Then some kind of annotation
would be needed, in connection with e.g. rewriting tools, to
facilitate location of such axioms.  But really, it is quite tedious
to spell out (and read!) such boring axioms, and some way of
abbreviating them would surely be appreciated by (potential) users.
(See my book on action semantics [Cambridge Tracts in TCS 26, CUP,
1992] for lots of examples of algebraic specifications making use of
associative functions.  Those of us who prefer to construct e.g. lists
using cons, rather than concatenation, probably don't feel the same
need for abbreviation...) 

(ii) One might exploit (presumably pre-defined) generic specifications
that provide the appropriate axioms for arbitrary parameter (sorts
and) functions, and instantiate with arguments fitting these sorts and
functions to the intended ones.  However, an instantiation is not a
BASIC-ITEM, so it could not be given along with the various
declarations and axioms within a BASIC-SPEC, making things quite
awkward.  Moreover, having to mention the fitting of the parameter
sorts (as well as the functions) would look clumsy, and (in simple
cases, at least) not give any real abbreviation at all.  [Higher-order
techniques, involving predicates that take functions as arguments, are
not available in the main CASL language. --PDM]

(iii) One might follow OBJ and some other languages by adding
PROPERTY* as a component of a FUN-DECL (and omitting ATTRIBUTION from
BASIC-ITEM).  Then the semantics would be exactly as the declaration
of FUN-DECL without the PROPERTY*, together with the proposed
ATTRIBUTION.  By bundling the PROPERTY* together with the FUN-DECL,
one forbids the following:
- augmenting the attributes of functions that were already declared in
  a specification being extended; 
- attributing the same set of properties simultaneously to several
  functions with different profiles;
- attributing one or more properties to all the (currently) declared
  functions with a particular name.
Perhaps this would not be any great loss; perhaps there might
also be some advantages of the discipline of attributing properties
only when declaring functions?

Note in connection with (iii) that it might be in any case useful to
allow PROPERTY* as a component of a FUN-DECL, as well as allowing the
separate ATTRIBUTION construct, so that repetition of the declared
function name can be avoided.

Since attributions (as proposed) have only very local impact on the
language design (and on semantics) it seems to me better to include
them straight away.  (Like all other constructs) they may be removed
later if they give rise to unexpected problems.  A fuller
investigation of the methodological and tools aspects of attributions
should be made early in 1997.

*** Library Constructs: Downloading

The proposed DOWNLOAD construct is motivated by the following
considerations (following discussions on the topic with Bernd): 

- encourage references to specifications that are developed/maintained
  at remote sites;

- discourage ad-hoc copying of specifications from remote
  sites/directories;

- avoid multiple references to the same remote library;

- make downloading from a particular library an atomic transaction;

- allow downloading only the needed specifications; 

- allow renaming of specifications when downloading, to avoid clashes
  with local (spec) names;

- avoid awareness of the names of any auxiliary specifications that
  are used by the downloaded ones;

- make all names available for reference in a local library evident;

- allow relative URLs, replacing them by absolute URLs when copying to
  other libraries.  BTW, cyclic or self-referential downloads are to be
  forbidden.

*** Various Constructs: Local declarations and definitions

I'm not so enthusiastic for these proposals, and I've never felt the
need for such constructs when writing algebraic specifications myself
- but others seem to think that they are essential, and they don't
cost too much extra syntax.  Let's include them (in some form)
straight away, and see how much they get used in the examples that
we'll be developing... we can always throw them out again later, if it
turns out that they very rarely get used.  However:

local-basic-items BASIC-ITEM* BASIC-ITEM* - this seems to be very
close to regarding the symbols declared by the first BASIC-ITEM* as
automatically hidden in the enclosing BASIC-SPEC.  Why not simply
allow:
  BASIC-ITEM ::= HIDDEN-DECLS
  HIDDEN-DECLS ::= hidden-decls SIG-DECL* 
instead?  N.B. it is pragmatically important not to have to list all
the hidden symbols declared in SIG-DECL* separately!

local-library-items LIBRARY-ITEM* LIBRARY-ITEM* - this allows
arbitrarily-deep nesting of LIBRARY-ITEM, and is unlikely to be as
easy to implement as the original proposal in Part IV; to me, it seems
like overkill.  The current proposal for DOWNLOADs (which seems to be
fairly easily implementable) allows a large library to be split into a
number of smaller libraries, such that any names not explicitly
downloaded from the subsidiary libraries are effectively hidden.  
I suspect that this degree of control might be adequate in practice.  
If one also wanted, when defining the name of a library-item, to
indicate that this was not to be available outside the current library
(i.e., hidden), this would be easy to add, without involving nested
LIBRARY-ITEMs.

Peter Mosses