An operator can have several subsort-overloaded instances. Maude requires that all these instances should have the same attributes, except for the case of the ctor attribute, that may be present in some instances but absent in others (see Section 4.4.3), and/or the metadata attribute (see Section 4.5.2). It is for example forbidden to have a subsort-overloaded instance in which an operator is declared assoc only, and another such instance in which it is declared assoc and comm.
The ditto attribute can be given to an operator for which another subsort-overloaded instance has already appeared, either in the same module or in a submodule. The ditto attribute is just a shorthand stating that this operator, being subsort overloaded, should have the same attributes as those appearing explicitly in a previous subsort-overloaded version, except for the ctor and metadata attributes, which are outside the scope of ditto. In this way we can avoid writing out a possibly long attribute list again and again.
It is not allowed to combine ditto with other attributes, except for ctor and metadata. That is, an operator given the ditto attribute either has no other explicitly given attributes, or can only have in addition either the ctor attribute if it is a constructor, or a metadata attribute, or both the ctor and metadata attributes. Furthermore, it is forbidden to use ditto on the first declared instance of an operator, since this is nonsensical.
In our numbers module we can add equational attributes to the declarations
of _+_ and _*_, and then use ditto to declare the
same attributes in other subsort-overloaded versions.
ops _+_ _*_ : Nat Nat -> Nat [assoc comm]. op _+_ : NzNat Nat -> NzNat [ditto] . op _*_ : NzNat NzNat -> NzNat [ditto] .
For an example making extensive use of the ditto attribute see the LTL-SIMPLIFIER module (in the file model-checker.maude), discussed in Chapter 10.