Module importations in Maude
In Maude, a module can be imported as a submodule of another in three different modes:
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:
protectingmode shows no junk and no confusion.
extendingmode is to allow junk, but to rule out confusion.
includingmode is to allow junk and/or confusion.