7 Architectural Concepts |

The intention with architectural specifications is primarily to
impose structure on models, expressing their ** composition**
from component units--and thereby also a

The component units may all be regarded as ** unit
functions**: functions without arguments give self-contained units;
functions with arguments use such units in constructing further units.
Note that a resulting unit may be needed for use as an argument in
more than one application.

The specification of a unit function indicates the properties to be assumed of the arguments, and the properties to be guaranteed of the result. Such a specification provides the appropriate interfaces for the development of the function. In CASL, self-contained units are simply models as defined in Part I, and their properties are expressed by ordinary (perhaps structured) specifications.

Thus a unit function maps models of argument specifications to models
of a result specification. A specification of such functions can be
simply a list of the argument specifications together with the result
specification. Thinking of argument and result specifications as
*types* of models, a specification of a unit function may be
regarded as a *function type*.

An entire ** architectural specification** is a collection of
unit function specifications, together with a description of how the
functions are to be composed to give a resulting unit. A model of an
architectural specification is a collection of unit functions with the
specified types or definitions, together with the result of composing
them as described.

The intention is that a unit function should actually make use of its
arguments. In particular, it should not re-implement the argument
specifications. This is ensured by requiring the unit function to be
*persistent*: the reduct of the result to each argument signature
yields exactly the given arguments.

As a consequence, the result *signature* has to include each
argument *signature*--any desired hiding has to be left to when
functions are composed. Moreover, since each *symbol* in the
union of the argument signatures has to be implemented the same way in
the result as in each argument where it occurs, the arguments must
already have the same implementation of all common symbols.
In the absence of subsorts, this is sufficient to allow one to
unambiguously *amalgamate* arguments into a single model over the
union of argument signatures. When subsorts are present, extra
conditions to ensure that implicit subsort embeddings can be defined
unambiguously in such an amalgamated model may be necessary. Let us
call arguments satisfying such a requirement ** compatible**.

Hence the interpretation of the specification of a unit function is as
all *persistent* functions from *compatible* tuples of
models of the argument specifications to models of the result
specification. When composing such functions, care must be taken to
ensure that arguments are indeed compatible. Notice that if two
arguments have the same signature, the arguments must be identical.
It is not possible to specify a function that should take two
arguments that implement the same signature independently--although
one can get the same effect, by renaming one or both of the argument
signatures.

CoFI Document: CASL/Summary -- Version: 1.0.1 -- 25 March 2001.

Comments to cofi-language@brics.dk

7 Architectural Concepts |