N.B. Views have only recently been incorporated in CASL, and their syntax and semantics have not yet been finalized. In fact the present version of this section differs significantly from the previous draft version, as it no longer relies on names of specifications to determine the applicability of views; it also makes the parameters of generic views explicit.
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. 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.
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.