Views

For a view having an object-oriented theory as its source, 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 C . A 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 with the declaration of the given message.