\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}

% Texttt curly brackets

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

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

\newcommand{\rewrites}{\Rightarrow}

\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}}

\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}

\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}

%% 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}

\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 ??\\[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. Section \ref{subsec:abs-syntax}

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

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

are generated in Maude, while Section \ref{sec:imp_dg} explains how

they are translated 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{Data structures}\label{sec:da}

\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{Conclusions and future work}\label{sec:conclusions}

\input{conclusions}

{\small

\bibliographystyle{abbrv}

\bibliography{alberto}

}

\end{document}