We use views to assert how a particular target module or theory is claimed to satisfy38 a source theory. In general, there may be several ways in which such requirements might be satisfied, if at all, by the target module or theory; that is, there can be many different views, each specifying a particular interpretation of the source theory in the target.
In the current version of Full Maude, default views are not supported. Therefore, all views have to be defined explicitly, and all of them must have a name. As any theory or module, views should have been defined before they are used.
In the definition of a view we have to indicate its name, the source theory, the target module or theory, and the mapping of each sort, function, class, and message in the source theory. Although the current version does not support default views in the style of OBJ3, "obvious" parts of a mapping do not need to be explicitly given, namely, any identical mapping of a function, message, or attribute f to itself such that its arity and coarity are mapped to those of an operator, message, or attribute with the same name in the target can be omitted. However, maps for all sorts in the source theory have to be given, even when they are identity maps.
The mapping of a sort S in the source theory to a sort S' in the target is expressed with syntax sort S to S' . The mapping of operators is expressed with syntax op O to O' . where O is an operator identifier or an operator identifier together with its arity and value sort. An operator map in which explicit arity and coarity are given affects, not only the operators with such arity and coarity, but the entire family of subsort-overloaded operators (see Section 2.1.1) associated to the given operator. The target operators can be derived operators, that is, they can be terms with variables. Therefore, we can map a function symbol, not only to another function symbol, but also to an expression. Consider, for example, the case in which we want to define a view from a theory in which we have a "less or equal" operator _<=_, defined with reflexivity, symmetry and transitivity equations, to a module in which such an operator does not exist but we have an operator "less than" _<_. Then, we can define a view with a map
op X <= Y to term X < Y or X == Y .
The mapping of a class C in the source theory to a class C' in the target is expressed with syntax class C to C' . Attribute maps have the form attr A . C to A' . where A is the name of an attribute of class C in the source theory and A' is an attribute of the image class of C under the view. The mapping of messages is expressed with syntax msg M to M' . where M is a message identifier or a message identifier together with its arity and value sort. As for operators, a message map in which explicit arity and coarity are given affects the entire family of subsort-overloaded message declarations associated to the declaration of the given message.
The syntax for views is given by the following declarations.
op op_to term_. : Bubble Bubble -> ViewDecl .
op op_to_. : Token Token -> ViewDecl .
op op_:_->_to_. : Token SortList Sort Token -> ViewDecl .
op op_: ->_to_. : Token Sort Token -> ViewDecl .
op sort_to_. : Sort Sort -> ViewDecl .
op class_to_. : Sort Sort -> ViewDecl .
op attr_._to_. : Token Sort Token -> ViewDecl .
op msg_to_. : Token Token -> ViewDecl .
op msg_:_->_to_. : Token SortList Sort Token -> ViewDecl .
op msg_: ->_to_. : Token Sort Token -> ViewDecl .
subsorts VarDecl < ViewDecl < ViewDeclList .
subsort VarDeclList < ViewDeclList .
op __ : ViewDeclList ViewDeclList -> ViewDeclList [assoc] .
op view_from_to_is_endv :
ViewToken ModExp ModExp ViewDeclList -> PreView .
Thus, we can have a view
(view MachineInt from TRIV to MACHINE-INT is
sort Elt to MachineInt .
endv)
which defines a view from the theory TRIV to the module
MACHINE-INT. In views from TRIV we encourage the convention
of naming such views by the name of the sort to which Elt is
mapped. Although it is not necessary to follow this convention, it can add
understandability to the specifications. What has to be avoided is using the
labels in interfaces of parameterized modules as names of views, since this
can sometimes generate ambiguities.
We can have views between theories, which is particularly useful to compose instantiations of views to link the formal parameter of some parameterized module to some actual parameter via some intermediate formal parameter of another parameterized module. We will give some examples in the coming sections. An example of a view whose target is a theory is the following.
(view Toset from TRIV to TOSET is
sort Elt to Elt .
endv)
As already mentioned, in some cases it is useful to be able to express mappings of functions, not to other functions but to expressions. For example, the _<_ relation of a toset can be mapped to an expression using the "less than or equal" operator _<=_ and the inequality operator _=/=_ as follows.
(view MachIntAsToset from TOSET to MACHINE-INT is
sort Elt to MachineInt .
vars X Y : Elt .
op X < Y to term X <= Y and X =/= Y .
endv)
Notice that, when dealing with parameterized modules with structured theories as parameters, as in the TOSET-PAIR example discussed in Section 3.5.1, we have to give a view not only for the top theory but for the entire "loose part," that is, for all other subtheories imported by the theory. In the near future we plan to handle parameterized theories and views as well, as a way to give more structure to both theories and views.