Module importations in Maude
1 min readSep 8, 2020
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.