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:

References

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store