UserGuide.tex revision c449906d0bfb0da56e503edfe7f5e998268e33b2
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder\documentclass{article}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\usepackage[show]{ed} % set to hide for producing a released version
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\usepackage{alltt}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder\usepackage{casl}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder\usepackage{xspace}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder\usepackage{color}
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder\usepackage{url}
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder\usepackage{threeparttable,hhline}
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder\usepackage[pdfborder=0 0 0,bookmarks,
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroederpdfauthor={Till Mossakowski, Christian Maeder, Mihai Codescu},
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroederpdftitle={Hets User Guide}]
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder{hyperref} %% do not load more packages after this line!!
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newcommand{\QUERY}[1]%{}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder\newcommand{\eat}[1]{}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder\newcommand{\IEXT}[1] {\\#1\I}
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder\newcommand{\IEND} {\I\END}
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder\newenvironment{EXAMPLEFORMAT} {}{}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder%% Added by MB to have some extra vertical space after the ``main'' examples
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder%% following the points (and some others in the text):
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newenvironment{BIGEXAMPLE} {\begin{EXAMPLE}} {\end{EXAMPLE}\medskip}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder\newenvironment{DETAILSFORMAT} {}{}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder\newenvironment{META}[1][] {#1\begin{METAFORMAT}}{\end{METAFORMAT}}
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder\newenvironment{METAFORMAT} {\medskip\vrule\hspace{1ex}\vrule\hspace{1ex}%
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder \begin{minipage}{0.9\textwidth}\it}
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder {\end{minipage}\par\medskip}
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder\newcommand{\SLIDESMALL} {}
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder\newcommand{\SLIDESONLY}[1] {}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder% SIMULATING SMALL-CAPS FOR BOLD, EMPH
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder%\newcommand {\CoFI}{CoFI\xspace}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newcommand{\largeELAN} {\largeTEXTSC{E}{LAN}\xspace}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newcommand {\HOL}{\normalTEXTSC{H}{OL}\xspace}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newcommand {\Isabelle}{\normalTEXTSC{I}{SABELLE}\xspace}
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newcommand {\SPASS}{\normalTEXTSC{S}{PASS}\xspace}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder%%%%% Klaus macros
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder\newcommand{\SROIQ}{$\mathcal{SROIQ}$(\textbf{D})\xspace}
25b4f7a4c38ef3061268cbb8c1281f957782fdbdJonathan von Schroeder\newcommand{\DL}{DL\xspace}
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder%%%%% end of Klaus macros
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder\newcommand{\LCF}{LCF\xspace}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder\newcommand{\ASF}{ASF\xspace}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder\newcommand{\SDF}{SDF\xspace}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder%% Do NOT use \ASF+\SDF (it gives a superfluous space in the middle)
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder\newcommand{\CCC}{CCC\xspace}
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder\newcommand{\CoCASL}{\normalTEXTSC{C}{O}\normalTEXTSC{C}{ASL}\xspace}
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder\newcommand{\CspCASL}{\normalTEXTSC{C}{SP}-\normalTEXTSC{C}{ASL}\xspace}
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroeder\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroeder\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroeder\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroeder\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\begin{document}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\title{{\bf \protect{\LARGEHets} User Guide}\\
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder-- Version 0.95 --}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\author{Till Mossakowski, Christian Maeder, Klaus L\"{u}ttich\\[1em]
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederDFKI Lab Bremen, Bremen, Germany.\\[1em]
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederComments to: hets-users@informatik.uni-bremen.de \\
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder(the latter needs subscription to the mailing list)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\section{Introduction}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von SchroederThe central idea of the Heterogeneous Tool Set (\protect\Hets) is to
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroederprovide a general framework for formal methods integration and proof
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroedermanagement. One can think of \Hets acting like a motherboard where
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroederdifferent expansion cards can be plugged in, the expansion cards here
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroederbeing individual logics (with their analysis and proof tools) as well
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroederas logic translations. Individual logics and their analysis and proof
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroedertools can be plugged into the \Hets motherboard using an
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroederobject-oriented interface based on institutions
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder\cite{GoguenBurstall92}. The \Hets motherboard already has plugged in
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroedera number of expansion cards (e.g., the theorem provers Isabelle, SPASS
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroederand more, as well as model finders). Hence, a variety of tools is
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroederavailable, without the need to hard-wire each tool to the logic at
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder \includegraphics[width=0.45\textwidth]{hets-motherboard}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder\caption{The \Hets motherboard and some expansion cards}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder\Hets supports a number of input languages directly, such as \CASL,
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von SchroederCommon Logic, OWL-DL, Haskell, and Maude. For heterogeneous
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroederspecification, \Hets offers language heterogeneous \CASL.
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von SchroederHeterogeneous \CASL (\HetCASL) generalises the structuring
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder\CASL \cite{CASL-UM,CASL/RefManual} to arbitrary logics
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder(if they are formalised as institutions and plugged into
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroederthe \Hets motherboard), as well as to heterogeneous
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroedercombination of specification written in different logics.
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von SchroederFig.~\ref{fig:lang} for a simple subset of the
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder\HetCASL syntax, where \emph{basic specifications} are unstructured
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroederspecifications or modules written in a specific logic. The graph of
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroedercurrently supported logics and logic translations (the latter are also
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroedercalled comorphisms) is shown in Fig.~\ref{fig:LogicGraph}, and the
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroederdegree of support by \Hets in Fig.~\ref{fig:Languages}.
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroeder\begin{figure}[ht]
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroeder\begin{verbatim}
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von SchroederSPEC ::= BASIC-SPEC
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroeder | SPEC then SPEC
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroeder | SPEC then %implies SPEC
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroeder | SPEC with SYMBOL-MAP
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroeder | SPEC with logic ID
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von SchroederDEFINITION ::= logic ID
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroeder | spec ID = SPEC end
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroeder | view ID : SPEC to SPEC = SYMBOL-MAP end
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder | view ID : SPEC to SPEC = with logic ID end
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von SchroederLIBRARY = DEFINITION*
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder\caption{Syntax of a simple subset of the heterogeneous
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroederspecification language.
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder\texttt{BASIC-SPEC} and \texttt{SYMBOL-MAP} have a logic
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroederspecific syntax, while \texttt{ID} stands for some form of
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederidentifiers.\label{fig:lang}
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von SchroederWith \emph{heterogeneous structured specifications}, it is possible to
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroedercombine and rename specifications, hide parts thereof, and also
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroedertranslate them to other logics. \emph{Architectural specifications}
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroederprescribe the structure of implementations. \emph{Specification
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder libraries} are collections of named structured and architectural
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder\Hets consists of logic-specific tools for the parsing and static
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroederanalysis of the different involved logics, as well as a
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroederlogic-independent parsing and static analysis tool for structured and
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroederarchitectural specifications and libraries. The latter of course needs
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroederto call the logic-specific tools whenever a basic specification is
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroeder\Hets is based on the theory of institutions \cite{GoguenBurstall92},
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroederwhich formalize the notion of a logic. The theory behind \Hets is laid
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroederout in \cite{Habil}. A short overview of \Hets is given in
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroeder\cite{MossakowskiEA06,MossakowskiEtAl07b}.
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder\section{Logics supported by Hets}
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von SchroederThe following list of logics (formalized as so-called institutions
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder\cite{GoguenBurstall92}) is currently supported by \Hets:
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder \includegraphics[scale=0.4]{LogicGraph}
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroeder\caption{Graph of logics currently supported by \Hets. The more an
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroederellipse is filled with green, the more stable is the implementation of the logic. Blue indicates a prover-supported logic.}
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroeder\label{fig:LogicGraph}
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder\begin{tabular}{|l|c|c|c|}\hline
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von SchroederLanguage & Parser & Static Analysis & Prover \\\hline
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder\CASL & x & x & - \\\hline
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder\CoCASL & x & x & - \\\hline
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder\ModalCASL & x & x & - \\\hline
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder\HasCASL & x & x & - \\\hline
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von SchroederHaskell & (x) & x & - \\\hline
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroeder\CspCASL & x & x & - \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\CspCASL\_Trace & - & - & x \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\CspCASL\_Failure & - & - & - \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederConstraint\CASL & x & (x) & - \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederTemporal & x & (x) & - \\\hline
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von SchroederRelScheme & x & (x) & - \\\hline
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von SchroederDFOL & x & (x) & - \\\hline
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von SchroederExtModal & x & (x) & - \\\hline
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von SchroederLF & x & (x) & - \\\hline
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder%Structured specifications & x & x & (x) \\\hline
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder%Architectural specifications & x & x & -\\\hline
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder\CASLDL & x & - & - \\\hline
25b4f7a4c38ef3061268cbb8c1281f957782fdbdJonathan von SchroederDMU & x & - & - \\\hline
25b4f7a4c38ef3061268cbb8c1281f957782fdbdJonathan von SchroederOWL DL & x & x & - \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederPropositional & x & x & x \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederSoftFOL & x & - & x \\\hline
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von SchroederMaude & x & x & - \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederVSE & x & x & x \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\Isabelle & (x) & - & x \\\hline
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder\caption{Current degree of \Hets support for the different languages.\label{fig:Languages}}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\begin{description}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\item[CASL] extends many sorted first-order logic with partial
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder functions and subsorting. It also provides induction sentences,
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder expressing the (free) generation of datatypes.
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder%It is mainly designed and used for the
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder%specification of requirements for software systems. But it is also
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder%used for the specification of \Dolce (Descriptive Ontology for
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder%Linguistic and Cognitive Engineering), an Upper Ontology for knowledge
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder%representation. \cite{Gangemi:2002:SOD} Further it is now used to
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder%specify calculi for time and space.
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederFor more details on \CASL see \cite{CASL/RefManual,CASL-UM}.
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von SchroederWe have implemented the \CASL logic in such a way that much of the
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroederimplementation can be re-used for \CASL extensions as well; this
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroederis achieved via ``holes'' (realized via polymorphic variables) in the
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroedertypes for signatures, morphisms, abstract syntax etc. This eases
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroederintegration of \CASL extensions and keeps the effort of integrating
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\CASL extensions quite moderate.
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\item[CoCASL] \cite{MossakowskiEA04} is a coalgebraic extension of \CASL,
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroedersuited for the specification of process types and reactive systems.
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederThe central proof method is coinduction.
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder\item[ModalCASL] \cite{ModalCASL}
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder is an extension of \CASL with multi-modalities and
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroederterm modalities. It allows the specification of modal systems with
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von SchroederKripke's possible worlds semantics. It is also possible to express
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroedercertain forms of dynamic logic.
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\item[HasCASL] is a higher order extension of \CASL allowing
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder polymorphic datatypes and functions. It is closely related to the
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder programming language Haskell and allows program constructs being
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder embedded in the specification.
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroederthe language is summarized in \cite{HasCASL/Summary}, the semantics
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroederin \cite{Schroder05b,Schroder-habil}.
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\item[Haskell] is a modern, pure and strongly typed functional
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder programming language. It simultaneously is the implementation
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder language of \Hets, such that in the future, \Hets might be applied
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederThe definitive reference for Haskell is \cite{PeytonJones03},
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\item[CspCASL] \cite{Roggenbach06} is a combination of \CASL
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder with the process algebra CSP.
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\item[ConstraintCASL] is an experimental logic for the specification
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroederof qualitative constraint calculi.
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\item[OWL DL] is the Web Ontology Language (OWL) recommended by the
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder World Wide Web Consortium (W3C, \url{http://www.w3c.org}). It is
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder used for knowledge representation and the Semantic Web
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder \cite{berners:2001:SWeb}.
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederHets calls an external OWL DL parser
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder written in JAVA to obtain the abstract syntax for an OWL file and its
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder imports. The JAVA parser is also doing a first analysis classifying
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder the OWL ontology into the sublanguages OWL Full, OWL DL and OWL
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder Hets only supports the last two, more restricted variants.
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder structuring of the OWL imports is displayed as Development Graph.
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder\item[CASL-DL] \cite{OWL-CASL-WADT2004}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroederis an extension of a restriction of \CASL, realizing
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroedera strongly typed variant of OWL DL in \CASL syntax.
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder \CASL with cardinality restrictions for the description of sorts and
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder unary predicates. The restrictions are based on the equivalence
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder between \CASLDL, OWL~DL and \SHOIN. Compared to \CASL only unary
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder and binary predicates, predefined datatypes and concepts (subsorts
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder of the topsort Thing) are allowed. It is used to bring OWL DL and
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder \CASL closer together.
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\item[Propositional] is classical propositional logic, with
02ef6fcc031a33d9753dda5a46e6101328b3d7c5Jonathan von Schroederthe zChaff SAT solver \cite{Herbstritt03} connected to it.
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder\item[SoftFOL] \cite{LuettichEA06a} offers three automated theorem
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder proving (ATP) systems for first-order logic with equality: (1) \SPASS
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder \cite{WeidenbachEtAl02}; (2) Vampire \cite{RiazanovV02}; and (3)
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder MathServe Broker\footnote{which chooses an appropriate ATP upon a
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder classification of the FOL problem} \cite{ZimmerAutexier06}.
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder These together comprise some of the most advanced theorem provers
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder for first-order logic.
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder for higher-order logic.
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\end{description}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\ednote{TODO Till: update list}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederVarious logics are supported with proof tools. Proof support for the
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroederother logics can be obtained by using logic translations to a
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederprover-supported logic.
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von SchroederAn introduction to \CASL can be found in the \CASL User Manual
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder\cite{CASL-UM}; the detailed language reference is given in
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroederthe \CASL Reference Manual \cite{CASL/RefManual}. These documents
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroederexplain both the \CASL logic and language of basic specifications as
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroederwell as the logic-independent constructs for structured and
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroederarchitectural specifications. The corresponding document explaining the
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder\HetCASL language constructs for \emph{heterogeneous} structured specifications
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederis the \HetCASL language summary \cite{Mossakowski04}; a formal
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroedersemantics as well as a user manual with more examples are in preparation.
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von SchroederSome of \HetCASL's heterogeneous constructs will be illustrated
b538e214277386123cb6f1ab0c99ae8fd3a03963Jonathan von Schroederin Sect.~\ref{sec:HetSpec} below.
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\section{Logic translations supported
75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder\label{comorphisms}
75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von SchroederLogic translations (formalized as institution comorphisms
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\cite{GoguenRosu02}) translate from a given source logic to a given
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroedertarget logic. More precisely, one and the same logic translation
25b4f7a4c38ef3061268cbb8c1281f957782fdbdJonathan von Schroedermay have several source and target \emph{sub}logics: for
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroedereach source sublogic, the corresponding sublogic of the target
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroederlogic is indicated.
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederA graph of the most important logics and sublogics, together with their
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroedercomorphisms, is shown in Fig.~\ref{fig:SublogicGraph}.
25b4f7a4c38ef3061268cbb8c1281f957782fdbdJonathan von Schroeder \includegraphics[scale=0.4]{SublogicGraph}
e29b8f886533643eb2b9a8601606a9f5e40cd237Jonathan von Schroeder\caption{Graph of most important sublogics currently supported by \Hets,
75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroedertogether with their comorphisms.}
75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von Schroeder\label{fig:SublogicGraph}
75a39ac3eec18df94df1be9c71a1f6b1f94a57a4Jonathan von SchroederIn more detail, the following list of logic translations is currently
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroedersupported by \Hets:
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\ednote{TODO Mihai,Till: check VSE, Maude, DFOL descr. or ref.}
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\begin{tabular}{|l|p{8cm}|}\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederCASL2CoCASL & inclusion \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederCASL2CspCASL & inclusion \\\hline
d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von SchroederCASL2HasCASL & inclusion \\\hline
d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von SchroederCASL2Isabelle & inclusion on sublogic CFOL=
d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroeder(translation $(7)$ of \cite{Mossakowski02}) \\\hline
d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von SchroederCASL2Modal & inclusion \\\hline
d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von SchroederCASL2PCFOL & coding of subsorting (SubPCFOL=) by injections, see Chap.\ III:3.1 of the CASL Reference Manual \cite{CASL/RefManual} \\\hline
d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von SchroederCASL2PCFOLTopSort & coding of subsorting (SulPeCFOL=) by a top sort and unary
d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroederpredicates for the subsorts \\\hline
d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von SchroederCASL2Propositional & translation of propositional FOL \\\hline
d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von SchroederCASL2SoftFOL & coding of CASL.SuleCFOL=E to SoftFOL \cite{LuettichEA06a},
d5d2f79ba9303ff0b00e04eb7b3b5d0bf5c8daaeJonathan von Schroedermapping types to soft types \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederCASL2SoftFOLInduction & same as CASL2SoftFOL but with instances of induction
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroederaxioms for all proof goals \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederCASL2SubCFOL & coding of partial functions by error elements
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder(translation $(4a')$ of \cite{Mossakowski02}, but extended to subsorting, i.e. sublogic SubPCFOL=) \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederCASL2VSE & inclusion on sublogic CFOL= \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederCASL2VSEImport & inclusion on sublogic CFOL= \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederCASL2VSERefine & refining translation of CASL.CFOL= to VSE \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederCASL\_DL2CASL & inclusion \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederCoCASL2CoPCFOL & coding of subsorting by injections, similar to CASL2PCFOL \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederCoCASL2CoSubCFOL & coding of partial functions by error supersorts, similar to CASL2SubCFOL \\\hline
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von SchroederCoCASL2Isabelle & extended translation similar to CASL2Isabelle \\\hline
02ef6fcc031a33d9753dda5a46e6101328b3d7c5Jonathan von SchroederCspCASL2CspCASL\_Failure & inclusion \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederCspCASL2CspCASL\_Trace & inclusion \\\hline
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von SchroederCspCASL2Modal & translating the CASL data part to ModalCASL \\\hline
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von SchroederDFOL2CASL & translating dependent types \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederDMU2OWL & interpreting Catia output as OWL \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroeder\begin{tabular}{|l|p{7cm}|}\hline
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von SchroederHasCASL2HasCASLNoSubtypes & coding out subtypes \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederHasCASL2HasCASLPrograms & coding of \HasCASL axiomatic recursive definitions
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von Schroederas \HasCASL recursive program definitions \\\hline
8f38f1aeb6ac1c9514f8d6d5e509ff7298ed5b78Jonathan von SchroederHasCASL2Haskell & translation of \HasCASL recursive program definitions to Haskell \\\hline
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von SchroederHasCASL2IsabelleOption & coding of HasCASL to Isabelle/HOL \cite{Groening05} \\\hline
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von SchroederHaskell2Isabelle & coding of Haskell to Isabelle/HOL \cite{TorriniEtAl07} \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederHaskell2IsabelleHOLCF & coding of Haskell to Isabelle/HOLCF \cite{TorriniEtAl07} \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederMaude2CASL & inclusion \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederModal2CASL & the standard translation of modal logic
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von Schroederto first-order logic \cite{blackburn_p-etal:2001a} \\\hline
255a89789d3d5b19f6a8c96bf6c260a96158ef6dJonathan von SchroederOWL2CASL & inclusion \\\hline
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von SchroederPropositional2CASL & inclusion \\\hline
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von SchroederRelScheme2CASL & inclusion \\\hline
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder\section{Getting started}
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von SchroederThe latest \Hets version can be obtained from the
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder\Hets tools home page
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder Since \Hets is being
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroederimproved constantly, it is recommended always to use the latest version.
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder\Hets currently is available (on Intel architectures only) for Linux, Solaris
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von SchroederThere are three possibilities to install \Hets:
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder\begin{enumerate}
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von SchroederThe Java-based \Hets installer. Download a \texttt{.jar} file and
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroederjava -jar \texttt{file.jar}
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von SchroederNote that you need Sun Java 1.4.2 or later. On a Mac, you can just
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroederdouble-click on the \texttt{.jar} file.
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von SchroederThe installer will lead you through the installation with
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroedera graphical interface. It will download and install further
62d292e9e9227b10af78c78c6f11074e0d4b0d99Jonathan von Schroedersoftware (if not already installed on your computer):
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder\begin{tabular}{|l|l|p{5cm}|}\hline
Hets-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
uDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
Tcl/Tk & graphics widget system & (version 8.4 or 8.5 must be installed before)\\\hline
\SPASS & theorem prover & \url{http://spass.mpi-sb.mpg.de/}\\\hline
Darwin & theorem prover & should be installed manually from \url{http://combination.cs.uiowa.edu/Darwin/}\\\hline
\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
zChaff & SAT solver & \url{http://www.princeton.edu/~chaff/zchaff.html} \\\hline
minisat & SAT solver & \url{http://minisat.se/} \\\hline
Pellet & OWL reasoner & \url{http://clarkparsia.com/pellet/} \\\hline
& \url{http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/} \\\hline
& \url{http://www.reduce-algebra.com/} \\\hline
Maude & rewrite system & \url{http://maude.cs.uiuc.edu/} \\\hline
Twelf & & \url{http://twelf.plparty.org/} \\\hline
\texttt{Order.casl} (actually, this file is provided
with the \Hets distribution as \texttt{Hets-lib/UserManual/Chapter3.casl}).
\texttt{hets Order.casl}
well as its correctness with respect to the static semantics (e.g.\
Use \texttt{DIR} as a colon separated list of directories for specification libraries (equivalently, you can set the variable \texttt{HETS\_LIB} before
constructs). Within a \HetCASL library, the current logic can be changed e.g.\
fac n = foldl (*) 1 [1..n]
Details can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
Let us extend the above library \texttt{Order.casl}. One use of the
\texttt{hets -g Order.casl}
\texttt{Order.casl}).
\texttt{hets -g Sorting.casl}
assuming that \texttt{Sorting.casl} contains the above specifications.
\I\VIEW \NAMEDEFN{v2}[\NAMEREF{Total\_Order}] ~:~ \NAMEREF{List\_Order\_Sorted}[\NAMEREF{Total\_Order}] \TO
We have already added this view to \texttt{Sorting.casl}.
links in the sense of \cite[IV:4]{CASL/RefManual}).
links in the sense of \cite[IV:4]{CASL/RefManual}.
\cite[IV:4]{CASL/RefManual}. These are usually created after
The ``Hide/show names'' menu is a toggle:
Manual \cite{CASL/RefManual} or one of
\item[Taxonomy graphs] (Only available for some logics) Shows the subsort graph of the signature of the node.
between them, i.e. translation (blue links) and inclusion (black links).
| graph.(exp.dot|dot)
The \texttt{owl} option \cite{books/sp/Kohlhase06} will produce OWL files in
The \texttt{omdoc} format \cite{books/sp/Kohlhase06} is an XML-based
When the \texttt{comptable.xml} format is selected, \Hets will extract
algebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
available from \texttt{www.cofi.info/Libraries}.
printed \LaTeX\ version of \texttt{Order.casl} by typing:
This will generate a file \texttt{Order.pp.tex}. It can be included
into \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
coming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty}) is used.
The format \texttt{pp.xml} represents a library in XML for our change
The \texttt{tptp} format (\url{http://www.tptp.org}) is a standard
\item[\texttt{-l LOGIC}, \texttt{--logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
\item[\texttt{-m FILE}, \texttt{--modelSparQ=FILE}] model check a qualitative calculus given in SparQ lisp notation \cite{SparQ06} against a \CASL specification
% http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0
\url{http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0}
\cite{DBLP:conf/tacas/Aspinall00,url:ProofGeneral} in a separate Emacs
The \Isabelle theory file conforms to the Isabelle/Isar syntax
E-KRHyper\footnote{\url{http://www.uni-koblenz.de/~bpelzer/ekrhyper/}}
KRHyper\footnote{\url{http://www.uni-koblenz.de/~wernhard/krhyper/}} by
version, where e.g.\ error handling is ignored. For technical reasons
the static analysis of basic specifications) and/or translates (along
of the \Hets home page at \url{http://www.dfki.de/sks/hets}.
%\input{hets.tex}