Differences between Full Maude and Core Maude

Apart from those features available in Full Maude that are not supported in Core Maude (discussed above in Section 14.3 and later in Chapter 15), we find a number of differences between Full Maude and Core Maude. There are some obvious ones, like the fact that any module, theory, view or command entered into Full Maude must be enclosed in parentheses, or the differences in printing, tracing, debugging, etc., but there are also others that impose certain limitations on the specifications themselves:

1. Operator and message names have to be given in their equivalent single-identifier form when they are declared (see below), but they can later be written in the usual way in statements and in terms for evaluation.
2. Sort names used in term qualifications, membership assertions, and on-the-fly declarations of variables have to be in their equivalent single-identifier form.
3. The continue, show component, show path, and show search graph commands are not supported in Full Maude.
4. Full Maude does not support external objects either.

In the rest of the section we explain the first two restrictions in some detail and give some hints on how to avoid them.

An operator name has to be given as a single identifier; multi-identifier operators have to be declared in their single-identifier form, that is, each identifier in a multi-identifier name has to be preceded by a backquote. For example, to define an operator with name _less than or equal_, we have to declare it in its single identifier form _less`than`or`equal_. Except for having to use the single-identifier form in the operator name, the declaration of operators is exactly as in Core Maude. For example, the declaration of this operator on sort, say, Int is as follows.

    op _less`than`or`equal_ : Int Int -> Bool .

Remember that not only blank spaces, but also the special characters `{', `}', `(', `)', `[', `]' and `,' break the identifiers. Therefore, to declare in Full Maude an operator such as {_} taking an element of sort, say, Int and with value sort Set, we should add appropriate backquotes, as follows:

    op `{_`} : Int -> Set .

As in Core Maude, several operators with the same arity and coarity can be defined in the same declaration using the keyword ops, but, again, each operator name has to be given in its single-identifier form. We could have for example the following declaration.

    ops _`{_`} _`,_ : Foo Bar -> Baz .

Since each operator name is a single identifier, parentheses are not needed to indicate the boundaries between the syntactic forms of the different operators.

As for operator names, message names can be mixfix, but they have to be declared in single-identifier form. Thus, to define a message credit in an object-oriented module (see Chapter 15) with syntax, say, (_)credit_ the declaration has to be given as follows.

    msg `(_`)credit_ : Oid Nat -> Msg .

And the same applies to declarations of multiple message names:

    msgs `(_`)credit_ `(_`)debit_ : Oid Nat -> Msg .

The second problem mentioned at the beginning of this section affects the qualification of terms by sort names, on-the-fly declarations of variables, and membership assertions. In these three situations, the user must use the names of parameterized sorts, not as he or she has defined them, but in their equivalent single-identifier form. Thus, if we have, for example, a sort List{Nat} and a constant nil in it, if necessary, it should be qualified as (nil).List`{Nat`}. A variable L of sort List{Nat} being declared on the fly should be written L:List`{Nat`}. Similarly, to check whether a term T has sort List{Nat} we have to write T : List`{Nat`} or T :: List`{Nat`}, depending on the kind of sort check we wish to perform.