[CoFI] Re: Architectural specifications

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

I believe that the considerations presented in a forthcoming note by
Michel Bidoit, Don Sannella and Andrzej Tarlecki lead to the following
modified design for CASL architectural constructs. SORRY: the note is
not available as yet. We hope to have it more-or-less ready for the
meeting in Bremen. What follows is the original section from the
language design proposal with some changes as we hereby propose. 

Andrzej

==============================================================================
\section{Architectural Constructs in CASL}
\label{sec-ArchitecturalConstructs}

This section describes the abstract syntax and determines the intended
interpretation of the language constructs for architectural
specifications, extending that given for basic and structured
specifications in Parts~I and~II.

\begin{grammar}
ARCH-SPEC-DEFN   ::=  arch-spec-defn ARCH-SPEC-NAME ARCH-SPEC
ARCH-SPEC-NAME   ::=  SIMPLE-ID
ARCH-SPEC        ::=  BASIC-ARCH-SPEC | ARCH-SPEC-NAME
SPEC             ::=  ... | ARCH-SPEC
\end{grammar}
An architectural specification definition \gram{ARCH-SPEC-DEFN}
provides a name \gram{ARCH-SPEC-NAME} for an architectural
specification \gram{ARCH-SPEC}.  The use of this \gram{ARCH-SPEC-NAME}
in another \gram{ARCH-SPEC-DEFN} merely introduces a synonym for the
same \gram{ARCH-SPEC}.  The use of an \gram{ARCH-SPEC} as a
\gram{SPEC} is interpreted as the signature and class of models that
consist of all the possible resulting units built by the
\gram{ARCH-SPEC} (in this case the resulting units must not be
parametrized).

\begin{grammar}
BASIC-ARCH-SPEC  ::=  basic-arch-spec UNIT-DECL-DEFN+ RESULT-UNIT
\end{grammar}
A basic architectural specification \gram{BASIC-ARCH-SPEC} consists of
a list of unit declarations and definitions \gram{UNIT-DECL-DEFN+},
together with a description of how such units are to be composed in a
\gram{RESULT-UNIT}.  A model of such an architectural specification
consists of a unit for each \gram{UNIT-DECL-DEFN}, and the described
composition of these units.

\atcomment{no changes so far, except for typos}

\subsection{Unit Declarations and Definitions}

\begin{grammar}
UNIT-DECL-DEFN   ::=  UNIT-DECL | UNIT-DEFN
UNIT-DECL        ::=  unit-decl UNIT-NAME UNIT-IMPORT UNIT-SPEC
UNIT-DEFN        ::=  unit-defn UNIT-NAME UNIT-EXPRESSION
UNIT-NAME        ::=  SIMPLE-ID
UNIT-IMPORT      ::=  unit-import UNIT-TERM*
\end{grammar}
A unit declaration \gram{UNIT-DECL} provides not only a unit
specification \gram{UNIT-SPEC} but also a \gram{UNIT-NAME}, which is
used for referring to the unit in a subsequent \gram{UNIT-EXPRESSION}.
The same unit may be used more than once in the composition. In
addition, a \gram{UNIT-IMPORT} clause lists the units that are
imported for the implementation of the declared unit. The imported
units must be declared or defined earlier.

\atcomment{We added the possibility to import some (closed) units
defined/declared earlier. Of course, the actual implementation of a
unit declared with an import clause is in essence generic, since it
has to accommodate an arbitrary actual realisation of the imported
units. So semantically, importing a unit is equivalent to a
declaration of an anonymous generic unit and then its immediate
application to the imported units as actual parameters. But
adding this construct as syntactic sugar corresponds to somewhat
different intuition for the situation where genericity is used only as
an information barrier, with no intention of multiple instances.}


A unit definition \gram{UNIT-DEFN} names the unit resulting from the
composition expressed by its \gram{UNIT-EXPRESSION}.  The visibility of
unit-names in architectural specifications is linear: each name has
to be declared or defined before it is used in a \gram{UNIT-EXPRESSION}.

\atcomment{I renamed \gram{UNIT-TERM} to \gram{UNIT-EXPRESSION} to
accommodate definitions of generic units (definitions of
closed units only were allowed so far).}

No \gram{UNIT-NAME} may be introduced more than once in a particular
architectural specification.

\begin{grammar}
UNIT-SPEC-DEFN   ::=  unit-spec-defn UNIT-SPEC-NAME UNIT-SPEC
UNIT-SPEC        ::=  UNIT-SPEC-NAME | UNIT-TYPE | ARCH-SPEC
UNIT-TYPE        ::=  unit-type SPEC* SPEC
UNIT-SPEC-NAME   ::=  SIMPLE-ID
\end{grammar}
A unit specification definition \gram{UNIT-SPEC-DEFN} provides a name
\gram{UNIT-SPEC-NAME} for a unit specification \gram{UNIT-SPEC}, which
is either a \gram{UNIT-TYPE} or the name \gram{UNIT-SPEC-NAME} of
another unit specification. A unit satisfies a \gram{UNIT-TYPE} when
it is a persistent function that maps compatible tuples of models of
the argument specifications \gram{SPEC*} to models of their extension
by the result specification \gram{SPEC}.

