Additions to CASL Rationale; minor addition to CASL; EXTENSION

[pdmosses@brics.dk]

Contents:

- additions to CASL Rationale 
  (attributions - variable declarations - visibility and scope)

- proposal for minor addition to CASL v0.96
  (attributions combined with function declarations)

- clarification concerning EXTENSION

COMMENTS are welcome! - also on all other parts of the CASL Rationale.

*** DEADLINE: Sunday 18 May 

The CASL Rationale will be finalized for v0.97 on Monday 19 May.

I'm still hoping to finalize the CASL Summary v0.97 by this coming
Wednesday, taking account of all comments received by:

*** DEADLINE: MIDNIGHT TONIGHT!

(OK: 8am Danish time tomorrow will be acceptable too :-)

Sorry that I couldn't find time for these things earlier...

Peter

_______________________________________

*** ADDITION TO CASL RATIONALE:

Attributions
____________

    Properties such as associativity may be attributed to functions.

Some properties of (binary) functions are particularly significant for
tools.  For instance, associativity may be relevant when parsing
specifications that use infix notation: repeated applications may be
left ungrouped, since all possible groupings are semantically
equivalent.  Associativity, commutativity, idempotence, and unit
properties may also be significant for term-rewriting tools.

Attributions of properties such as associativity to functions are
familiar from (e.g.) OBJ3, where they are specified together with
function declarations.  CASL [might allow this in v0.97, see
accompanying proposal below, but in any case] allows attributions to
be specified as separate items, so that further properties may be
attributed to previously-declared functions in extensions of
specifications.  Moreover, CASL allows the concise attribution of the
same properties to an arbitrary list of functions, possibly having
different profiles.

    Attributions are distinct from axioms.

Properties like associativity may also be asserted using axioms.  For
conciseness, such axioms could also be specified generically, and
instantiated for particular sorts and functions.  Tools, however, need
to be able to distinguish attributions from general axioms, which
motivates CASL providing a separate construct for them.



*** ADDITION TO CASL RATIONALE:

Variable Declarations
_____________________

    Declarations of variables provide implicit universal quantification.

Axioms in algebraic specifications are typically intended to be
universally quantified over all the (sorted) variables that occur in
them.  Such quantifications may be given explicitly in CASL, with
variables of particular sorts declared for use in individual formulae.

It is also possible in CASL to abbreviate universal quantifications
that are common to different axioms, by giving variable declarations
separately, as items of basic specifications.  The effect of such a
variable declaration is implicit universal quantification with that
variable of all the axioms of the enclosing basic specification; but
variable declarations do not contribute to the signature determined by
the specification, so they do not affect other axioms.  

Quantification over variables that do not occur (freely) in a formula
is always semantically irrelevant in CASL, since models with empty
carriers are not allowed.  Thus one may also regard the implicit
quantification as being limited to the freely-occurring variables.



*** ADDITION TO CASL RATIONALE:

Visibility and Scope
____________________

    The order in which items of basic specifications are listed
    is insignficant.

Basic specifications in CASL involve items of various syntactic
categories: signature declarations (sorts, subsorts, functions,
predicates, datatypes), variable declarations, attributions, axioms,
and sort generation constraints.  

In many cases, it is possible to group these items in a natural order:
first sort and subsort declarations, then function and predicate
declarations, etc., and finally the axioms) with each item referring
only to the symbols declared in the preceding items.  However, it may
also be desirable to group axioms together with the sorts, functions,
and predicates that they define, or to defer the declarations and
axioms concerning auxiliary entities (to be hidden) to the end of the
list.  Moreover, datatype declarations may often be best presented in
a `top-down' order (cf. the grammar for the abstract syntax of CASL);
they may also involve `mutual recursion' that cannot be linearized at
all (unless extra declarations of sorts are inserted).

Such considerations motivated the CASL design decision to allow items
of basic specifications to be listed in any order.  Thus parsers
(human or otherwise) for CASL have to take account of the entire
enclosing basic specification regarding declarations of the symbols
used in each item.  On the other hand, they do not have to keep track
of a varying local environment, reflecting the scopes of declarations
within basic specifications.

Note that the structured specifications of CASL [v0.96] do allow
linear visibility to be expressed: by means of a list of extensions,
where each step of extension might even be essentially a single
declaration or axiom (but note that the scopes of variable
declarations are limited to the list of basic items in which they
occur).  And the specification of auxiliary entities may be separated
as a local specification, which corresponds to a combination of
extension and hiding.


*** PROPOSAL for v0.97:  Allow attribution of properties also in FUN-DECL

Constants and Functions
_______________________

         FUN-DECL ::= fun-decl FUN-NAME+ FUN-TYPE PROPERTY* 
...  
A function declaration FUN-DECL determines that each function name in
the list FUN-NAME+ is in the signature, being in the set of partial or
total function symbols, and with the argument sorts SORT+ and result
! SORT as specified by the function type FUN-TYPE.  When the list
! PROPERTY* is non-empty, it determines moreover evident sentences
! asserting that each of the functions is to have each of the specified
! properties (see \ref{Attributions}).


*** CLARIFICATION:

The following comment in a recent message was misleading:

  This motivated the new syntax for EXTENSION in v0.96.  I see that
  the comment in the CASL Rationale on this point is misleading, it's
  not entirely a matter of `convenience'; I'll try and amplify on it in
  the next version.

In fact the possibility of a list of extensions is merely for
convenience: binary extension is associative, so the grouping is
irrelevant, just like for union, conjunction, etc.; the same for
binary conservative extension.  The essential point for expressiveness
is to be able to specify
  (extension conservative SP1 (extension non-conservative SP2 SP3))
to ensure that the models of SP1 are protected in the result.