dg.tex revision c1cf2f634a37116ff90e99ca710179a23115cbfb
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoWe show in this section the details of the generation of development
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescographs for Maude specifications.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\subsection{Parameterized modules}
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoAs we have seen in Section \ref{subsec:pmod}, parameterized modules
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoreceive a list of parameters $P_i$ each one associated to a module
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoexpression $M_i$. Since these module expressions are theories, they
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescocan have sorts that are not instantiated yet, so to avoid clash of
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesconames these sorts are qualified with the parameter name. These
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoqualifications induce an implicit morphism in the definition links
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoof the development graph between the theory and the parameterized
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\subsection{Module expressions}
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoMaude module expressions allow to combine and modify the information
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescocontained in Maude modules.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\begin{itemize}
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\item The summation expression of the module expressions $\mathit{ME}_1$ and
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco$\mathit{ME}_2$ generates a new node in the development graph
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco$(\mathit{ME}_1 + \mathit{ME}_2)$ with
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescothe union of the information in both expressions. A definition link
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescois also created between the original expressions and the resulting one.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\item The renaming expression $\mathit{ME} * (R)$ creates a morphism with
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescothe information given in $R$ that will be used in the link
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\item The instantiation module expression\footnote{This module expression
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescocannot be used in Core Maude in all places where the rest of expressions
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescocan be used, for more information see \cite{maude-book}} assigns a view
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoor a parameter to each of the
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoNote that an instantiation generates some implicit morphisms and modifies
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescothe ones stated in the views:
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\begin{itemize}
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\item When the parameter is instantiated with a view
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\item As explained in the previous section, parameterized modules can
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescodefine sorts of the form \verb"name{X1, ..., Xn}", where \verb"X1, ..., Xn"
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoare parameter names that can be instantiated or bound by new parameters.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoThus, in addition to the morphism
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\item When the module expression is a simple identifier the development
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescograph remains unchanged.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\subsection{Importations}
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoMaude allow three different kinds of module importation:
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\begin{itemize}
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\item Protecting, that means that \emph{no junk} and \emph{no confusion}
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoare added to the imported module expression.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\item Extending, that means that allows ``junk'' to be added to imported
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescomodule expression, while ``confusion'' is forbidden.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\item Including, that allows both ``junk'' and ``confusion'' to be
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoadded to the imported module expression.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoEach of these importation modes generates links with different proofs
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoobligations in the development graph:
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\begin{itemize}
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\item When a module expression $M_1$ is imported in protecting mode
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoby a module $M_2$ a new node $M_1'$ with the same signature that $M_1$
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescois generated and a free link between $M_1$ and $M_1'$
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoplaced, while a definition link between $M_1'$ and $M_2$.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\item Extending mode generates a theorem link with the annotation
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\verb"PCons", standing for proof-theoretic conservativity. This
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoconstraint cannot be discharged in the current version of the system.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\item Including mode generates a definition link from the imported module
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoexpression to the module that imports it.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoThe morphism in all these links depends of the type of module expression.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoIt will be an inclusion if the module expression does not contains a
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescorenaming, while it be a morphism in other case.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\subsection{Views}
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoMaude views have a theory as source and either a module or a theory
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoas target. All the sorts and operators declared in the source theory
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescohave to be mapped to sorts and operators in the target
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoA particular case of mapping between operators is the mapping between
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoterms, that has the general form \emph{op $e$ to term $t$}
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescowhere $e$ is a term consisting of a
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescosingle operator applied to variables�declared either on-the-�y or with
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescovariable declarations in the same view and the target term is any term
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescowith variables, those in the source $e$ in the corresponding sorts
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoresulting from the mapping.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoSince this shortcut allows to map operators with different profiles,