The intention with architectural specifications is primarily to
impose structure on models, expressing their *composition*
from component units--and thereby also a *decomposition* of
the task of developing such models from requirements specifications.
This is in contrast to the structured specifications summarized in
Part II, where the specified models
have no more structure than do those of the basic specifications
summarized in Part I.

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. Let us
call such arguments *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 specification, the corresponding 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-v1.0 -- Version: 1.0 -- 22 October 1998.

Comments to cofi-language@brics.dk