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.