Prev Up
Go backward to 3.5 Parameterized Programming
Go up to 3 Full Maude

3.6 Syntactic Restrictions and Caveats

We can write functional and system modules in Full Maude as we do it in Core Maude, but enclosing them in parentheses. However, there are some syntactic differences between what is currently allowed in Core Maude and in Full Maude. As a consequence, some syntactic restrictions should be taken into account when using Full Maude to write specifications:

  1. Operator and message names have to be given in their equivalent single identifier form when they are declared, and
  2. sort names used in term qualifications and in sort tests have to be in their equivalent single identifier form.
We plan to remove these syntactic restrictions in a future version. In the rest of the section we explain them in some detail and give some hints on how to avoid them.

Operator names have to be given as a single identifier. To declare multi-identifier operators they have to be given 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 use its single identifier form _less`than`or`equal_. Except for having to use the single identifier form in the operator name, the declaration of operations is exactly as for Core Maude. For example, the declaration of this operator on sort, say, Int is as follows. 

 
    op _less`than`or`equal_ : Int Int -> Bool .
Notice 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 write 
 
    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 .
Notice that, 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 with syntax, say, (_)credit_ the declaration has to be given as follows. 

 
    msg `(_`)credit_ : Oid MachineInt -> Msg .
And the same applies to declarations of multiple message names: 
 
    msgs `(_`)credit_ `(_`)debit_ : Oid MachineInt -> Msg .

The last problem mentioned at the beginning of this section has to do with the qualification of terms by sort names and with sort tests. Since qualifications by sort and sort tests--as well as parentheses, polymorphism, and other syntactic features in the extended signature of a specification-are directly handled by Core Maude, and Core Maude does not know about parameterized sorts, the user is forced to use in these cases 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`]. Similarly, to check whether a term T has the sort List[Nat] we have to write T : List`[Nat`] or T :: List`[Nat`].

We plan to add to the Maude system new functionality supporting a more flexible treatment of the syntax of Full Maude and other languages, so that these syntactic restrictions will eventually be removed.

Prev Up