\atcomment{No changes in unit specifications, except for adding the
possibility to use architectural specifications as unit
specifications. This was possible so far only indirectly, via the
coercion to structured specifications, and so for architectural
specifications of closed units only.}


\subsection{Unit Compositions}

\atcomment{Considerable changes here. Unit application allowed with
fitting morphisms and amalgamation/pushout semantics. Unit reduction
redesigned to fit what seems to be emerging for structured specs (from
the concrete syntax I saw). Unit translation, amalgamation and local
unit definitions added. In this way we seem to have here counterparts
to all the constructs in the structured specification --- with a
crucially different semantics, however. This is easiest to notice when
considering the difference between union and amalgamation as well as
between translation and unit translation. For units, static semantics
will require that there is enough sharing ensured that the constructs
as applied to the given units make sense and produce results. This is
in contrast with the constructs for structured specifications where
union and (non-injective) translation might introduce
inconsistencies.}

\begin{grammar}
RESULT-UNIT      ::=  result-unit UNIT-EXPRESSION
UNIT-EXPRESSION  ::=  unit-expression UNIT-BINDING* UNIT-TERM
UNIT-BINDING     ::=  unit-binding UNIT-NAME UNIT-SPEC
UNIT-TERM        ::=  UNIT-APPL | UNIT-REDUCTION | UNIT-TRANSLATION
                   |  AMALGAMATION | LOCAL-UNIT
\end{grammar}
A \gram{RESULT-UNIT} determines how the units declared (or defined) in
the enclosing architectural specification are to be composed, using a
\gram{UNIT-TERM} built from applications \gram{UNIT-APPL}, reductions
\gram{UNIT-REDUCTION}, unit translations \gram{UNIT-TRANSLATION} and
amalgamations \gram{AMALGAMATION}, as well as allowing for the
possibility of local unit definitions in \gram{LOCAL-UNIT}.

Taking the \gram{UNIT-TYPE} of each \gram{UNIT-NAME} from its
declaration, the \gram{UNIT-TERM} must be well-typed. All the
constructs involved must get argument units over the appropriate
signatures.

The auxiliary unit bindings \gram{UNIT-BINDING*} (which are like unit
declarations but with no possibility of importing other units) in a
\gram{UNIT-EXPRESSION} are for (non-parametrized) units that are
required, but not specified, by the enclosing architectural
specification; this allows compositions which express partial
architectural specifications that depend on external units as
specified in the declarations.

\begin{grammar}
UNIT-APPL        ::=  unit-appl UNIT-NAME FITTING-ARG-UNIT*
FITTING-ARG-UNIT ::=  fitting-arg-unit UNIT-TERM SYMB-MAP*
\end{grammar}

A fitting argument \gram{FITTING-ARG-UNIT} fits the argument unit
given by \gram{UNIT-TERM} to the corresponding formal argument for the
generic unit \gram{UNIT-NAME} via a signature morphism determined by
\gram{SYMB-MAP*}. Unmapped symbols are included unchanged.
Of course, the signature of the actual argument might coincide with
the corresponding signature in the generic unit type, in which case no
extra fitting is needed, and the argument unit is passed to the
generic unit directly.
The compatibility of the arguments must be ensured (by checking that
common symbols originate from the same unit declaration).

\begin{grammar}
UNIT-REDUCTION   ::=  unit-reduction UNIT-TERM RESTRICTION
RESTRICTION      ::=  HIDING | REVEALING
HIDING           ::=  hiding SYMB+
REVEALING        ::=  revealing SYMB-OR-MAP+
SYMB-OR-MAP      ::=  SYMB | SYM-MAP
\end{grammar}

A unit reduct \gram{UNIT-REDUCTION} allows parts of the unit to be
hidden or renamed.

\atcomment{The slight generalisation of revealing here follows what
seems to be happening in structured specifications these days
(according to the [imminent --PDM] concrete syntax proposal). Both
here and there this works as a composition of the obvious reduction
followed by translation, as introduced for units below.}

\begin{grammar}
UNIT-TRANSLATION ::=  unit-translation UNIT-TERM SYMB-MAP*
\end{grammar}

A unit translation \gram{UNIT-TRANSLATION} allows some of the unit
symbols to be renamed. Any symbols that happen to be identified
by the renaming must be checked to come from the same symbol in
some unit.

\begin{grammar}
AMALGAMATION     ::=  amalgamation UNIT-TERM+
\end{grammar}

\gram{AMALGAMATION} produces a unit that consists of the components of
all the amalgamated units put together. Compatibility of the unit
terms must be ensured.

\begin{grammar}
LOCAL-UNIT       ::=  local-unit UNIT-DEFN UNIT-TERM
\end{grammar}

This allows for naming a unit locally defined for use in the
\gram{UNIT-TERM}.

\atcomment{No particularly strong presure from me to add local unit
definitions at this stage --- this can be skipped now, as any
definition which is meant to be local can just as well be put as a
unit definition in the given arch spec (modulo name clashes to be
avoided). However, I consider it useful, so let me as well try to
propose having them in.  [Presumably examples illustrating the claimed
usefulness will be included in the promised note...  --PDM]}
==============================================================================