\documentclass[10pt,a4paper]{article}

\usepackage{geometry}

\geometry{a4paper}

\geometry{margin=2.5cm,nohead}

\usepackage{amsfonts}

\usepackage[leqno]{amsmath}

\usepackage{rotating}

\usepackage[english]{babel}

\usepackage{url}

\usepackage{proof}

\usepackage{alltt}

\usepackage{hyperref}

\usepackage{verbatim}

\usepackage{amssymb}

\usepackage{xspace}

\usepackage{xypic}

\usepackage{hetcasl}

\usepackage{wrapfig}

\usepackage{graphicx}

\usepackage{proof}

\usepackage{hetcasl}

% Images

%\renewcommand{\topfraction}{0.95}

%\renewcommand{\textfraction}{0.1}

%\renewcommand{\floatpagefraction}{0.75}

% Texttt curly brackets

\newcommand{\ttlcb}{\texttt{\char'173}}

\newcommand{\ttrcb}{\texttt{\char'175}}

\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}

\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil

\penalty50\hskip1em\null\nobreak\hfil\squareforqed

\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}

\newtheorem{definition}{Definition} %[chapter]

\newtheorem{proposition}{Proposition} %[chapter]

\newtheorem{property}{Property} %[chapter]

\newtheorem{lemma}{Lemma} %[chapter]

\newtheorem{theorem}{Theorem} %[chapter]

\newenvironment{proof}{\par\addvspace{\bigskipamount}%

\noindent\textit{Proof.}\ }{\qed\par\addvspace{\bigskipamount}}

\newcommand{\stroke}{|}

\newcommand{\forget}[1]{|_{#1}}

\newcommand{\Mod}{\mathbf{Mod}}

\newcommand{\Sen}{\mathbf{Sen}}

\newcommand{\red}{\upharpoonright}

\newcommand{\codesize}{\small}

\newcommand{\field}[1]{\mathbb{#1}}

\newcommand{\vertex}[1]{\|\,#1\,\|}

\newcommand{\mt}{{\small$\blacktriangle$}}

\newcommand{\leaf}[1]{{\small$\blacktriangle\;$}#1{\small$\;\blacktriangle$}}

\newcommand{\nodo}[1]{\rule[-.5ex]{0pt}{2.4ex}\,#1\,}

%\newcommand{\lab}[1]{\!\raisebox{0.5ex}{\scriptsize\textsf{#1}}}

\newcommand{\lab}[1]{\!{\scriptsize\textsf{#1}}}

\newcommand{\labb}[2]{\!{\scriptsize\textsf{#1}_\textsf{#2}}}

\newcommand{\labapt}[2]{{\scriptstyle\;\textsf{#1}_\textsf{#2}}}

\newcommand{\model}{\mathcal{A}} % use: $\model$

\newcommand{\stepRule}[1]{\scriptstyle{ #1}}

\newcommand{\den}[1]{[\![#1]\!]_\model} % use: $\den{e}$

\newcommand{\bigunion}{\mathop{ \mathgroup\symoperators \bigcup}}

\newcommand{\fracc}[2]{\begin{array}{c}{#1}\\ \hline {#2} \end{array}}

\newcommand{\Hets}{\textmd{\textsc{Hets}}\xspace}

\newcommand{\CASL}{\textmd{\textsc{Casl}}\xspace}

\newcommand{\CoFI}{\textmd{\textsc{CoFI}}\xspace}

\newcommand{\free}[2]{\mbox{\textbf{free} $#1$ \textbf{along} $#2$}}

\newcommand{\rewrites}{\Rightarrow}

%% macros for development graphs

\newcommand{\glinka}[3]{\!\xymatrix{{#1} \ar@{=>}[r]^{#2} & {#3}}\!\!}

\newcommand{\longglinka}[3]{\!\xymatrix{#1 \ar@{=>}[rr]^{#2} && #3}\!\!}

\newcommand{\llinka}[3]{\!\xymatrix{#1 \ar[r]^{#2} & #3}\!\!}

\newcommand{\hlinka}[3]{\!\xymatrix{#1 \ar@{=>}[r]^{#2}_{\mathit{hide}} & #3}\!\!}

\newcommand{\longhlinka}[3]{\!\xymatrix{#1 \ar@{=>}[rr]^{#2}_{\mathit{hide}} && #3}\!\!}

\newcommand{\flinka}[3]{\!\xymatrix{#1 \ar@{=>}[r]^{#2}_{\mathit{free}} & #3}\!\!}

\newcommand{\longflinka}[3]{\!\xymatrix{#1 \ar@{=>}[rr]^{#2}_{\mathit{free}} && #3}\!\!}

\newcommand{\tglinka}[3]{\!\xymatrix{#1 \ar@{==>}[r]^{#2} & #3}\!\!}

\newcommand{\longtglinka}[3]{\!\xymatrix{#1 \ar@{==>}[rr]^{#2} && #3}\!\!}

\newcommand{\thlinka}[4]{\!\xymatrix{#1 \ar@{==>}[r]^{#2}_{{\mathit{hide}}\ #3} & #4}\!\!}

\newcommand{\longthlinka}[4]{\!\xymatrix{#1 \ar@{==>}[rr]^{#2}_{{\mathit{hide}}\ #3} && #4}\!\!}

\newcommand{\tflinka}[4]{\!\xymatrix{#1 \ar@{==>}[r]^{#2}_{\mathit{free}\ #3} & #4}\!\!}

\newcommand{\tllinka}[3]{\!\xymatrix{#1 \ar@{-->}[r]^{#2} & #3}\!\!}

\newcommand{\gclinka}[3]{\!\xymatrix{#1 \ar@{=>}[r]^{#2}_{\mathit{cons}} & #3}\!\!}

\newcommand{\gdlinka}[3]{\!\xymatrix{#1 \ar@{=>}[r]^{#2}_{\mathit{def}} & #3}\!\!}

\newcommand{\gmlinka}[3]{\!\xymatrix{#1 \ar@{=>}[r]^{#2}_{\mathit{mono}} & #3}\!\!}

\newcommand{\tclinka}[3]{\!\xymatrix{#1 \ar@{==>}[r]^{#2}_{\mathit{cons}} & #3}\!\!}

\newcommand{\tdlinka}[3]{\!\xymatrix{#1 \ar@{==>}[r]^{#2}_{\mathit{def}} & #3}\!\!}

\newcommand{\tmlinka}[3]{\!\xymatrix{#1 \ar@{==>}[r]^{#2}_{\mathit{mono}} & #3}\!\!}

\newcommand{\longtclinka}[3]{\!\xymatrix{#1 \ar@{==>}[rr]^{#2}_{\mathit{cons}} && #3}\!\!}

\newcommand{\longtdlinka}[3]{\!\xymatrix{#1 \ar@{==>}[rr]^{#2}_{\mathit{def}} && #3}\!\!}

\newcommand{\longtmlinka}[3]{\!\xymatrix{#1 \ar@{==>}[rr]^{#2}_{\mathit{mono}} && #3}\!\!}

\newcommand{\greaches}[1]{\!\xymatrix{\ar@{=>>}[r]^{#1} & }\!\!}

\newcommand{\lreaches}[1]{\!\xymatrix{\ar@{>=>>}[r]^{#1} & }\!\!}

\newtheorem{fact}{Fact}

\newcommand{\mi}[1]{\mathit{#1}}

\graphicspath{{images/}}

\title{Integrating Maude into Hets%

%\thanks{Research supported by MEC Spanish project

%\emph{DESAFIOS} (TIN2006-15660-C02-01) and Comunidad de

%Madrid program \emph{PROMESAS} (S�0505/TIC/0407).}

}

\author{Mihai Codescu, Till Mossakowski,

Adri\'an Riesco, and Christian Maeder\\[.7cm]

\normalsize Technical Report 07/10\\[1ex]

\normalsize\textit{Departamento de Sistemas Inform\'aticos y Computaci\'on}\\

\normalsize\textit{Universidad Complutense de Madrid}\\[.4cm]

September 2010

}

\date{}

%\institute{}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}

%

\maketitle

\thispagestyle{empty}

\newpage

\thispagestyle{empty}

\mbox{}\vfill

\begin{abstract}

Maude modules can be understood as models that can be formally analyzed

and verified with respect to different properties expressing various

formal requirements.

However, Maude lacks the formal tools to perform some of these analyses

and thus they can only be done by hand.

The Heterogeneous Tool Set \Hets is an institution-based

combination of different logics and corresponding rewriting, model

checking, and proof tools.

%

We present in this paper an integration of Maude into \Hets that allows

to use the logics and tools already integrated in \Hets with

Maude specifications. To achieve such integration we have defined an

institution for Maude based on preordered algebras and a comorphism

between Maude and \CASL, the central logic in \Hets.

\smallskip

\noindent\textbf{Keywords:} rewriting logic, heterogeneous specifications,

Maude, \CASL

\end{abstract}

\vfill

\begin{small}

\tableofcontents

\end{small}

\vfill

\mbox{}

\newpage

%\setcounter{page}{1}

\section{Introduction}\label{sec:intro}

\input{intro}

\section{Rewriting logic and Maude}\label{sec:maude}

\input{maude}

\section{\Hets}\label{sec:hets}

\input{hets}

\section{Relating the Maude and \CASL logics}\label{sec:comoprh}

\input{inst}

\section{Building development graphs}\label{sec:dg}

\input{dg}

\section{An example: Reversing lists}\label{ex:rev}

\input{example}

\section{Implementation}\label{sec:implemen}

We describe in this section how the integration described in the

previous sections has been implemented. We have used Maude to parse

Maude modules, taking advantage of the reflective capabilities of rewriting

logic \cite{ClavelMeseguerPalomino07}, while the rest of the system

has been implemented in Haskell, the implementation language of \Hets.

%

Section \ref{subsec:abs-syntax}

shows the abstract syntax used to represent Maude modules in Haskell, while

Section \ref{subsec:maude-parser} presents how these data structures

are generated in Maude. Section \ref{sec:logic_imp} shows how

Maude signatures, sentences, and morphisms are obtained, and

Section \ref{sec:imp_dg} explains how

they are introduced into a development graph. Finally, Section \ref{sec:imp_free}

outlines how the freeness constraints are implemented.

\subsection{Abstract syntax}\label{subsec:abs-syntax}

\input{abs-syntax}

\subsection{Maude parsing}\label{subsec:maude-parser}

\input{maude-parsing}

\subsection{Logic}\label{sec:logic_imp}

\input{logic-imp}

\subsection{Development graph}\label{sec:imp_dg}

\input{imp-dg}

\subsection{Comorphism}\label{sec:comorphism}

\input{imp-comorph}

\subsection{Freeness constraints}\label{sec:imp_free}

\input{freeness}

\section{Concluding remarks and future work}\label{sec:conclusions}

\input{conclusions}

{\small

\bibliographystyle{abbrv}

\bibliography{alberto}

}

\end{document}