VIEW-DEFN ::= view-defn VIEW-NAME GENERICITY VIEW-TYPE SYMB-MAP-ITEMS*
VIEW-TYPE ::= view-type SPEC SPEC
A view definition VIEW-DEFN with some generic parameters is written:
When the list of generic parameters is empty, the view definition is simply written:
- view
- VN [SP1] ... [SPn] : SP to SP' =
- SM
- end
The terminating `end' keyword is optional.
- view
- VN : SP to SP' =
- SM
- end
It declares the view name VN to have the type of specification morphisms from SP to SP', and defines it by the symbol mapping SM. [CHANGED:] Symbol mappings SM are described in Sections 6.4 and 6.5. The view definition is well-formed only if the set of signature morphisms determined by the symbol mapping SM, as explained in Chapter 5, is a singleton. [] The definition extends the global environment (which must not already include a definition for VN).
Generic parameters in a view definition allow the same view to be instantiated with different fitting arguments, giving compositions of the morphism defined by the view with other fitting morphisms. [CHANGED:] The source SP of the view is not in the scope of the view parameters SP1, ..., SPn, and view instantiation affects only the target of the generic view. [] It is required that the reduct by the specification morphism of each model of the target SP' is a model of the source SP; otherwise the semantics is undefined.
VIEW-NAME ::= SIMPLE-ID
A view name VIEW-NAME is normally displayed in a SMALL-CAPS font, and input in mixed upper and lower case.