UserGuide.tex revision 464c78620a182d2e8fbd125098045eae8788e2bd
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\documentclass{article}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage{alltt}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage{casl}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage{xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\usepackage{color}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\usepackage{url}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\usepackage{threeparttable,hhline}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\usepackage[pdfborder=0 0 0,bookmarks,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinipdfauthor={Till Mossakowski, Christian Maeder, Klaus Lüttich},
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinipdftitle={Hets User Guide}]
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini{hyperref} %% do not load more packages after this line!!
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\newcommand{\QUERY}[1]%{}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\eat}[1]{}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\newcommand{\IEXT}[1] {\\#1\I}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\newcommand{\IEND} {\I\END}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\newenvironment{EXAMPLEFORMAT} {}{}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini%% Added by MB to have some extra vertical space after the ``main'' examples
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini%% following the points (and some others in the text):
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newenvironment{BIGEXAMPLE} {\begin{EXAMPLE}} {\end{EXAMPLE}\medskip}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\newenvironment{DETAILSFORMAT} {}{}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\newenvironment{META}[1][] {#1\begin{METAFORMAT}}{\end{METAFORMAT}}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\newenvironment{METAFORMAT} {\medskip\vrule\hspace{1ex}\vrule\hspace{1ex}%
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini \begin{minipage}{0.9\textwidth}\it}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini {\end{minipage}\par\medskip}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\SLIDESMALL} {}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\SLIDESONLY}[1] {}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini% SIMULATING SMALL-CAPS FOR BOLD, EMPH
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini%\newcommand {\CoFI}{CoFI\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\largeELAN} {\largeTEXTSC{E}{LAN}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand {\HOL}{\normalTEXTSC{H}{OL}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand {\Isabelle}{\normalTEXTSC{I}{SABELLE}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand {\SPASS}{\normalTEXTSC{S}{PASS}\xspace}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%%%%% Klaus macros
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini%%%%% end of Klaus macros
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\LCF}{LCF\xspace}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\newcommand{\ASF}{ASF\xspace}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\SDF}{SDF\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini%% Do NOT use \ASF+\SDF (it gives a superfluous space in the middle)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\newcommand{\CCC}{CCC\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\CoCASL}{\normalTEXTSC{C}{O}\normalTEXTSC{C}{ASL}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\CspCASL}{\normalTEXTSC{C}{SP}-\normalTEXTSC{C}{ASL}\xspace}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{document}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\title{{\bf \protect{\LARGEHets} User Guide}\\
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini-- Version 0.85 --}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\author{Till Mossakowski, Christian Maeder, Klaus L\"{u}ttich\\[1em]
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo TorriniDFKI Lab Bremen, Bremen, Germany.\\[1em]
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo TorriniComments to: hets-users@informatik.uni-bremen.de \\
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini(the latter needs subscription to the mailing list)
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\section{Introduction}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo TorriniThe Heterogeneous Tool Set (\protect\Hets) is the main analysis tool
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrinifor the specification language heterogeneous \CASL. Heterogeneous
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\CASL (\HetCASL) combines the specification language \CASL
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\cite{CASL-UM,CASL/RefManual} with \CASL extensions
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torriniand sublanguages, as well as completely different logics and even
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torriniprogramming languages such as Haskell. \HetCASL
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini(see Fig.~\ref{fig:lang} for a simple subset)
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torriniextends the structuring mechanisms of \CASL:
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\emph{Basic specifications} are
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torriniunstructured specifications or modules written in a specific logic.
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo TorriniThe graph of currently supported logics and logic translations (the
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrinilatter are also called comorphisms) is shown in
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo TorriniFig.~\ref{fig:LogicGraph}, and the degree of support by \Hets in
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo TorriniFig.~\ref{fig:Languages}.
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\begin{figure}[ht]
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\begin{verbatim}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo TorriniSPEC ::= BASIC-SPEC
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini | SPEC then SPEC
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini | SPEC then %implies SPEC
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini | SPEC with SYMBOL-MAP
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini | SPEC with logic ID
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniDEFINITION ::= logic ID
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini | spec ID = SPEC end
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini | view ID : SPEC to SPEC = SYMBOL-MAP end
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini | view ID : SPEC to SPEC = with logic ID end
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo TorriniLIBRARY = DEFINITION*
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\end{verbatim}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\caption{Syntax of a simple subset of the heterogeneous
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrinispecification language.
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\texttt{BASIC-SPEC} and \texttt{SYMBOL-MAP} have a logic
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrinispecific syntax, while \texttt{ID} stands for some form of
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torriniidentifiers.\label{fig:lang}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo TorriniWith \emph{heterogeneous structured specifications}, it is possible to
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrinicombine and rename specifications, hide parts thereof, and also
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrinitranslate them to other logics. \emph{Architectural specifications}
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torriniprescribe the structure of implementations. \emph{Specification
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini libraries} are collections of named structured and architectural
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrinispecifications.
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\Hets consists of logic-specific tools for the parsing and static
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrinianalysis of the different involved logics, as well as a
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrinilogic-independent parsing and static analysis tool for structured and
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torriniarchitectural specifications and libraries. The latter of course needs
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrinito call the logic-specific tools whenever a basic specification is
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\Hets is based on the theory of institutions \cite{GoguenBurstall92},
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torriniwhich formalize the notion of a logic. The theory behind \Hets is laid
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torriniout in \cite{Habil}. A short overview of \Hets is given in
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\cite{MossakowskiEA06,MossakowskiEtAl07b}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Logics supported by Hets}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe following list of logics (formalized as so-called institutions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{GoguenBurstall92}) is currently supported by \Hets:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{figure}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \begin{center}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \includegraphics[scale=0.4]{LogicGraph}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\caption{Graph of logics currently supported by \Hets. The more an
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniellipse is filled with green, the more stable is the implementation of the logic. Blue indicates a prover-supported logic.}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\label{fig:LogicGraph}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{figure}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{center}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{tabular}{|l|c|c|c|}\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniLanguage & Parser & Static Analysis & Prover \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\CASL & x & x & - \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\CoCASL & x & x & - \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\ModalCASL & x & x & - \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\HasCASL & x & x & - \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell & x & x & -\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\CspCASL & (x) & - & - \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniConstraint\CASL & x & (x) & - \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%Structured specifications & x & x & (x) \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%Architectural specifications & x & x & -\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\CASLDL & x & - & - \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniOWL DL basic & x & (x) & - \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniOWL DL structure & x & (x) & - \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniPropositional & x & x & x \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniSoftFOL & - & - & x \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Isabelle & - & - & x \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\caption{Current degree of \Hets support for the different languages.\label{fig:Languages}}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[CASL] extends many sorted first-order logic with partial
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini functions and subsorting. It also provides induction sentences,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini expressing the (free) generation of datatypes.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%It is mainly designed and used for the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%specification of requirements for software systems. But it is also
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%used for the specification of \Dolce (Descriptive Ontology for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%Linguistic and Cognitive Engineering), an Upper Ontology for knowledge
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%representation. \cite{Gangemi:2002:SOD} Further it is now used to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%specify calculi for time and space.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFor more details on \CASL see \cite{CASL/RefManual,CASL-UM}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniWe have implemented the \CASL logic in such a way that much of the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniimplementation can be re-used for \CASL extensions as well; this
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniis achieved via ``holes'' (realized via polymorphic variables) in the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitypes for signatures, morphisms, abstract syntax etc. This eases
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniintegration of \CASL extensions and keeps the effort of integrating
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\CASL extensions quite moderate.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[CoCASL] \cite{MossakowskiEA04} is a coalgebraic extension of \CASL,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisuited for the specification of process types and reactive systems.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe central proof method is coinduction.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[ModalCASL] \cite{ModalCASL}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini is an extension of \CASL with multi-modalities and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniterm modalities. It allows the specification of modal systems with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniKripke's possible worlds semantics. It is also possible to express
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicertain forms of dynamic logic.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[HasCASL] is a higher order extension of \CASL allowing
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini polymorphic datatypes and functions. It is closely related to the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini programming language Haskell and allows program constructs being
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini embedded in the specification.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe language is summarized in \cite{HasCASL/Summary}, the semantics
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin \cite{Schroder05b,Schroder-habil}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Haskell] is a modern, pure and strongly typed functional
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini programming language. It simultaneously is the implementation
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini language of \Hets, such that in the future, \Hets might be applied
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe definitive reference for Haskell is \cite{PeytonJones03},
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[CspCASL] \cite{Roggenbach06} is a combination of \CASL
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini with the process algebra CSP.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[ConstraintCASL] is an experimental logic for the specification
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof qualitative constraint calculi.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[OWL DL] is the Web Ontology Language (OWL) recommended by the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini World Wide Web Consortium (W3C, \url{http://www.w3c.org}). It is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini used for knowledge representation and the Semantic Web
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \cite{berners:2001:SWeb}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHets calls an external OWL DL parser
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini written in JAVA to obtain the abstract syntax for an OWL file and its
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini imports. The JAVA parser is also doing a first analysis classifying
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini the OWL ontology into the sublanguages OWL Full, OWL DL and OWL
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini Hets only supports the last two, more restricted variants.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini structuring of the OWL imports is displayed as Development Graph.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[CASL-DL] \cite{OWL-CASL-WADT2004}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniis an extension of a restriction of \CASL, realizing
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinia strongly typed variant of OWL DL in \CASL syntax.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \CASL with cardinality restrictions for the description of sorts and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini unary predicates. The restrictions are based on the equivalence
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini between \CASLDL, OWL~DL and \SHOIN. Compared to \CASL only unary
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini and binary predicates, predefined datatypes and concepts (subsorts
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini of the topsort Thing) are allowed. It is used to bring OWL DL and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \CASL closer together.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Propositional] is classical propositional logic, with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe zChaff SAT solver \cite{Herbstritt03} connected to it.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[SoftFOL] \cite{LuettichEA06a} offers three automated theorem
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini proving (ATP) systems for first-order logic with equality: (1) \SPASS
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \cite{WeidenbachEtAl02}; (2) Vampire \cite{RiazanovV02}; and (3)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini MathServe Broker\footnote{which chooses an appropriate ATP upon a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini classification of the FOL problem} \cite{ZimmerAutexier06}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini These together comprise some of the most advanced theorem provers
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini for first-order logic.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini for higher-order logic.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniPropositional, SoftFOL and \Isabelle are currently the only logics
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicoming with a prover. Proof support for the other logics can be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniobtained by using logic translations to a prover-supported logic.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAn introduction to \CASL can be found in the \CASL User Manual
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{CASL-UM}; the detailed language reference is given in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe \CASL Reference Manual \cite{CASL/RefManual}. These documents
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniexplain both the \CASL logic and language of basic specifications as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwell as the logic-independent constructs for structured and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniarchitectural specifications. The corresponding document explaining the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\HetCASL language constructs for \emph{heterogeneous} structured specifications
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniis the \HetCASL language summary \cite{Mossakowski04}; a formal
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisemantics as well as a user manual with more examples are in preparation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniSome of \HetCASL's heterogeneous constructs will be illustrated
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin Sect.~\ref{sec:HetSpec} below.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Logic translations supported
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\label{comorphisms}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniLogic translations (formalized as institution comorphisms
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{GoguenRosu02}) translate from a given source logic to a given
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitarget logic. More precisely, one and the same logic translation
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimay have several source and target \emph{sub}logics: for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinieach source sublogic, the corresponding sublogic of the target
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilogic is indicated.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniA graph of the most important logics and sublogics, together with their
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicomorphisms, is shown in Fig.~\ref{fig:SublogicGraph}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{figure}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \begin{center}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \includegraphics[scale=0.4]{SublogicGraph}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\caption{Graph of most important sublogics currently supported by \Hets,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitogether with their comorphisms.}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\label{fig:SublogicGraph}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn more detail, the following list of logic translations is currently
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisupported by \Hets:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{tabular}{|l|p{5cm}|}\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniCASL2CoCASL & inclusion \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniCASL2CspCASL & inclusion \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniCASL2HasCASL & inclusion \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniCASL2Modal & inclusion \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniCASL2PCFOL & coding of subsorting by injections, see Chap.\ III:3.1 of the CASL Reference Manual \cite{CASL/RefManual}\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniCASL2SubCFOL & coding of partial functions by error elements
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(translation $(4a')$ of \cite{Mossakowski02}, but extended to subsorting) \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniCASL2TopSort & coding of subsorting by a top sort and unary
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipredicates for the subsorts \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniCFOL2IsabelleHOL & coding of \CASL to Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(translation $(7)$ of \cite{Mossakowski02}) \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniCoCASL2CoPCFOL & coding of subsorting by injections, similar to CASL2PCFOL \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniCoCASL2CoSubCFOL & coding of partial functions by error supersorts, similar to CASL2SubCFOL \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniCoCFOL2IsabelleHOL & coding of \CoCASL to Isabelle, similar to CFOL2IsabelleHOL \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%CoPCFOL2CoCFOL & coding of partial functions by error elements,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%similar to PCFOL2CFOL \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%%CspCASL2IsabelleHOL & \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%%CspCASL2Modal & \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHasCASL2HasCASL & coding of \HasCASL axiomatic recursive definitions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinias \HasCASL recursive program definitions \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHasCASL2Haskell & translation of \HasCASL recursive program definitions to Haskell \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHasCASL2IsabelleHOL & coding of HasCASL to Isabelle/HOL \cite{Groening05} \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell2IsabelleHOL & coding of Haskell to Isabelle/HOL \cite{TorriniEtAl07} \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell2IsabelleHOLCF & coding of Haskell to Isabelle/HOLCF \cite{TorriniEtAl07}\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniModal2CASL & the standard translation of modal logic
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito first-order logic \cite{blackburn_p-etal:2001a} \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%PCFOL2CFOL & coding of partial functions by error elements
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%(translation $(4a')$ of \cite{Mossakowski02}) \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniPCoClTyConsHOL2IsabelleHOL & coding of \HasCASL to Isabelle/HOL\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniSuleCFOL2SoftFOL & coding of CASL to SoftFOL \cite{LuettichEA06a},
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimapping types to soft types \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniSuleCFOL2SoftFOLIndcuction & dto., but with instances of induction
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaxioms for all proof goals\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniProp2CASL & inclusion \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniProp2CNF & conversion of propositional formulas to conjunctive normal form\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Getting started}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe latest \Hets version can be obtained from the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Hets tools home page
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini Since \Hets is being
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniimproved constantly, it is recommended always to use the latest version.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Hets currently is available for Linux, Solaris and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThere are three possibilities to install \Hets:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{enumerate}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe Java-based \Hets installer. Download a \texttt{.jar} file and
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrinijava -jar \texttt{file.jar}
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo TorriniNote that you need Sun Java 1.4.2 or later. On a Mac, you can just
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrinidouble-click on the \texttt{.jar} file.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe installer will lead you through the installation with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinia graphical interface. It will download and install further
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisoftware (if not already installed on your computer):
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{tabular}{|l|l|l|}\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniCASL-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniuDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniTcl/Tk & graphics widget system & \url{http://www.scriptics.com/software/tcltk/} \\\hline
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrini\SPASS & theorem prover & \url{http://spass.mpi-sb.mpg.de/}\\\hline
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrini\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(X)Emacs & editor (for Isabelle) & (must be installed manually)\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIf you do not have Sun Java, you can just download the hets binary.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniYou have to unpack it with \texttt{bunzip2} and then put it at
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisome place coverd by your \texttt{PATH}. You also have to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinstall the above mentioned software and set
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniseveral environment variables, as explained on the installation page.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIf you want to compile \Hets from the sources, please follow the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilink ``Hets: source code and information for developers''
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinion the \Hets web page, download the sources (as tarball or from
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisvn), and follow the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinstructions in the \texttt{INSTALL} file.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{enumerate}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Analysis of Specifications}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniConsider the following \CASL
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinispecification:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{BIGEXAMPLE}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\I\SPEC \NAME{Strict\_Partial\_Order} =
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{ITEMS}[\PRED]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\I\SORT \( Elem \)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% \COMMENTENDLINE{\PRED abbreviates predicate}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\(\[ \FORALL x,y,z : Elem \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{COMMENT}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniNote that there may exist \(x, y\) such that\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinineither \(x < y\) nor \(y < x\).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{BIGEXAMPLE}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Hets can be used for parsing and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinichecking static well-formedness of specifications.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \index{parsing}%
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \index{static!analysis}%
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \index{analysis, static}%
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniLet us assume that the example is in a file named
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\texttt{Order.casl} (actually, this file is provided
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwith the \Hets distribution).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThen you can check the well-formedness of the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinispecification by typing (into some shell):
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Hets checks both the correctness of this specification
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini with respect to the \CASL syntax, as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwell as its correctness with respect to the static semantics (e.g.\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwhether all identifiers have been declared before they are used,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwhether operators are applied to arguments of the correct sorts,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwhether the use of overloaded symbols is unambiguous, and so on).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe following flags are available in this context:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing -- the static analysis
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{-s}, \texttt{--just-structured}] Do the parsing and the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini static analysis of (heterogeneous) structured specifications, but
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini leave out the analysis of basic specifications. This can be used
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini for prototyping issues, namely to quickly produce a development graph
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini showing the dependencies among the specifications (cf.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini Sect.~\ref{sec:DevGraph}) even if the individual specifications are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini not correct yet.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniUse \texttt{DIR} as the directory for specification libraries
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(equivalently, you can set the variable \texttt{HETS\_LIB} before
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicalling \Hets).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{--casl-amalg=ANALYSIS}]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini For the analysis of architectural specification (a quite advanced
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini amalgamability checking
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini algorithm for \CASL logic; it is a comma-separated list of zero or
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini more of the following options:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \begin{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \item[\texttt{sharing}] perform sharing analysis for sorts,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini operations and predicates.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \item[\texttt{cell}] perform cell condition check; implies
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \texttt{sharing}. With this option on, the subsort embeddings are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \item[\texttt{colimit-thinness}] perform colimit thinness check;
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini implies \texttt{sharing}. The colimit thinness check is less
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini complete and usually takes longer than the full cell condition
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini check (\texttt{cell} option), but may prove more efficient in case
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini of certain specifications.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \end{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini If \texttt{ANALYSIS} is empty then amalgamability analysis for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \CASL is skipped.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini The default value for \texttt{--casl-amalg} is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \texttt{cell}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Heterogeneous Specification} \label{sec:HetSpec}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Hets accepts plain text input files with the following endings:\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{tabular}{|l|c|c|}\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniEnding & default logic & structuring language\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\texttt{.casl} & \CASL & \CASL \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\texttt{.het} & \CASL & \CASL \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\texttt{.hs} & Haskell & Haskell\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\texttt{.owl} & OWL DL, OWL Lite & OWL\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAlthough the endings \texttt{.casl} and \texttt{.het} are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinterchangeable, the former should be used for libraries of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihomogeneous \CASL specifications and the latter for \HetCASL libraries
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torriniof heterogeneous specifications (that use the \CASL structuring
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torriniconstructs). Within a \HetCASL library, the current logic can be changed e.g.\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito \HasCASL in the following way:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{verbatim}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{verbatim}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe subsequent specifications are then parsed and analysed as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\HasCASL specifications. Within such specifications,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniit is possible to use references to named \CASL specifications;
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithese are then automatically translated along the default
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniembedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(There are also heterogeneous constructs
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifor explicit translations between logics, see \cite{Mossakowski04}.)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniA \CspCASL specification consists of a \CASL specification
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifor the data part and a \Csp process built over this data part.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniTherefore, \HetCASL provides a heterogeneous language construct
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\texttt{data} as follows:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{verbatim}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilibrary Buffer
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini free type List[Elem] ::= nil | cons(Elem; List[Elem])
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini channel read, write : Elem
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini let Buf(l:List[Elem]) =
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini read?x -> Buf( cons(x,nil) )
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini [] if l=nil then STOP else write!last(l) -> Buf( rest(l) )
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{verbatim}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHere, the construct \texttt{data List} refers to the \CASL specification
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\texttt{List}, which is implicitly embedded into \CspCASL.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe ending \texttt{.hs} is available for directly reading in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHaskell programs % and HasSLe specifications,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand hence supports the Haskell module system.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe logic Haskell has to be chosen explicitly, and the \CASL structuring
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisyntax needs to be used:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{verbatim}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilibrary Factorial
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinispec Factorial =
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifac :: Int -> Int
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifac n = foldl (*) 1 [1..n]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{verbatim}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniNote that according to the Haskell syntax, Haskell function
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinideclarations and definitions need to start with the first column of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Development Graphs}\label{sec:DevGraph}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniDevelopment graphs are a simple kernel formalism for (heterogeneous)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinistructured theorem proving and proof management.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniA development graph consists of a set of nodes (corresponding to whole
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinistructured specifications or parts thereof), and a set of arrows
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicalled \emph{definition links}, indicating the dependency of each
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinvolved structured specification on its subparts. Each node is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniassociated with a signature and some set of local axioms. The axioms
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof other nodes are inherited via definition links. Definition links
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniare usually drawn as black solid arrows, denoting an import of another
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinispecification.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniComplementary to definition links, which \emph{define} the theories of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirelated nodes, \emph{theorem links} serve for \emph{postulating}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinirelations between different theories. Theorem links are the central
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidata structure to represent proof obligations arising in formal
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniTheorem links can be \emph{global} (drawn as solid arrows) or
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{local} (drawn as dashed arrows): a global theorem link
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipostulates that all axioms of the source node (including the inherited
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniones) hold in the target node, while a local theorem link only postulates
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithat the local axioms of the source node hold in the target node.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniBoth definition and theorem links can be \emph{homogeneous},
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinii.e. stay within the same logic, or \emph{heterogeneous}, i.e.\ %% such that
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe logic changes along the arrow. Technically, this is the case
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifor Grothendieck signature morphisms $(\rho,\sigma)$ where
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini$\rho\not=id$. This case is indicated with double arrows.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniTheorem links are initially displayed in red.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe \emph{proof
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini calculus} for development graphs
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{MossakowskiEtAl05,Habil} is given by rules
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithat allow for proving global theorem links by decomposing them
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinto simpler (local and global) ones. Theorem links that have been
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniproved with this calculus are drawn in green. Local theorem links can
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinibe proved by turning them into \emph{local proof goals}. The latter
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinican be discharged using a logic-specific calculus as given by an
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinientailment system for a specific institution. Open local
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniproof goals are indicated by marking the corresponding node in the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidevelopment graph as red; if all local implications are proved, the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininode is turned into green. This implementation ultimately is based
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinion a theorem \cite{Habil} stating soundness and relative completeness
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof the proof calculus for heterogeneous development graphs.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand in \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe following option lets \Hets show the development graph of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinia specification library:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window.\end{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniLet us extend the above library \texttt{Order.casl}. One use of the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilibrary might be to express the fact that the natural numbers form a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinistrict partial order as a view, as follows:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{BIGEXAMPLE}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{BIGEXAMPLE}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{EXAMPLE}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\I\SPEC \NAMEDEFN{Natural\_Order\_2} =
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\IEXT{\NAMEREF{Natural}} \THEN
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\I\PRED \( \_\_<\_\_ : Nat \* Nat\)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\(\[ \FORALL x,y:Nat \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \. 0 < suc(x) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \. \neg x < 0 \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \. suc(x) < suc(y) \IFF x < y
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{EXAMPLE}%[\SLIDESMALL]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\NAMEREF{Natural\_Order\_2} =
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\I{} \( Elem \MAPSTO Nat\)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAgain, these specifications can be checked with \Hets. However, this
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinionly checks syntactic and static semantic well-formedness -- it is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniby a strict partial ordering relation. Checking this requires theorem
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniproving, which will be discussed below.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHowever, before coming to theorem proving, let us first inspect the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniproof obligations arising from a specification. This can be done with:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\texttt{hets -g Order.casl}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(assuming that the above two specifications and the view
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihave been added to the file
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Hets now displays a so-called development graph
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(which is just an overview graph showing the overall structure
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof the specifications in the library), see Fig.~\ref{fig:dg0}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{figure}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{center}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\includegraphics[scale=0.7]{dg-order-0}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\caption{Sample development graph.\label{fig:dg0}}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniNodes in a development graph correspond to \CASL specifications.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniArrows show how specifications are related by the structuring
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe black arrow denotes an ordinary import of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinispecifications (generated by the extension), while the red arrow
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidenotes a proof obligation (corresponding to the view).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThis proof obligation needs to be discharged in order to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinishow that the view is well-formed (then its color turns into green).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAs a more complex example, consider the following loose specification
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof a sorting function, taken from the \CASL User Manual
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{CASL-UM}, Chap.~6:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{BIGEXAMPLE}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\I\SPEC \NAMEREF{List\_Order\_Sorted}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{ITEMS}[\WITHIN]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{ITEMS}[\PRED]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\I\PRED \( \_\_is\_sorted : List \)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\(\[ \FORALL e,e': Elem; L : List \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \. empty~is\_sorted \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \. cons(e,empty)~is\_sorted \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \. cons(e,cons(e',L))~is\_sorted \IFF
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{ITEMS}[\OP]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\I\OP \( order : List \TOTAL List \)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{BIGEXAMPLE}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe following specification of sorting by insertion also is taken from
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe \CASL User Manual \cite{CASL-UM}, Chap.~6:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{BIGEXAMPLE}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\I\SPEC \NAMEREF{List\_Order}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\phantomsection
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{ITEMS}[\WITHIN]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{ITEMS}[\OP]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\I\OP \( insert : Elem \* List \TOTAL List \)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\(\[ \FORALL e,e':Elem; L:List \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \. insert(e, empty) = cons(e, empty) \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \. insert(e, cons(e',L)) = \[ cons(e', insert(e,L)) \WHEN e' < e\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \ELSE cons(e, cons(e',L)) \] \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{ITEMS}[\OP]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\I\OP \( order : List \TOTAL List \)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\(\[ \FORALL e:Elem; L:List \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \. order(empty) = empty \\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \. order(cons(e,L)) = insert(e, order(L)) \]\)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{BIGEXAMPLE}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniBoth specifications are related. To see this, we first inspect
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitheir signatures. This is possible with:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\texttt{hets -g Sorting.casl}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniassuming that \texttt{Sorting.casl} contains the above specifications.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{figure}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{center}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\includegraphics[scale=0.7]{dg-order-1}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\caption{Development graph for the two sorting specifications.\label{fig:dg1}}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn the above-mentioned development graph, we have two types of nodes.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe named ones correspond to named specifications, but there
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniare also unnamed nodes corresponding to anonymous basic
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinispecifications like the declaration of the $insert$ operation in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\NAMEREF{List\_Order} above. Basically, there is an
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniunnamed node for each structured specification that is not named.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAgain, the black arrows denote an ordinary import of specifications
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(corresponding to the extensions and unions in the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinispecifications), while the blue arrows denote hiding (corresponding to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe local specification).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniBy clicking on the nodes, one can inspect their signatures.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn this way, we can see that both \NAMEREF{List\_Order\_Sorted} and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\NAMEREF{List\_Order} have the same signature. Hence, it
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniis legal to add a view:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{EXAMPLE}%[\SLIDESMALL]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\I\VIEW \NAMEDEFN{v2}[\NAMEREF{Total\_Order}] ~:~ \NAMEREF{List\_Order\_Sorted}[\NAMEREF{Total\_Order}] \TO
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\NAMEREF{List\_Order}[\NAMEREF{Total\_Order}]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniWe have already added this view to \texttt{Sorting.casl}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe corresponding
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniproof obligation between \NAMEREF{List\_Order\_Sorted} and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\NAMEREF{List\_Order} is displayed in Fig.~\ref{fig:dg1}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini as a red arrow.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHere is a summary of the types of nodes and links occurring in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidevelopment graphs:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Named nodes] correspond to a named specification.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Unnamed nodes] correspond to an anonymous specification.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Elliptic nodes] correspond to a specification in the current library.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Rectangular nodes] are external nodes corresponding
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini to a specification downloaded from
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinianother library.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Red nodes] have open proof obligations.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Green nodes] have all proof obligations resolved.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Black links] correspond to reference to other specifications
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(definition links in the sense of \cite[IV:4]{CASL/RefManual}).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Blue links] correspond to hiding (hiding definition links).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Red links] correspond to open proof obligations (theorem links).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Green links] correspond to proved proof obligations (theorem links).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Yellow links] correspond to open proof obligations involving hiding (hiding theorem links).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Solid links] correspond to global (definition or theorem)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilinks in the sense of \cite[IV:4]{CASL/RefManual}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Dashed links] correspond to local (definition or theorem) links in the sense of \cite[IV:4]{CASL/RefManual}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Single links] have homogeneous signature morphisms (staying within
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinione and the same logic).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Double links] have heterogeneous signature morphisms (moving between
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniWe now explain the menus of the development graph window.
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo TorriniMost of the pull-down menus of the window are uDraw(Graph)-specific
12138d113e5e25fc91b7e8ba0a179a3da00b9a91Paolo Torrinitheir function can be looked up in the uDraw(Graph) documentation\footnote{see
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\url{http://www.informatik.uni-bremen.de/uDrawGraph/en/service/uDG31\_doc/}.}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe exception is the Edit menu. Moreover, the nodes and links
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof the graph have attached pop-up menus, which appear when
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniclicking with the right mouse button.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Edit] This menu has the following submenus:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[undo] Undo the last development graph proof step (see under Proofs)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[redo] Restore the last undone development graph proof step (see
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini under Proofs)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[reload] Reload the specification library (Attention! all proofs are lost. A change management keep proofs is in preparation.)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Unnamed nodes]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe ``Hide/show names'' menu is a toggle:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniyou can switch on or off the display of names for nodes that
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniare initially unnamed. The newly named nodes get names that
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniare derived from named neighbour nodes.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniWith the ``Hide nodes'' submenu, it is possible
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito reduce the complexity of the graph by hiding all unnamed nodes;
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinionly nodes corresponding to named specifications remain displayed.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniPaths between named nodes going through unnamed nodes
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniare displayed as links. With the ``Show nodes'' submenu, the unnamed
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininodes re-appear.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Proofs] This menu allows to apply some of the deduction rules
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini for development graphs, see Sect. IV:4.4 of the \CASL Reference
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini Manual \cite{CASL/RefManual} or one of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}. While support for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini local and global (definition or theorem) links is stable, support
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini for hiding links and checking conservativity is still experimental.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini In most cases, it is advisable to use ``Automatic'', which
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini automatically applies the rules in the correct order. As a result,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini the the open theorem links (marked in red) will be reduced to local
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini proof goals, that is, they become green, and instead, some of the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini node will get red, indicating open local proof goals.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini Besides the deduction rules, the menu contains entries for computing
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini a colimit approximation for the development graph and for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini computing normal forms of all nodes (needed when dealing with hiding).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Translate Graph] translates the whole development graph
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinialong a logic comorphism.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Show Logic Graph] shows the graph of logics and logic comorphisms
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicurrently supported by \Hets.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Show Library Graph] shows the graph of libraries that have
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinibeen loaded into \Hets, and their dependencies. For library,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe corresponding development graphs can be shown using its node menu.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAlso, a list of specifications and views can be shown.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Pop-up menu for nodes]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHere, the number of submenus depends on the type of the node:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Show signature] Shows the signature of the node.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Show local axioms] Shows the local axioms of the node.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Show theory] Shows the theory of the node (including axioms
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniimported from other nodes). Warning: axioms imported via hiding links
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniare not part of the theory; they can be made visible only by re-adding
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe hidden symbols, using the proof rule \emph{Theorem-Hide-Shift}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Translate theory] Translates the theory of a node to another logic.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniA menu with the possible translation paths will be displayed.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Taxonomy graphs] (Only available for some logics) Shows the subsort graph of the signature of the node.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Show sublogic] Shows the logic and, within that logic, the minimal sublogic
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifor the signature and the axioms of the node.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Show origin] Shows the kind of \CASL structuring construct that
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniled to the node.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Show proof status] Show open and proven local proof goals.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Prove] Try to prove the local proof goals. See Section~\ref{sec:Proofs}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Check consistency] Check the consistency of the theory of the node.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Show just subtree] (Only for named nodes) Reduce the complexity
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof the graph by just showing the subtree below the current node.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Undo show just subtree] (Only for named nodes) Undo the reduction.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Show referenced library] (Only for external nodes) Open a new window
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinishowing the development graph for the library the external node refers to.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%\item[Show spec] Show the structured specification of the node.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% (not fully implemented yet)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Show number of node] Show the internal number of the node.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Pop-up menu for links]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAgain, the number of submenus depends on the type of the link:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Show morphism] Shows the signature morphism of the link. It consists
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof two components: a logic translation and a signature morphism in the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitarget logic of the logic translation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn the (most frequent) case
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof an intra-logic signature morphism, the logic translation component is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinijust the identity.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Show origin] Shows the kind of \CASL structuring construct that
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniled to the link.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Show proof status] (Only for theorem links) Show the proof status.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Check conservativity] (Experimental) Check whether the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitheory of the target node of the link
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniis a conservative extension of the theory of the source node.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Show ID of this edge] Shows the internal number of the edge.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThese numbers are also used in the proof status information for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Reading, Writing and Formatting}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Hets provides several options controlling the types of files
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithat are read and written.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{-i ITYPE}, \texttt{--input-type=ITYPE}] Specify
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\texttt{ITYPE} as the type of the input file. The default is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\texttt{het} (\HetCASL plain text). \texttt{ast} is for reading
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin abstract syntax trees in ATerm format, while \texttt{ast.baf}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinireads in the compressed ATerm format.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe possible input types are:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{verbatim}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini (casl|het|owl|hs|prf|omdoc|hpf|[tree.]gen_trm[.baf])
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{verbatim}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{-O DIR}, \texttt{--output-dir=DIR}]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniSpecify \texttt{DIR} as destination directory for output files.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{-o OTYPES}, \texttt{--output-types=OTYPES}]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\texttt{OTYPES} is a comma separated list of output types:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{verbatim}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini | (sig|th)[.delta]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini | pp.(het|tex)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini | graph.(exp.dot|dot)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{verbatim}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe default is \texttt{prf} (a synonym for \texttt{dg.taf}), which
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimeans that the development graph of the library is stored in textual
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniATerm format (\texttt{taf}). This format can be read in when a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilibrary is downloaded from another library, avoiding the need to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinire-analyse the downloaded library. You can also directly read in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe \texttt{prf} format (both from the command line, by calling
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Hets on the \texttt{prf} file, and from the GUI, using the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFile-Open menu.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe \texttt{env} format is currently not used.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe \texttt{omdoc} format \cite{books/sp/Kohlhase06} is an XML-based
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimarkup format and data model for Open Mathematical Documents. It
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniserves as semantics-oriented representation format and ontology
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilanguage for mathematical knowledge. Currently, \CASL specifications
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinican be output in this format; support for further logics is planned.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe \texttt{hs} format is used for Haskell modules. Executable \CASL or
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\HasCASL specifications can be translated to Haskell.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniWhen the \texttt{thy} format is selected, \Hets will try to translate
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinieach specification in the library to \Isabelle, and write one \Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\texttt{.thy} file per specification.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniWhen the \texttt{comptable.xml} format is selected, \Hets will extract
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe composition and inverse table of a Tarskian relation algebra from
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinispecification(s) (selected with the \texttt{-n} or \texttt{--spec}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinioption). It is assumed that the relation algebra is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinigenerated by basic relations, and that the specification is written
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin the \CASL logic. A sample specification of a relation
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinialgebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniavailable from \texttt{www.cofi.info/Libraries}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe output format is XML, the URL of the DTD is included in the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe \texttt{pp} format is for pretty printing, either as plain text
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(\texttt{het}), \LaTeX input (\texttt{tex}) or HTML (\texttt{html}).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniA formatter with pretty-printed output currently is available only for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe \CASL logic. For example, it is possible to generate a pretty
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniprinted \LaTeX\ version of \texttt{Order.casl} by typing:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThis will generate a file \texttt{Order.pp.tex}. It can be included
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinto \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicoming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty}) is used.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe \texttt{dfg} format is used by the \SPASS theorem prover
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{WeidenbachEtAl02}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe \texttt{tptp} format (\url{http://www.tptp.org}) is a standard
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniformat for first-order theorem provers.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{-t TRANS}, \texttt{--translation=TRANS}]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinichooses a translation option. \texttt{TRANS} is a colon-separated list
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwithout blanks of one or more comorphism names (see Sect.~\ref{comorphisms}).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{-R}, \texttt{--recursive}] output also imported libraries.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe other output formats are for future usage.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Miscellaneous Options}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{-v[Int]}, \texttt{--verbose[=Int]}]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniSet the verbosity level according to \texttt{Int}. Default is 1.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{-q}, \texttt{--quiet}]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniBe quiet -- no diagnostic output at all. Overrides -v.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{-V}, \texttt{--version}] Print version number and exit.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{-h}, \texttt{--help}, \texttt{--usage}]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniPrint usage information and exit.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{+RTS -KIntM -RTS}] Increase the stack size to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \texttt{Int} megabytes (needed in case of a stack overflow).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThis must be the first option.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{-l LOGIC}, \texttt{--logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinideclaration. The default is \CASL.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{-n SPECS}, \texttt{--spec=SPECS}]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinichooses a list of named specifications for processing
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{-m FILE}, \texttt{--modelSparQ=FILE}] model check a qualitative calculus given in SparQ lisp notation \cite{SparQ06} against a \CASL specification
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[\texttt{-I}, \texttt{--interactive}] run \Hets in interactive mode
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Proofs with \Hets}\label{sec:Proofs}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe proof calculus for development graphs (Sect.~\ref{sec:DevGraph})
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinireduces global theorem links to local proof goals. Local proof goals
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(indicated by red nodes in the development graph) can be eventually
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidischarged using a theorem prover, using the ``Prove'' menu of a red node.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe graphical user interface (GUI) for calling a prover is shown in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFig. \ref{fig:proof_window} --- we call it ``Proof Management GUI''.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe list on the left shows all goal names prefixed with the proof
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinistatus in square brackets. A proved goal is indicated by a `+', a `-'
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniindicates a disproved goal, a space denotes an open goal, and a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini`$\times$' denotes an inconsistent specification (aka a fallen `+';
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisee below for details).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{figure}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\includegraphics[width=\textwidth]{proofmanagement1}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\caption{Hets Goal and Prover Interface\label{fig:proof_window}}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIf you open this GUI when processing the goals of one node for the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifirst time, it will show all goals as open. Within this list you can
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniselect those goals that should be inspected or proved. The button
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini`Display' shows the selected goals in the ASCII syntax of this
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitheory's logic in a separate window. With the `Prove' button the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniactual prover is launched. This is described in more detail in the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniparagraphs below. By pressing the `Show Proof Details' button a window
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniis opened where for each proved goal the used axioms, its proof
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniscript, and its proof are shown --- the level of detail depends on the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniused theorem prover. The `Status:' shows either `No prover running' or
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini`Waiting for prover' in black or blue. If you press the `Close' button
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe window is closed and the status of the goals' list is integrated
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinto the development graph. If all goals have been proved, the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniselected node turns from red into green.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe list `Pick Theorem Prover:' lets you choose one of the connected
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniprovers (currently, these are \Isabelle, MathServe Broker, \SPASS,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniVampire, and zChaff, described below). By pressing `Prove' the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniselected prover is launched and the theory along with the selected
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinigoals is translated via the shortest possible path of comorphisms into
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe provers logic. The button `More fine grained selection...' lets
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniyou pick a (composed) comorphism in a separate window from where the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniprover is launched then.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniSince the amount and kind of sentences sent to an ATP system is a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimajor factor for the performance of the ATP system, it is possible to
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniselect the axioms and proven theorems that will comprise the theory
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof the next proof attempt. Based on this selection the sublogic may
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinivary and also the available provers and comorphisms to provers. Former
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitheorems that are imported from other specifications are marked with
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe prefix `(Th)'. Since former theorems do not add additional logical
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicontent, they may be safely removed from the theory.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection[Automated Theorem Proving Systems]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini{Automated Theorem Proving Systems\\(Logic SoftFOL)}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\label{sec:ATP}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{figure}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\includegraphics[width=\textwidth]{spassGUI1}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\caption{Interface of the \SPASS prover\label{fig:SPASS_GUI}}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAll ATPs integrated into \Hets share the same GUI, with only a slight
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimodification for the MathServe Broker: it does not have input
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifields for extra options. Figure~\ref{fig:SPASS_GUI} shows the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinstantiation for \SPASS, where in the lower part of the window the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinibatch mode can be controlled. The upper part shows on the left the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilist of goals (with the same status indicators as in the Proof
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniManagement GUI), and on the right a proof attempt of the selected goal
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniis controlled and the result of the last proof attempt is displayed.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe status line indicates `Open', `Running', `Proved', `Disproved',
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini`Open (Time is up!)', and `Proved (Theory inconsistent!)'. The list of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniused axioms is actually only filled by \SPASS. The help button displays
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinformation about the extra options accepted by the ATP system. The
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinibutton `Show Details' shows the whole output of the ATP system. `Save
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniProver Configuration' allows you to save the configuration and status
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof each proof for documentation. By pressing the button `Exit Prover'
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe status of these proofs and goals is transferred back to the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniProof Management GUI.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe MathServe system \cite{ZimmerAutexier06} developed by J\"{u}rgen
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniZimmer provides a unified interface to a range of different ATP
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisystems; the most important systems are listed in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniTable~\ref{tab:MathServe}, along with their capabilities. These
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicapabilities are derived from the \emph{Specialist Problem Classes}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(SPCs) defined upon the basis of logical, language and syntactical
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniproperties by Sutcliffe and Suttner \cite{SutcliffeEA:2001:EvalATP}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniOnly two of the Web services provided by the MathServe system are used
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniby \Hets currently: Vampire and the brokering system. The ATP systems
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniare offered as Web Services using standardized protocols and formats
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisuch as SOAP, HTTP and XML. Currently, the ATP system Vampire may be
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniaccessed from \Hets via MathServe; the other systems are only reached
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniafter brokering.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{table}[t]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \begin{threeparttable}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \begin{tabular}{|l|c|p{7cm}|}\firsthline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini ATP System & Version & Suitable Problem Classes\tnote{a}\\
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \hhline{|=|=|=|}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini DCTP & 10.21p & effectively propositional \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini EP & 0.91 & effectively propositional; real first-order, no
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini equality; real first-order, equality\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini Otter & 3.3 & real first-order, no equality\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \SPASS & 2.2 & effectively propositional; real first-order, no
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini equality; real first-order, equality\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini Vampire & 8.0 & effectively propositional; pure equality, equality
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini clauses contain non-unit equality clauses; real first-order, no
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini equality, non-Horn\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini Waldmeister & 704 & pure equality, equality clauses are unit
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini equality clauses\\\lasthline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \end{tabular}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini %\renewcommand{\thempfootnote}{\arabic{mpfootnote}}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini %\footnotetext%[\value{footnote}\stepcounter{footnote}]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \begin{tablenotes}\footnotesize
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini {The list of problem classes for each ATP system is not
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini exhaustive, but only the most appropriate problem classes are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini named according to benchmark tests made with MathServe by
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini J\"urgen Zimmer.}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \end{tablenotes}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \end{threeparttable}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \caption{ATP systems provided as Web services by MathServe}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\vspace*{-4mm}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \label{tab:MathServe}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsubsection*{\SPASS}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe ATP system \SPASS \cite{WeidenbachEtAl02} is a resolution-based
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniprover for first-order logic with equality. Furthermore, it provides a soft
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinityping mechanism with subsorting that treats sorts as unary
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinipredicates. The ATP \SPASS should be installed locally and available
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithrough your \verb,$PATH, environment variable.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsubsection*{Vampire}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe ATP system Vampire is the winner of the last 5 CADE ATP System
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniCompetitions (CASC) (2002--2006) in the devisions \verb,FOF, and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\verb,CNF,. It is a resolution based ATP system supporting the calculi
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof ordered binary resolution and superposition for handling equality.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\url{http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifor detailed information. The connection to Vampire is achieved by
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniusing an Web service of the MathServe system.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsubsection*{MathServe Broker}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% The classes ``effectively propositional'' and ``real first-order''
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% apply to first-order problems that are distinguished by the finiteness
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% of the Herbrand universe; an effectively propositional problem has
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% only constants (generated by finitely many terms) whereas a real
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini% first-order problem contains true functions with an infinite Herbrand
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe brokering service chooses the most appropriate ATP system
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniupon a classification based on the SPCs, and on a training with the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilibrary Thousands of Problems for Theorem Provers (TPTP)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{ZimmerAutexier06}. The TPTP format
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihas been introduced by Sutcliffe and Suttner for the annual
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicompetition CASC \cite{Sutcliffe:2006:CASC} and provides a unified
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisyntax for untyped FOL with equality, but without any symbol
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{Isabelle}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Isabelle \cite{NipPauWen02} is an interactive theorem prover, which is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimore powerful than ATP systems, but also requires more user interaction.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihas a very small core guaranteeing correctness, and its provers,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilike the simplifier or the tableaux prover, are built on top of this
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicore. Furthermore, there is over fifteen years of experience with it,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand several mathematical textbooks have been partially
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \index{formal!verification}%
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Isabelle is a tactic based theorem prover implemented in standard ML.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe main \Isabelle logic (called Pure) is some weak intuitionistic type
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitheory with polymorphism. The logic Pure is used to represent a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinivariety of logics within \Isabelle; one of them being \HOL (higher-order
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilogic). For example, logical implication in Pure (written
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\texttt{==>}, also called meta-implication), is different from logical
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniimplication in \HOL (written \texttt{-->}, also called object
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIt is essential to be aware of the fact that the \Isabelle/\HOL logic
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniis different from the logics that are encoded into it via comorphisms.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniTherefore, the formulas appearing in subgoals of proofs with \Isabelle
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwill not conform to the syntax of the original input logic. They may
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinieven use features of \Isabelle/\HOL such as higher-order functions
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithat are not present in an input logic like \CASL.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Isabelle is started with ProofGeneral
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{DBLP:conf/tacas/Aspinall00,url:ProofGeneral} in a separate Emacs
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{url:Emacs,url:XEmacs}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe \Isabelle theory file conforms to the Isabelle/Isar syntax
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{NipPauWen02}. It starts with the theory (encoded along the selected
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini comorphism), followed by a list of theorems. Initially, all the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini theorems have trivial proofs, using the `oops` command. However, if
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini you have saved earlier proof attempts, \Hets will patch these into
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini the generated \Isabelle theory file, ensuring that your previous work
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini is not lost. (But note that this patching can only be successful
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini if you do not rename specifications, or change their structure.) You
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini now can replace the 'oops' commands with real \Isabelle proofs, and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini use Proof General to step through the proofs. You finish your session
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini by saving your file (using the Emacs file menu, or the Ctrl-x Ctrl-s
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini key sequence), and by exiting Emacs (Ctrl-x Ctrl-c).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\subsection{zChaff}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorrinizChaff is a solver for satisfiabily problems of boolean formulas
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(\normalTEXTSC{S}{AT})
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin CNF. It is connected as a prover for propositional logic to \Hets. The prover
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\SPASS is used to transform arbitrary boolean formulas to CNF. zChaff
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniimplements the \normalTEXTSC{C}{HAFF}\xspace algorithm. We are
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniusing the property, that a conjecture under the assumption of a set of axioms is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitrue, if the variables of axioms together with the negation of the conjecture
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinihave no satisfying assignment, to prove theorems with zChaff. That is why you see
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe result \normalTEXTSC{U}{NSAT}\xspace in the proof details, if a theorem has been proved
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito be true. zChaff uses the same ATP GUI as the provers for SoftFOL (ref. to section
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\ref{sec:ATP}). zChaff does not accept any options apart from the time-limit. The
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinicurrent integration of zChaff into \Hets has been tested with zChaff 2004.11.15.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Limits of Hets}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Hets is still intensively under development. In particular, the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifollowing points are still missing:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{itemize}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item There is no proof support for architectural specifications.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item Distributed libraries are always downloaded from the local disk,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininot from the Internet.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item Version numbers of libraries are not considered properly.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item The proof engine for development graphs provides only experimental
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisupport for hiding links and for conservativity.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Architecture of Hets}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe architecture of \Hets is shown in Fig.~\ref{fig:hets}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHow is a single logic implemented in the Heterogeneous Tool Set?
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThis is depicted in the left column of Fig.~\ref{fig:hets}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Hets provides an abstract interface for
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \index{institution!independence}%
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \index{independence, institution}%
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinstitutions, so
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithat new logics can be integrated smoothly.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn order to do so, a parser,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinia static checker and a prover for basic specifications in the logic have
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito be provided.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{figure}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{center}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{verbatim}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniclass Logic lid sign morphism sentence basic_spec symbol_map
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini | lid -> sign morphism sentence basic_spec symbol_map where
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini identity :: lid -> sign -> morphism
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini compose :: lid -> morphism -> morphism -> morphism
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini dom, codom :: lid -> morphism -> sign
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini parse_basic_spec :: lid -> String -> basic_spec
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini parse_symbol_map :: lid -> String -> symbol_map
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini parse_sentence :: lid -> String -> sentence
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini empty_signature :: lid -> sign
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini basic_analysis :: lid -> sign -> basic_spec -> (sign, [sentence])
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini stat_symbol_map :: lid -> sign -> symbol_map -> morphism
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini map_sentence :: lid -> morphism -> sentence -> sentence
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini lid -> [(sign, [sentence]) -> [sentence] -> Proof_status]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini cons_checkers :: lid -> [(sign, [sentence]) -> Proof_status]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniclass Comorphism cid
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini lid1 sign1 morphism1 sentence1 basic_spec1 symbol_map1
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini lid2 sign2 morphism2 sentence2 basic_spec2 symbol_map2
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini | cid -> lid1 lid2 where
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini sourceLogic :: cid -> lid1 targetLogic :: cid -> lid2
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini map_theory :: cid -> (sign1, [sentence1]) -> (sign2, [sentence2])
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini map_morphism :: cid -> morphism1 -> morphism2
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{verbatim}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\caption{The basic ingredients of logics and logic comorphisms}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\label{fig:logic:all}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniEach logic is realized in the programming language Haskell
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{PeytonJones03} by a set of types and functions, see
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFig.~\ref{fig:logic:all}, where we present a simplified, stripped down
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniversion, where e.g.\ error handling is ignored. For technical reasons
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinia logic is \emph{tagged} with a unique identifier type (\texttt{lid}),
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwhich is a singleton type the only purpose of which is to determine
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniall other type components of the given logic. In Haskell jargon, the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinterface is called a multiparameter type class with functional
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidependencies \cite{TypeClasses}. The Haskell interface for logic
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslations is realised similarly.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe logic-independent modules in \Hets can be found in the right half
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof Fig.~\ref{fig:hets}. These modules comprise roughly one third of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Hets' 100.000 lines of Haskell code.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe heterogeneous parser transforms a string
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniconforming to the syntax in Fig.~\ref{fig:lang}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinito an abstract syntax tree, using the \texttt{Parsec} combinator parser
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{Parsec}. Logic and translation names are looked up in the logic
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinigraph --- this is necessary to be able to choose the correct parser
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifor basic specifications. Indeed, the parser has a state that carries
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe current logic, and which is updated if an explicit specification
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof the logic is given, or if a logic translation is encountered (in
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe latter case, the state is set to the target logic of the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitranslation). With this, it is possible to parse basic specifications
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniby just using the logic-specific parser of the current logic as
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniobtained from the state.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe static analysis is based on the static analysis of basic
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinispecifications, and transforms an abstract syntax tree to a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidevelopment graph (cf.\ Sect.~\ref{sec:DevGraph} above). Starting with a
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininode corresponding to the empty theory, it successively extends (using
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe static analysis of basic specifications) and/or translates (along
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe intra- and inter-logic translations) the theory, while
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisimultaneously adding nodes and links to the development graph.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHeterogeneous proof management is done using heterogeneous
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinidevelopment graphs, as described in Sect.~\ref{sec:DevGraph}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFor local proof goals, logic-specific provers are invoked,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinisee Sect.~\ref{sec:Proofs}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Hets can store development graphs, including their proofs.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniTherefore, \Hets uses the so-called
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \index{ATerms}%
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniATerm format \cite{BJKO00}, which is used as interchange format
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifor interfacing with other tools.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniMore details can be found in \cite{Habil,MossakowskiEtAl07b}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniand in the overview of modules provided in the developers section
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof the \Hets home page at \url{http://www.dfki.de/sks/hets}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{figure}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{center}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\includegraphics[scale=0.4]{hets2007}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\caption{Architecture of the heterogeneous tool set.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\label{fig:hets}}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Hets is mainly maintained by
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniChristian Maeder (Christian.Maeder@dfki.de) and Till Mossakowski
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(Till.Mossakowski@dfki.de). The mailing list is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \url{hets-users@informatik.uni-bremen.de}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe homepage is
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\url{http://www.informatik.uni-bremen.de/mailman/listinfo/hets-users}.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniYou need to subscribe to the list before you can send a mail.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniBut note that subscription is very easy!
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIf your favourite logic is missing in \Hets, please tell us
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini(hets-users@informatik.uni-bremen.de). We will take account your
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifeedback when deciding which logics and proof tools to integrate next
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniinto \Hets. Help with integration of more logics and proof tools into
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Hets is also welcome.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\paragraph{Acknowledgement}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe heterogeneous tool set \Hets would not have possible
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniwithout cooperation with many people.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%Christian Maeder and Klaus L\"uttich.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniBesides the authors, the following people have been involved
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniin the implementation of \Hets:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniKatja Abu-Dib,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniMihai Codescu,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniCarsten Fischer,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniJorina Freya Gerken,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniRainer Grabbe,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniSonja Gr\"{o}ning,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniDaniel Hausmann,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniWiebke Herding,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniCui ``Ken'' Jian,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAnton Kirilov,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniTina Krausser,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniMartin K\"{u}hl,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniDominik L\"{u}cke,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%Klaus L\"{u}ttich,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%Christian Maeder,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniMaciek Makowski,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniImmanuel Normann,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniRazvan Pascanu,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniDaniel Pratsch,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFelix Reckers,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniMarkus Roggenbach,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniPascal Schmidt,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniPaolo Torrini,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniRen\'{e} Wagner,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniJian Chun Wang and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThiemo Wiedemeyer.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Hets has been built based on experiences with its
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \index{Cats@\Cats}%
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \index{Maya@\MAYA}%
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe \CASL Tool Set (\Cats)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\cite{Mossakowski:2000:CST,Mossakowski:1998:SSA}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniprovides parsing and static analysis for \CASL.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIt has been developed by the first author with help
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniof Mark van den Brand, Kolyang, Bartek Klin, Pascal Schmidt and
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniFrederic Voisin.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\MAYA \cite{Autexier:2002:IHD,AutexierEtal02} is a proof management
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitool based on development graphs. \MAYA only supports development
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinigraphs without hiding and without logic translations. \MAYA has been
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinideveloped by Serge Autexier and Dieter Hutter.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniWe also want to thank Agn\`es Arnould, Thibaud Brunet, Pascale LeGall,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniKathrin Hoffmann, Katiane Lopes,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini%Klaus L\"uttich, Christian Maeder,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniStefan Merz, Maria Martins Moreira, Christophe
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniRingeissen, Markus Roggenbach, Dmitri Schamschurko, Lutz Schr\"oder,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniKonstantin Tchekine and Stefan W\"olfl
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifor giving feedback about \Cats, HOL-CASL and \Hets. Finally,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinispecial thanks to Christoph L\"uth and George Russell
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifor help with connecting \Hets to their UniForM workbench.
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\bibliographystyle{plain}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\bibliography{cofibib,cofi-ann,UM,hets,kl}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\end{document}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini%%% Local Variables:
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini%%% mode: latex
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini%%% TeX-master: "UserGuide"