UNIT-TERM ::= UNIT-REDUCTION | UNIT-TRANSLATION | AMALGAMATION
| LOCAL-UNIT | UNIT-APPL
Unit terms provide counterparts to most of the constructs of structured specifications: translations, reductions, amalgamations (corresponding to unions), local unit definitions, and applications (corresponding to instantiations).
Unit terms use the same notation as structured specifications--but 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 requires that enough sharing is ensured so that the constructs as applied to the given units will always make sense and produce results. This is in contrast with the constructs for structured specifications, where union and (non-injective) translation might introduce inconsistencies.
[CHANGED:] Any sharing of symbols in a unit term must be supported by a sharing of symbols in a common unit. (In the presence of subsorts, the notion of sharing here is related to the overloading relation.) [] Taking the unit type of each unit name from its declaration, the unit term must be well-typed. All the constructs involved must get argument units over the appropriate signatures.