Up Next
Go up to 8 Architectural Constructs
Go forward to 8.2 Unit Compositions

8.1 Unit Declarations

UNIT-DECL       ::=   unit-decl UNIT-NAME UNIT-SPEC
UNIT-NAME       ::=   SIMPLE-ID
Each unit declaration UNIT-DECL provides not only a unit specification UNIT-SPEC but also a UNIT-NAME, which is used for referring to the unit in the specification of the result unit.
[TM] As far as I understood is, the result unit is being defined and not specified?!?
Discharged: This is right.
The same unit may be used more than once in the composition. No UNIT-NAME may be declared more than once in a particular architectural specification. 

UNIT-SPEC-DEFN  ::=   unit-spec-defn SPEC-NAME UNIT-SPEC
UNIT-SPEC       ::=   UNIT-TYPE | SPEC-NAME
UNIT-TYPE       ::=   unit-type SPEC* SPEC
A unit specification definition UNIT-SPEC-DEFN provides a name SPEC-NAME for a unit specification UNIT-SPEC, which is either a UNIT-TYPE or the name SPEC-NAME of another unit specification.
[HB] What if SPEC-NAME in UNIT-SPEC refers to a generic specification instead of a unit specification? See comment about SPEC-INST in a preceding section.
Discharged: This can't happen -- it can only be a UNIT-SPEC-NAME.
A unit satisfies a UNIT-TYPE when it is a persistent function that maps compatible tuples of models of the argument specifications SPEC* to models of their extension by the result specification SPEC. A UNIT-TYPE is well-formed only when the signature of the union of the argument specifications is included in the signature of the result.
[AT] I am not sure if UNIT-SPEC or only UNIT-TYPE should be allowed in UNIT-SPEC-DEFN. UNIT-TYPE here would perhaps be more uniform with other definitions (ARCH-SPEC-DEFN, SPEC-DEFN) where we cannot refer directly to a named specification in the library. On the other hand, re-using a named unit specification defined earlier in a library may need a bit more writing than in other cases (in the case when the unit is parameterised, some eta-expansion might be required).
Discharged: ARCH-SPEC can now be ARCH-SPEC-NAME, and UNIT-SPEC can be UNIT-SPEC-NAME.
[AT] As far as I can see, we can now refer (at least according to the syntax) to architectural specifications as specs (as a parameterless generic spec instantiated with no arguments) and as unit specs only if they are named (in a definition in a library). Is any of these possibilities supposed to be excluded by context conditions? I guess we could allow this, but perhaps something has to be said about this, and the meaning of the coercion involved should be made clear.

But is it intended that anonymous architectural specifications cannot be used as specs? I guess I do not mind this, at least in the case of specs. For unit specs, it just might be natural to use unnamed architectural specs, say as follows: 

arch spec
     unit F : SP1 -> SP
     unit U : arch spec
                   unit X : SP
                   result T1
              end
     result T2
end
But now there may be a question of visibility of units raised:
  • Can T1 use F?
  • Can T2 use X (qualified as "the X that comes from U")?
I think that an ultimate answer might be yes in both cases, but we might prefer to keep it as no for now. The former question does not arise if we allow only named architectural specifications to be used as unit specs. ([HB] T2 shouldn't be able to use X. U is an architectural specification converted to a unit specification and a unit specification has no components. In any case, there should be no difference whether one writes an anonymous architectural specification or uses a named one from the library. Either one has access to the components of an architectural specification or one doesn't.)
Discharged: We now have three categories of specification names, with a coercion from architectural specifications to ordinary specifications as mentioned earlier. The example is not legal, and there is no visibility through architectural specification boundaries, as HB points out.
CoFI Note: S-1 --Version 1.3-- 25 April 1997.
Comments to cofi-semantics@brics.dk

Up Next