Module importations in Maude

In Maude, a module can be imported as a submodule of another in three different modes: protecting, extending, including. This is done with the syntax declarations

protecting ⟨ModuleExpression⟩ . 
extending ⟨ModuleExpression⟩ . 
including ⟨ModuleExpression⟩ .

which can be abbreviated, respectively, to

pr ⟨ModuleExpression⟩ . 
ex ⟨ModuleExpression⟩ . 
inc ⟨ModuleExpression⟩ .

The different modes of importation can be understood as promises by the user, which would need to be proved by him/herself. Before explaining each difference, I clarify no junk and no confusion. No junk is that extra values should not be added. No confusion is that different values should not be made equal.

The different modes of importation is as follows:

• protecting mode shows no junk and no confusion.
• extending mode is to allow junk, but to rule out confusion.
• including mode is to allow junk and/or confusion.

References

• http://maude.lcc.uma.es/manual271/maude-manualch6.html