Specifications and code should be structured in modules of relatively small size to facilitate understandability of large systems, increase reusability of components, and localize the effects of system changes. In Maude, the fullest support of these goals is achieved in Full Maude, which has a rich and extensible module algebra supporting, in particular, parameterized programming techniques in the OBJ3 style [27]. However, Core Maude provides already some useful basic support for modularity by allowing the definition of module hierarchies, that is, acyclic graphs of module importations. Mathematically, we can think of such hierarchies as partial orders of theory inclusions, that is, the theory of the importing module contains the theories of its submodules as subtheories.
Recall that a rewrite theory is a four-tuple R= (Omega,E,L,R), where (Omega,E) is a theory in membership equational logic. As already mentioned, and further explained in Section 4, a system module is a rewrite theory with initial semantics. Note that we can use the inclusion of membership equational logic into rewriting logic to view a functional module specifying an equational theory (Omega,E) as a degenerate case of a rewrite theory, namely the rewrite theory (Omega,E,Ø,Ø). In fact the initial algebra of (Omega,E) and the initial model of (Omega,E,Ø,Ø) coincide [37]. Therefore, in essence we can view all modules as rewrite theories.
The most general form of module inclusion is provided by the including keyword, followed by the nonempty list of imported modules and finished by a period. The protecting keyword is a more restricted form of inclusion, in the sense that it makes a semantic assertion about the relationship between the initial models of the two theories. Let R = (Omega,E,L,R) be the rewrite theory specified by a system module, and let R'=(Omega',E',L',R') be the theory of a supermodule, so that we have a theory inclusion R c R'. Then, we can view each model M' of R' as a model M'|R of R, simply by disregarding the extra sorts, operations, equations, membership axioms, and rules in R'-R. Since, as further explained in Section 4, the rewrite theories R and R' have respective initial models TR and TR', by initiality of TR we always have a unique R-homomorphims
h:TR --> TR'|R.The protecting importation asserts that for each sort s in the signature Omega of R' the function hs is an isomorphism of categories12. Intuitively, this means that the initial model of the supermodule does not add any "junk" or any "confusion" to the initial model of the submodule.
Of course, the protecting assertion cannot be checked by Maude at runtime. It requires inductive theorem proving. Using the proof techniques in [4] together with an inductive theorem prover for membership equational logic and a Church-Rosser checker such as those described in [12], this can be done for functional modules; and it seems natural to expect that these techniques and tools will extend to similar ones for rewrite theories.
By contrast, the including assertion does not make such requirements on h. It does, however, make some requirements. Namely, if the subtheory R does itself contain a proper subtheory R0 that it imports in protecting mode, then the inclusion R0 c R' does still have to be protecting. If we do not want it to be, we have to say so by explicitly listing the module defining R0 in the list of modules imported in including mode.
We give below an example of a module hierarchy, namely, the number hierarchy from the naturals to the rationals in a somewhat different form than in Appendix C.7 of [27]. This hierarchy happens to be a linear order of theory inclusions, with BOOL implicitly at the bottom. In general, any partial order of inclusions can be defined in the same way. Note that all the importations are protecting importations. The including importation, although possible in Core Maude, is more natural in the context of a module renaming operation. Indeed, if the semantics of a module is going to be modified by a supermodule it is better to make a copy of such a module and import the copy. At present, Core Maude does not support renaming; it is supported by Full Maude (see Section 3.5.4). Renaming will probably be added to Core Maude in a future version.
fmod NAT is
sorts Nat NzNat Zero .
subsorts Zero NzNat < Nat .
op 0 : -> Zero .
op s_ : Nat -> NzNat .
op p_ : NzNat -> Nat .
op _+_ : Nat Nat -> Nat [comm] .
op _*_ : Nat Nat -> Nat [comm] .
op _*_ : NzNat NzNat -> NzNat [comm] .
op _>_ : Nat Nat -> Bool .
op d : Nat Nat -> Nat [comm] .
op quot : Nat NzNat -> Nat .
op gcd : NzNat NzNat -> NzNat [comm] .
vars N M : Nat .
vars N' M' : NzNat .
eq p s N = N .
eq N + 0 = N .
eq (s N) + (s M) = s s (N + M) .
eq N * 0 = 0 .
eq (s N) * (s M) = s (N + (M + (N * M))) .
eq 0 > M = false .
eq N' > 0 = true .
eq s N > s M = N > M .
eq d(0, N) = N .
eq d(s N, s M) = d(N, M) .
ceq quot(N, M') = s quot(d(N, M'), M') if N > M' .
eq quot(M', M') = s 0 .
ceq quot(N, M') = 0 if M' > N .
eq gcd(N', N') = N' .
ceq gcd(N', M') = gcd(d(N', M'), M') if N' > M' .
endfm
fmod INT is
sorts Int NzInt .
protecting NAT .
subsort Nat < Int .
subsorts NzNat < NzInt < Int .
op -_ : Int -> Int .
op -_ : NzInt -> NzInt .
op _+_ : Int Int -> Int [comm] .
op _*_ : Int Int -> Int [comm] .
op _*_ : NzInt NzInt -> NzInt [comm] .
op quot : Int NzInt -> Int .
op gcd : NzInt NzInt -> NzNat [comm] .
vars I J : Int .
vars I' J' : NzInt .
vars N' M' : NzNat .
eq - - I = I .
eq - 0 = 0 .
eq I + 0 = I .
eq M' + (- M') = 0 .
ceq M' + (- N') = - d(N', M') if N' > M' .
ceq M' + (- N') = d(N', M') if M' > N' .
eq (- I) + (- J) = - (I + J) .
eq I * 0 = 0 .
eq I * (- J) = - (I * J) .
eq quot(0, I') = 0 .
eq quot(- I', J') = - quot(I', J') .
eq quot(I', - J') = - quot(I', J') .
eq gcd(- I', J') = gcd(I', J') .
endfm
fmod RAT is
sorts Rat NzRat .
protecting INT .
subsort Int < Rat .
subsorts NzInt < NzRat < Rat .
op _/_ : Rat NzRat -> Rat .
op _/_ : NzRat NzRat -> NzRat .
op -_ : Rat -> Rat .
op -_ : NzRat -> NzRat .
op _+_ : Rat Rat -> Rat [comm] .
op _*_ : Rat Rat -> Rat [comm] .
op _*_ : NzRat NzRat -> NzRat [comm] .
vars I' J' : NzInt . vars R S : Rat .
vars R' S' : NzRat .
eq R / (R' / S') = (R * S') / R' .
eq (R / R') / S' = R / (R' * S') .
ceq J' / I'
= quot(J', gcd(J', I')) / quot(I', gcd(J', I'))
if gcd(J', I') > s 0 .
eq R / s 0 = R .
eq 0 / R' = 0 .
eq R / (- R') = (- R) / R' .
eq - (R / R') = (- R) / R' .
eq R + (S / R') = ((R * R') + S) / R' .
eq R * (S / R') = (R * S) / R' .
endfm