UserGuide.tex revision 12a1614014912501fbfc30a74242d6f3a5c97e80
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\documentclass{article}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{alltt}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{casl}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{color}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\QUERY}[1]%{}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\eat}[1]{}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\IEXT}[1] {\\#1\I}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\IEND} {\I\END}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newenvironment{EXAMPLEFORMAT} {}{}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%% Added by MB to have some extra vertical space after the ``main'' examples
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%% following the points (and some others in the text):
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newenvironment{BIGEXAMPLE} {\begin{EXAMPLE}} {\end{EXAMPLE}\medskip}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newenvironment{DETAILSFORMAT} {}{}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newenvironment{META}[1][] {#1\begin{METAFORMAT}}{\end{METAFORMAT}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newenvironment{METAFORMAT} {\medskip\vrule\hspace{1ex}\vrule\hspace{1ex}%
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \begin{minipage}{0.9\textwidth}\it}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder {\end{minipage}\par\medskip}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\SLIDESMALL} {}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\SLIDESONLY}[1] {}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder% SIMULATING SMALL-CAPS FOR BOLD, EMPH
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%\newcommand {\CoFI}{CoFI\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeELAN} {\largeTEXTSC{E}{LAN}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\HOL}{\normalTEXTSC{H}{OL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\Isabelle}{\normalTEXTSC{I}{SABELLE}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%%%%% Klaus macros
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%%%%% end of Klaus macros
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LCF}{LCF\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\ASF}{ASF\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\SDF}{SDF\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%% Do NOT use \ASF+\SDF (it gives a superfluous space in the middle)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\CCC}{CCC\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\CoCASL}{\normalTEXTSC{C}{O}\normalTEXTSC{C}{ASL}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\CspCASL}{\normalTEXTSC{C}{SP}-\normalTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\begin{document}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\title{{\bf \protect{\LARGEHets} User Guide}\\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder-- Version 0.7 --}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\author{Till Mossakowski, Christian Maeder, Klaus L\"{u}ttich\\[1em]
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederDFKI Lab Bremen, Bremen, Germany.\\[1em]
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederComments to: hets@informatik.uni-bremen.de\\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederor to: hets-users@informatik.uni-bremen.de \\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder(the latter needs subscription to the mailing list)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\section{Introduction}
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederThe Heterogeneous Tool Set (\protect\Hets) is the main analysis tool
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederfor the specification language heterogeneous \CASL. Heterogeneous
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\CASL (\HetCASL) combines the specification language \CASL
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\cite{CASL-UM,CASL/RefManual} with \CASL extensions
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederand sublanguages, as well as completely different logics and even
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederprogramming languages such as Haskell. \HetCASL
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederextends the structuring mechanisms of \CASL:
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\emph{Basic specifications} are
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederunstructured specifications or modules written in a specific logic.
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederThe graph of currently supported logics and logic translations (the
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederlatter are also called comorphisms) is shown in
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederFig.~\ref{fig:LogicGraph}, and the degree of support by \Hets in
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederFig.~\ref{fig:Languages}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederWith \emph{heterogeneous structured specifications}, it is possible to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercombine and rename specifications, hide parts thereof, and also
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedertranslate them to other logics. \emph{Architectural specifications}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederprescribe the structure of implementations. \emph{Specification
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder libraries} are collections of named structured and architectural
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\Hets consists of logic-specific tools for the parsing and static
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederanalysis of the different involved logics, as well as a
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederlogic-independent parsing and static analysis tool for structured and
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederarchitectural specifications and libraries. The latter of course needs
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederto call the logic-specific tools whenever a basic specification is
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\Hets is based on the theory of institutions \cite{GoguenBurstall92},
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederwhich formalize the notion of a logic. The theory behind \Hets is
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederlaid out in \cite{Habil}. A short overview is given in \cite{MossakowskiEA06}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\section{Logics supported by Hets}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe following list of logics (formalized as so-called institutions
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\cite{GoguenBurstall92}) is currently supported by \Hets:
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \includegraphics[scale=0.4]{LogicGraph}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\caption{Graph of logics currently supported by \Hets. The more an
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederellipse is filled with green, the more stable is the implementation of the logic. Blue indicates a prover-supported logic.}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\label{fig:LogicGraph}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{tabular}{|l|c|c|c|}\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederLanguage & Parser & Static Analysis & Prover \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\CASL & x & x & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\CoCASL & x & x & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\ModalCASL & x & x & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\HasCASL & x & x & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHaskell & x & x & -\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\CspCASL & (x) & - & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederConstraint\CASL & x & (x) & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%Structured specifications & x & x & (x) \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%Architectural specifications & x & x & -\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\CASLDL & x & - & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederOWL DL basic & x & (x) & - \\\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederOWL DL structure & x & (x) & - \\\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederPropositional & x & x & - \\\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederSoftFOL & - & - & x \\\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\Isabelle & - & - & x \\\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\caption{Current degree of \Hets support for the different languages.\label{fig:Languages}}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\begin{description}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\item[CASL] extends many sorted first-order logic with partial
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder functions and subsorting. It also provides induction sentences,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder expressing the (free) generation of datatypes.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%It is mainly designed and used for the
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%specification of requirements for software systems. But it is also
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%used for the specification of \Dolce (Descriptive Ontology for
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%Linguistic and Cognitive Engineering), an Upper Ontology for knowledge
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%representation. \cite{Gangemi:2002:SOD} Further it is now used to
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%specify calculi for time and space.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederFor more details on \CASL see \cite{CASL-RM,CASL-UM}.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederWe have implemented the \CASL logic in such a way that much of the
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederimplementation can be re-used for \CASL extensions as well; this
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederis achieved via ``holes'' (realized via polymorphic variables) in the
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedertypes for signatures, morphisms, abstract syntax etc. This eases
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederintegration of \CASL extensions and keeps the effort of integrating
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\CASL extensions quite moderate.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\item[CoCASL] \cite{MossakowskiEA04} is a coalgebraic extension of \CASL,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedersuited for the specification of process types and reactive systems.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederThe central proof method is coinduction.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\item[ModalCASL] \cite{ModalCASL}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder is an extension of \CASL with multi-modalities and
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederterm modalities. It allows the specification of modal systems with
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederKripke's possible worlds semantics. It is also possible to express
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercertain forms of dynamic logic.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[HasCASL] is a higher order extension of \CASL allowing
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder polymorphic datatypes and functions. It is closely related to the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder programming language Haskell and allows program constructs being
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder embedded in the specification.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederthe language is summarized in \cite{HasCASL/Summary}, the semantics
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederin \cite{Schroder05b,Schroder-habil}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[Haskell] is a modern, pure and strongly typed functional
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder programming language. It simultaneously is the implementation
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder language of \Hets, such that in the future, \Hets might be applied
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe definitive reference for Haskell is \cite{PeytonJones03},
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[CspCASL] \cite{Roggenbach:2003:C-CN} is a combination of \CASL
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder with the process algebra CSP.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[ConstraintCASL] is an experimental logic for the specification
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederof qualitative constraint calculi.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[OWL DL] is the Web Ontology Language (OWL) recommended by the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder World Wide Web Consortium (W3C, \texttt{http://www.w3c.org}). It is
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder used for knowledge representation and the Semantic Web
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \cite{berners:2001:SWeb}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHets calls an external OWL DL parser
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder written in JAVA to obtain the abstract syntax for an OWL file and its
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder imports. The JAVA parser is also doing a first analysis classifying
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder the OWL ontology into the sublanguages OWL Full, OWL DL and OWL
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder Hets only supports the last two, more restricted variants.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder structuring of the OWL imports is displayed as Development Graph.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[CASL-DL] \cite{OWL-CASL-WADT2004}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederis an extension of a restriction of \CASL, realizing
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedera strongly typed variant of OWL DL in \CASL syntax.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \CASL with cardinality restrictions for the description of sorts and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder unary predicates. The restrictions are based on the equivalence
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder between \CASLDL, OWL~DL and \SHOIN. Compared to \CASL only unary
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder and binary predicates, predefined datatypes and concepts (subsorts
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder of the topsort Thing) are allowed. It is used to bring OWL DL and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \CASL closer together.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[Propositional] is classical propositional logic, which will
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederbe connected to SAT solvers in the near future.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[SoftFOL] \cite{LuettichEA06a} offers three automated theorem
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder proving systems (ATP) for first-order logic with equality: (1) SPASS
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \cite{WeidenbachEtAl02}; (2) Vampire \cite{RiazanovV02}; and (3)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder MathServ Broker\footnote{which chooses an appropriate ATP upon a
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder classification of the FOL problem} \cite{ZimmerAutexier06}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder These together comprise some of the most advanced theorem provers
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder for first-order logic.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover for higher-order
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\end{description}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederSoftFOL and \Isabelle are currently the only logics coming with a
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederprover. Proof support for the other logics can be obtained by using
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederlogic translations to a prover-supported logic.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederAn introduction to \CASL can be found in the \CASL User Manual
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\cite{CASL-UM}; the detailed language reference is given in
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederthe \CASL Reference Manual \cite{CASL/RefManual}. These documents
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederexplain both the \CASL logic and language of basic specifications as
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederwell as the logic-independent constructs for structured and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederarchitectural specifications. Corresponding documents explaining the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\HetCASL language constructs for \emph{heterogeneous} structured specifications
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederare forthcoming, until then, \cite{Mossakowski:2003:FHS} may serve as a short
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederintroduction. Moreover, the main heterogeneous constructs will be illustrated
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederin Sect.~\ref{sec:HetSpec} below.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\section{Logic translations supported
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\label{comorphisms}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe following list of logic translations (formalized as institution
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercomorphisms \cite{GoguenRosu02}) is currently supported by \Hets:
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{tabular}{|l|p{5cm}|}\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2CoCASL & inclusion \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2CspCASL & inclusion \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2HasCASL & inclusion \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2Modal & inclusion \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2PCFOL & coding of subsorting by injections, see Chap.\ III:3.1 of the CASL Reference Manual \cite{CASL/RefManual}\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2SubCFOL & coding of partial functions by error elements
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder(translation $(4a')$ of \cite{Mossakowski02}, but extended to subsorting) \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2TopSort & coding of subsorting by a top sort and unary
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederpredicates for the subsorts \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCFOL2IsabelleHOL & coding of \CASL to Isabelle
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder(translation $(7)$ of \cite{Mossakowski02}) \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCoCASL2CoPCFOL & coding of subsorting by injections, similar to CASL2PCFOL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCoCASL2CoSubCFOL & coding of partial functions by error supersorts, similar to CASL2SubCFOL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCoCFOL2IsabelleHOL & coding of \CoCASL to Isabelle, similar to CFOL2IsabelleHOL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%CoPCFOL2CoCFOL & coding of partial functions by error elements,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%similar to PCFOL2CFOL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%%CspCASL2IsabelleHOL & \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%%CspCASL2Modal & \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHasCASL2HasCASL & coding of \HasCASL axiomatic recursive definitions
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederas \HasCASL recursive program definitions \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHasCASL2Haskell & translation of \HasCASL recursive program definitions to Haskell \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHasCASL2IsabelleHOL & coding of HasCASL to Isabelle/HOL \cite{Groening05} \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHaskell2IsabelleHOL & coding of Haskell to Isabelle/HOL \cite{TorriniEtAl07} \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHaskell2IsabelleHOLCF & coding of Haskell to Isabelle/HOLCF \cite{TorriniEtAl07}\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederModal2CASL & the standard translation of modal logic
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederto first-order logic \cite{blackburn_p-etal:2001a} \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%PCFOL2CFOL & coding of partial functions by error elements
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%(translation $(4a')$ of \cite{Mossakowski02}) \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederPCoClTyConsHOL2IsabelleHOL & coding of \HasCASL to Isabelle/HOL\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederSuleCFOL2SoftFOL & coding of CASL to SoftFOL \cite{LuettichEA06a},
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedermapping types to soft types \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederSuleCFOL2SoftFOLIndcuction & dto., but with instances of induction
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederaxioms for all proof goals\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederProp2CASL & inclusion \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederProp2CNF & conversion of propositional formulas to conjunctive normal form\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\section{Getting started}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe latest \Hets version can be obtained from the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\Hets tools home page
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder Since \Hets is being
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederimproved constantly, it is recommended always to use the latest version.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\Hets currently is available for Linux, Solaris and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThere are three possibilities to install \Hets:
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{enumerate}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe Java-based \Hets installer. Download a \texttt{.jar} file and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederjava -jar \texttt{file.jar}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederNote that you need Sun Java 1.4.2 or later. On a Mac, you can just
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdouble-click on the \texttt{.jar} file.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe installer will lead you through the installation with
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedera graphical interface. It will download and install further
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersoftware (if not already installed on your computer):
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{tabular}{|l|l|l|}\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederuDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederTcl/Tk & graphics widget system & \url{http://www.scriptics.com/software/tcltk/} \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederSPASS & theorem prover & \texttt{http://spass.mpi-sb.mpg.de/}\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder(X)Emacs & editor (for Isabelle) & (must be installed manually)\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIf you do not have Sun Java, you can just download the hets binary.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederYou have to unpack it with \texttt{bunzip2} and then put it at
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersome place coverd by your \texttt{PATH}. You also have to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederinstall the above mentioned software and set
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederseveral environment variables, as explained on the installation page.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIf you want to compile \Hets from the sources, please follow the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederlink ``Hets: source code and information for developers''
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederon the \Hets web page, download the sources (as tarball or from
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedercvs), and follow the
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederinstructions in the \texttt{INSTALL} file.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\section{Analysis of Specifications}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederConsider the following \CASL
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\begin{BIGEXAMPLE}
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\I\SPEC \NAMEREF{Strict\_Partial\_Order} =
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\begin{ITEMS}[\PRED]
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\I\SORT \( Elem \)
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder% \COMMENTENDLINE{\PRED abbreviates predicate}
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\(\[ \FORALL x,y,z : Elem \\
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederNote that there may exist \(x, y\) such that\\
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederneither \(x < y\) nor \(y < x\).
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\end{BIGEXAMPLE}
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\Hets can be used for parsing and
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederchecking static well-formedness of specifications.
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder \index{parsing}%
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder \index{static!analysis}%
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \index{analysis, static}%
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederLet us assume that the example is in a file named
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\texttt{Order.casl} (actually, this file is provided
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederwith the \Hets distribution).
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederThen you can check the well-formedness of the
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederspecification by typing (into some shell):
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\Hets checks both the correctness of this specification
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder with respect to the \CASL syntax, as
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederwell as its correctness with respect to the static semantics (e.g.\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederwhether all identifiers have been declared before they are used,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederwhether operators are applied to arguments of the correct sorts,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederwhether the use of overloaded symbols is unambiguous, and so on).
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederThe following flags are available in this context:
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\begin{description}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing -- the static analysis
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\item[\texttt{-s}, \texttt{--just-structured}]
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederDo the parsing and the static analysis of (heterogeneous) structured
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederspecifications, but leave out the analysis of basic specifications.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederThis can be used to quickly produce a development graph
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedershowing the dependencies among the specifications (cf. Sect.~\ref{sec:DevGraph}).
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederUse \texttt{DIR} as the directory for specification libraries
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder(equivalently, you can set the variable \texttt{HETS\_LIB} before
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[\texttt{--casl-amalg=ANALYSIS}]
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder For the analysis of architectural specification (a quite advanced
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder amalgamability checking
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder algorithm for \CASL logic; it is a comma-separated list of zero or
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder more of the following options:
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \begin{description}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \item[\texttt{sharing}] perform sharing analysis for sorts,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder operations and predicates.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \item[\texttt{cell}] perform cell condition check; implies
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \texttt{sharing}. With this option on the subsort embeddings are
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \item[\texttt{colimit-thinness}] perform colimit thinness check;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder implies \texttt{sharing}. The colimit thinness check is less
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder complete and usually takes longer than the full cell condition
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder check (\texttt{cell} option), but may prove more efficient in case
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder of certain specifications.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \end{description}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder If \texttt{ANALYSIS} is empty then amalgamability analysis for
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \CASL is skipped.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder The default value for \texttt{--casl-amalg} is
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\end{description}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\section{Heterogeneous Specification} \label{sec:HetSpec}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\Hets accepts plain text input files with the following endings:\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{tabular}{|l|c|c|}\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederEnding & default logic & structuring language\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\texttt{.casl} & \CASL & \CASL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\texttt{.het} & \CASL & \CASL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\texttt{.hs} & Haskell/HasSLe & Haskell\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\texttt{.owl} & OWL DL, OWL Lite & OWL\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederAlthough the endings \texttt{.casl} and \texttt{.het} are
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederinterchangeable, the former should be used for libraries of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederhomogeneous \CASL specifications and the latter for \HetCASL libraries
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederof heterogeneous specifications (that use the \CASL structuring
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederconstructs). Within a \HetCASL library, the current logic can be changed e.g.\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederto \HasCASL in the following way:
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{verbatim}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe subsequent specifications are then parsed and analysed as
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\HasCASL specifications. Within such specifications,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederit is possible to use references to named \CASL specifications;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederthese are then automatically translated along the default
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederembedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder(There are also heterogeneous constructs
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederfor explicit translations between logics.)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederA \CspCASL specification consists of a \CASL specification
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederfor the data part and a \Csp process built over this data part.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederTherefore, \HetCASL provides a heterogeneous language construct
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\texttt{data} as follows:
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{verbatim}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder free type List[Elem] ::= nil | cons(Elem; List[Elem])
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder channel read, write : Elem
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder let Buf(l:List[Elem]) =
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder read?x -> Buf( cons(x,nil) )
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder [] if l=nil then STOP else write!last(l) -> Buf( rest(l) )
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHere, the construct \texttt{data List} refers to the \CASL specification
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\texttt{List}, which is implicitly embedded into \CspCASL.
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}.
(definition links in the sense of \cite[IV:4]{CASL/RefManual}).
links in the sense of \cite[IV:4]{CASL/RefManual}.
\item[Dashed links] correspond to local (definition or theorem) links in the sense of \cite[IV:4]{CASL/RefManual}.
The ``Hide/show names'' menu is a toggle:
Manual \cite{CASL/RefManual}. While support for local and global
\item[Taxonomy graphs] (Only available for some logics) Shows the subsort graph of the signature of the node.
in abstract syntax trees in ATerm format, while \texttt{ast.baf}
The default is \texttt{dg.taf}, which means that the development
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.
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}.
\item[\texttt{-l LOGIC}, \texttt{--logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
\cite{DBLP:conf/tacas/Aspinall00,url:ProofGeneral} in a separate Emacs
The \Isabelle theory file conforms to the Isabelle/Isar syntax
%\input{hets.tex}