UserGuide.tex revision 6135dff41a8cf187b8821aab7def02f624f8e856
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\documentclass{article}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\usepackage[show]{ed} % set to hide for producing a released version
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\usepackage{alltt}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\usepackage{casl}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\usepackage{xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\usepackage{color}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\usepackage{url}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\usepackage{threeparttable,hhline}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\usepackage[pdfborder=0 0 0,bookmarks,
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannpdfauthor={Till Mossakowski, Christian Maeder, Mihai Codescu},
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannpdftitle={Hets User Guide}]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann{hyperref} %% do not load more packages after this line!!
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\QUERY}[1]%{}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\eat}[1]{}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\IEXT}[1] {\\#1\I}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\IEND} {\I\END}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newenvironment{EXAMPLEFORMAT} {}{}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%% Added by MB to have some extra vertical space after the ``main'' examples
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%% following the points (and some others in the text):
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newenvironment{BIGEXAMPLE} {\begin{EXAMPLE}} {\end{EXAMPLE}\medskip}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newenvironment{DETAILSFORMAT} {}{}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newenvironment{META}[1][] {#1\begin{METAFORMAT}}{\end{METAFORMAT}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newenvironment{METAFORMAT} {\medskip\vrule\hspace{1ex}\vrule\hspace{1ex}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \begin{minipage}{0.9\textwidth}\it}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann {\end{minipage}\par\medskip}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\SLIDESMALL} {}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\SLIDESONLY}[1] {}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% SIMULATING SMALL-CAPS FOR BOLD, EMPH
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%\newcommand {\CoFI}{CoFI\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\largeELAN} {\largeTEXTSC{E}{LAN}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand {\HOL}{\normalTEXTSC{H}{OL}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand {\Isabelle}{\normalTEXTSC{I}{SABELLE}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand {\SPASS}{\normalTEXTSC{S}{PASS}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%%%%% Klaus macros
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\SROIQ}{$\mathcal{SROIQ}$(\textbf{D})\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\DL}{DL\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%%%%% end of Klaus macros
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\LCF}{LCF\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\ASF}{ASF\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\SDF}{SDF\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%% Do NOT use \ASF+\SDF (it gives a superfluous space in the middle)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\CCC}{CCC\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\CoCASL}{\normalTEXTSC{C}{O}\normalTEXTSC{C}{ASL}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\CspCASL}{\normalTEXTSC{C}{SP}-\normalTEXTSC{C}{ASL}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{document}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\title{{\bf \protect{\LARGEHets} User Guide}\\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann-- Version 0.98 --}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\author{Till Mossakowski, Christian Maeder,
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Mihai Codescu\\[1em]
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannDFKI GmbH, Bremen, Germany.\\[1em]
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannComments to: hets-users@informatik.uni-bremen.de \\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann(the latter needs subscription to the mailing list)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\section{Introduction}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe central idea of the Heterogeneous Tool Set (\protect\Hets) is to
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannprovide a general framework for formal methods integration and proof
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannmanagement. One can think of \Hets acting like a motherboard where
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanndifferent expansion cards can be plugged in, the expansion cards here
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannbeing individual logics (with their analysis and proof tools) as well
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannas logic translations. Individual logics and their analysis and proof
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanntools can be plugged into the \Hets motherboard using an
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannobject-oriented interface based on institutions
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\cite{GoguenBurstall92}. The \Hets motherboard already has plugged in
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanna number of expansion cards (e.g., the theorem provers Isabelle, SPASS
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannand more, as well as model finders). Hence, a variety of tools is
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannavailable, without the need to hard-wire each tool to the logic at
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{figure}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{center}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \includegraphics[width=0.45\textwidth]{hets-motherboard}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\caption{The \Hets motherboard and some expansion cards}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\Hets supports a number of input languages directly, such as \CASL,
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCommon Logic, OWL-DL, Haskell, and Maude. For heterogeneous
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannspecification, \Hets offers the language heterogeneous \CASL.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannHeterogeneous \CASL (\HetCASL) generalises the structuring
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\CASL \cite{CASL-UM,CASL/RefManual} to arbitrary logics
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann(if they are formalised as institutions and plugged into
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannthe \Hets motherboard), as well as to heterogeneous
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanncombination of specification written in different logics.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannFig.~\ref{fig:lang} for a simple subset of the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\HetCASL syntax, where \emph{basic specifications} are unstructured
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannspecifications or modules written in a specific logic. The graph of
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanncurrently supported logics and logic translations (the latter are also
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanncalled comorphisms) is shown in Fig.~\ref{fig:LogicGraph}, and the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanndegree of support by \Hets in Fig.~\ref{fig:Languages}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{figure}[ht]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{verbatim}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannSPEC ::= BASIC-SPEC
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann | SPEC then SPEC
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann | SPEC then %implies SPEC
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann | SPEC with SYMBOL-MAP
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann | SPEC with logic ID
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannDEFINITION ::= logic ID
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann | spec ID = SPEC end
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann | view ID : SPEC to SPEC = SYMBOL-MAP end
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann | view ID : SPEC to SPEC = with logic ID end
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannLIBRARY = DEFINITION*
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\end{verbatim}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\caption{Syntax of a simple subset of the heterogeneous
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannspecification language.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\texttt{BASIC-SPEC} and \texttt{SYMBOL-MAP} have a logic
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannspecific syntax, while \texttt{ID} stands for some form of
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannidentifiers.\label{fig:lang}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannWith \emph{heterogeneous structured specifications}, it is possible to
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanncombine and rename specifications, hide parts thereof, and also
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanntranslate them to other logics. \emph{Architectural specifications}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannprescribe the structure of implementations. \emph{Specification
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann libraries} are collections of named structured and architectural
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannspecifications.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\Hets consists of logic-specific tools for the parsing and static
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannanalysis of the different involved logics, as well as a
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannlogic-independent parsing and static analysis tool for structured and
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannarchitectural specifications and libraries. The latter of course needs
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannto call the logic-specific tools whenever a basic specification is
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\Hets is based on the theory of institutions \cite{GoguenBurstall92},
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannwhich formalize the notion of a logic. The theory behind \Hets is laid
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannout in \cite{Habil}. A short overview of \Hets is given in
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\cite{MossakowskiEA06,MossakowskiEtAl07b}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\section{Logics supported by Hets}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe following list of logics (formalized as so-called institutions
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\cite{GoguenBurstall92}) is currently supported by \Hets:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{figure}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \begin{center}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \includegraphics[scale=0.4]{LogicGraph}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\caption{Graph of logics currently supported by \Hets. The more an
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannellipse is filled with green, the more stable is the implementation of the logic. Blue indicates a prover-supported logic.}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\label{fig:LogicGraph}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{figure}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{center}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{tabular}{|l|c|c|c|}\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannLanguage & Parser & Static Analysis & Prover \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\CASL & x & x & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\CoCASL & x & x & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\ModalCASL & x & x & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\HasCASL & x & x & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannHaskell & (x) & x & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCspCASL & x & x & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCspCASL\_Trace & - & - & x \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCspCASL\_Failure & - & - & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCommonLogic & x & x & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannConstraint\CASL & x & (x) & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannTemporal & x & (x) & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannRelScheme & x & (x) & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannDFOL & x & (x) & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannExtModal & x & (x) & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannLF & x & (x) & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%Structured specifications & x & x & (x) \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%Architectural specifications & x & x & -\\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\CASLDL & x & - & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannDMU & x & - & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannFreeCAD & - & - & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannOWL DL & x & x & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannPropositional & x & x & x \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannQBF & x & x & x \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannSoftFOL & x & - & x \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannMaude & x & x & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannVSE & x & x & x \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\Isabelle & (x) & - & x \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannHolLight & (x) & - & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannAdl & x & x & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannFpl & x & x & - \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannEnCL & x & x & x \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\caption{Current degree of \Hets support for the different languages.\label{fig:Languages}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{description}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[CASL] extends many sorted first-order logic with partial
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann functions and subsorting. It also provides induction sentences,
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann expressing the (free) generation of datatypes.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%It is mainly designed and used for the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%specification of requirements for software systems. But it is also
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%used for the specification of \Dolce (Descriptive Ontology for
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%Linguistic and Cognitive Engineering), an Upper Ontology for knowledge
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%representation. \cite{Gangemi:2002:SOD} Further it is now used to
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%specify calculi for time and space.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannFor more details on \CASL see \cite{CASL/RefManual,CASL-UM}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannWe have implemented the \CASL logic in such a way that much of the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimplementation can be re-used for \CASL extensions as well; this
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannis achieved via ``holes'' (realized via polymorphic variables) in the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanntypes for signatures, morphisms, abstract syntax etc. This eases
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannintegration of \CASL extensions and keeps the effort of integrating
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\CASL extensions quite moderate.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[CoCASL] \cite{MossakowskiEA04} is a coalgebraic extension of \CASL,
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannsuited for the specification of process types and reactive systems.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe central proof method is coinduction.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[ModalCASL] \cite{ModalCASL}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann is an extension of \CASL with multi-modalities and
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannterm modalities. It allows the specification of modal systems with
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannKripke's possible worlds semantics. It is also possible to express
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanncertain forms of dynamic logic.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[ExtModal] is an extended modal logic, currently in an experimental state.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[HasCASL] is a higher order extension of \CASL allowing
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann polymorphic datatypes and functions. It is closely related to the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann programming language Haskell and allows program constructs being
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann embedded in the specification.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannthe language is summarized in \cite{HasCASL/Summary}, the semantics
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannin \cite{Schroder05b,Schroder-habil}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Haskell] is a modern, pure and strongly typed functional
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann programming language. It simultaneously is the implementation
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann language of \Hets, such that in the future, \Hets might be applied
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe definitive reference for Haskell is \cite{PeytonJones03},
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[CspCASL] \cite{Roggenbach06} is a combination of \CASL
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann with the process algebra \Csp.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[CommonLogic] \url{http://en.wikipedia.org/wiki/Common_logic}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[ConstraintCASL] is an experimental logic for the specification
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannof qualitative constraint calculi.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[OWL DL] is the Web Ontology Language (OWL) recommended by the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann World Wide Web Consortium (W3C, \url{http://www.w3c.org}). It is
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann used for knowledge representation and the Semantic Web
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \cite{berners:2001:SWeb}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannHets calls an external OWL DL parser
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann written in JAVA to obtain the abstract syntax for an OWL file and its
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann imports. The JAVA parser is also doing a first analysis classifying
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann the OWL ontology into the sublanguages OWL Full, OWL DL and OWL
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Hets only supports the last two, more restricted variants.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann structuring of the OWL imports is displayed as Development Graph.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[CASL-DL] \cite{OWL-CASL-WADT2004}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannis an extension of a restriction of \CASL, realizing
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanna strongly typed variant of OWL DL in \CASL syntax.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \CASL with cardinality restrictions for the description of sorts and
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann unary predicates. The restrictions are based on the equivalence
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann between \CASLDL, OWL~DL and \SHOIN. Compared to \CASL only unary
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann and binary predicates, predefined datatypes and concepts (subsorts
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann of the topsort Thing) are allowed. It is used to bring OWL DL and
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \CASL closer together.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Propositional] is classical propositional logic, with
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannthe zChaff SAT solver \cite{Herbstritt03} connected to it.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[QBF] are quantified boolean formulas, with
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannDepQBF \url{http://fmv.jku.at/depqbf/} connected to it.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[RelScheme] is a logic for relational databases \cite{DBLP:journals/ao/SchorlemmerK08}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[SoftFOL] \cite{LuettichEA06a} offers three automated theorem
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann proving (ATP) systems for first-order logic with equality: (1) \SPASS
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \cite{WeidenbachEtAl02}; (2) Vampire \cite{RiazanovV02}; and (3)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann MathServe Broker\footnote{which chooses an appropriate ATP upon a
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann classification of the FOL problem} \cite{ZimmerAutexier06}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann These together comprise some of the most advanced theorem provers
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann for first-order logic.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann for higher-order logic.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[HolLight] \url{http://www.cl.cam.ac.uk/~jrh13/hol-light/}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann is John Harrison's interactive theorem prover
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann for higher-order logic.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[VSE] is an interactive theorem prover, see \ref{subsec:VSE}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[DMU] is a dummy logic to read output of ``Computer Aided
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Three-dimensional Interactive Application'' (Catia).
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[FreeCAD] is a logic to read design files of the CAD system
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann FreeCAD\\\url{http://sourceforge.net/projects/free-cad}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Maude] is a rewrite system \url{http://maude.cs.uiuc.edu/} for
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann first-order logic. In order to use this logic the environment variable
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \verb+HETS_MAUDE_LIB+ must be set to a directory containing the files
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \verb+full-maude.maude+, \verb+hets.prj+, \verb+maude2haskell.maude+ and
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[DFOL] is an extension of first-order logic with dependent types \cite{rabe:dfol:06}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item [LF] is the dependent type theory of Twelf \url{http://twelf.plparty.org/}. Hets
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann calls Twelf on \verb+.elf+ files (for this, the environment variable
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \verb+TWELF_LIB+ must be set) and reads in the OMDoc generated by Twelf.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Moreover, LF can be used as a logical framework to add new logics in Hets \cite{CHK+2011a}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Logic definitions in LF are based in the logic atlas of the Latin project \cite{project:latin}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann and therefore the environment variable \verb+LATIN_LIB+ must be set to the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann repository with the Latin logic definitions.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Framework] is a dummy logic added for declarative logic definitions \cite{CHK+2011a}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Adl] is ``A Description Language'' based on relational algebra originally
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann designed for requirements engineering of business rules
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \url{https://lab.cs.ru.nl/BusinessRules/Requirements_engineering}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Fpl] is a ``logic for functional programs'' as an extension of a
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann restriction of \CASL. (\CASL predicates are disabled.)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann A detailed description of FPL will appear elsewhere.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[EnCL] is an ``engineering calculation language'' based on first
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann order theory of real numbers with some predefined binders
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \cite{logic:EnCL}. It allows the formulation of executable
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann specifications of engineering calculation methods. For the execution
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann of these specifications Hets provides connections to the computer
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann algebra systems Mathematica, Maple and Reduce.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\end{description}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannVarious logics are supported with proof tools. Proof support for the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannother logics can be obtained by using logic translations to a
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannprover-supported logic.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannAn introduction to \CASL can be found in the \CASL User Manual
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\cite{CASL-UM}; the detailed language reference is given in
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannthe \CASL Reference Manual \cite{CASL/RefManual}. These documents
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannexplain both the \CASL logic and language of basic specifications as
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannwell as the logic-independent constructs for structured and
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannarchitectural specifications. The corresponding document explaining the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\HetCASL language constructs for \emph{heterogeneous} structured specifications
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannis the \HetCASL language summary \cite{Mossakowski04}; a formal
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannsemantics as well as a user manual with more examples are in preparation.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannSome of \HetCASL's heterogeneous constructs will be illustrated
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannin Sect.~\ref{sec:HetSpec} below.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\section{Logic translations supported
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\label{comorphisms}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannLogic translations (formalized as institution comorphisms
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\cite{GoguenRosu02}) translate from a given source logic to a given
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanntarget logic. More precisely, one and the same logic translation
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannmay have several source and target \emph{sub}logics: for
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanneach source sublogic, the corresponding sublogic of the target
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannlogic is indicated.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannA graph of the most important logics and sublogics, together with their
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanncomorphisms, is shown in Fig.~\ref{fig:SublogicGraph}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{figure}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \begin{center}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \includegraphics[scale=0.4]{SublogicGraph}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\caption{Graph of most important sublogics currently supported by \Hets,
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanntogether with their comorphisms.}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\label{fig:SublogicGraph}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannIn more detail, the following list of logic translations is currently
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannsupported by \Hets:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{tabular}{|l|p{8cm}|}\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannAdl2CASL & inclusion taking relations to CASL predicates \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCASL2CoCASL & inclusion \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCASL2CspCASL & inclusion \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCASL2HasCASL & inclusion \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCASL2Isabelle & inclusion on sublogic CFOL=
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann(translation $(7)$ of \cite{Mossakowski02}) \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCASL2Modal & inclusion \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCASL2PCFOL & coding of subsorting (SubPCFOL=) by injections, see Chap.\ III:3.1 of the CASL Reference Manual \cite{CASL/RefManual} \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCASL2PCFOLTopSort & coding of subsorting (SulPeCFOL=) by a top sort and unary
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannpredicates for the subsorts \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCASL2Propositional & translation of propositional FOL \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCASL2SoftFOL & coding of CASL.SuleCFOL=E to SoftFOL \cite{LuettichEA06a},
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannmapping types to soft types \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCASL2SoftFOLInduction & same as CASL2SoftFOL but with instances of induction
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannaxioms for all proof goals \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCASL2SoftFOLInduction2 & similar to CASL2SoftFOLInduction but replaces goals with induction premises \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCASL2SubCFOL & coding of partial functions by error elements
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann(translation $(4a')$ of \cite{Mossakowski02}, but extended to subsorting, i.e. sublogic SubPCFOL=) \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCASL2VSE & inclusion on sublogic CFOL= \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCASL2VSEImport & inclusion on sublogic CFOL= \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCASL2VSERefine & refining translation of CASL.CFOL= to VSE \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCASL\_DL2CASL & inclusion \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCoCASL2CoPCFOL & coding of subsorting by injections, similar to CASL2PCFOL \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCoCASL2CoSubCFOL & coding of partial functions by error supersorts, similar to CASL2SubCFOL \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCoCASL2Isabelle & extended translation similar to CASL2Isabelle \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCommonLogic2CASL & coding Common Logic to CASL \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCspCASL2CspCASL\_Failure & inclusion \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCspCASL2CspCASL\_Trace & inclusion \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCspCASL2Modal & translating the CASL data part to ModalCASL \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannDFOL2CASL & translating dependent types \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannDMU2OWL & interpreting Catia output as OWL \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{tabular}{|l|p{7cm}|}\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannHasCASL2HasCASLNoSubtypes & coding out subtypes \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannHasCASL2HasCASLPrograms & coding of \HasCASL axiomatic recursive definitions
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannas \HasCASL recursive program definitions \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannHasCASL2Haskell & translation of \HasCASL recursive program definitions to Haskell \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannHasCASL2IsabelleOption & coding of HasCASL to Isabelle/HOL \cite{Groening05} \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannHaskell2Isabelle & coding of Haskell to Isabelle/HOL \cite{TorriniEtAl07} \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannHaskell2IsabelleHOLCF & coding of Haskell to Isabelle/HOLCF \cite{TorriniEtAl07} \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannHolLight2Isabelle & coding of HolLight to Isabelle/HOL \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannMaude2CASL & encoding of rewrites as predicates \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannModal2CASL & the standard translation of modal logic
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannto first-order logic \cite{blackburn_p-etal:2001a} \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannOWL2CASL & inclusion \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannOWL2CommonLogic & inclusion \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannPropositional2CASL & inclusion \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannPropositional2QBF & inclusion \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannQBF2Propositional & inclusion \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannRelScheme2CASL & inclusion \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\section{Getting started}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe latest \Hets version can be obtained from the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\Hets tools home page
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Since \Hets is being
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimproved constantly, it is recommended always to use the latest version.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\Hets is currently available (on Intel architectures only) for Linux, Solaris
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThere are several possibilities to install \Hets.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{enumerate}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe best support is currently given via Ubuntu packages.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{verbatim}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannsudo apt-add-repository ppa:hets/hets
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannsudo apt-add-repository \
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann "deb http://archive.canonical.com/ubuntu lucid partner"
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannsudo apt-get update
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannsudo apt-get install hets
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\end{verbatim}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThis will also install quite a couple of tools for proving requiring about
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann800 MB of disk space. For a minimal installation \texttt{apt-get install
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann hets-core} instead of \texttt{hets}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item For Mac OSX 10.6 (Snow Leopard) we provide a meta package
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \texttt{Hets.mpkg} based on MacPorts that will be extended by further tools
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann for proving in the future.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThen we have Java based \Hets installer that we may drop in the future.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannDownload a \texttt{.jar} file and start it with
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannjava -jar \texttt{file.jar}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannNote that you need Sun Java 1.4.2 or later. On a Mac, you can just
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanndouble-click on the \texttt{.jar} file, but you have to install the MacPorts
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\texttt{libglade2} package (and all its dependencies) yourself. In order to
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannspeed this up we provide a meta package \texttt{libglade2.mpkg}, too.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe installer will lead you through the installation with
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanna graphical interface. It will download and install further
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannsoftware (if not already installed on your computer):
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{tabular}{|l|l|p{5cm}|}\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannHets-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannuDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannTcl/Tk & graphics widget system & (version 8.4 or 8.5 must be installed before)\\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\SPASS & theorem prover & \url{http://spass.mpi-sb.mpg.de/}\\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannDarwin & theorem prover & should be installed manually from \url{http://combination.cs.uiowa.edu/Darwin/}\\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann(X)Emacs & editor (for Isabelle) & (must be installed manually)\\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannIf you do not have Sun Java, you can just download the hets binary.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannYou have to unpack it with \texttt{bunzip2} and then put it at
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannsome place coverd by your \texttt{PATH}. You also have to
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanninstall the above mentioned software and set
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannseveral environment variables, as explained on the installation page.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannYou may compile \Hets from the sources, please follow the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannlink ``Hets: source code and information for developers''
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannon the \Hets web page, download the sources (as tarball or from
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannsvn), and follow the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanninstructions in the \texttt{INSTALL} file, but be prepared to take some time.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\end{enumerate}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannDepending on your application further tools are supported and may be
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanninstalled in addition:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{tabular}{|l|l|p{5cm}|}\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannzChaff & SAT solver & \url{http://www.princeton.edu/~chaff/zchaff.html} \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannminisat & SAT solver & \url{http://minisat.se/} \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannPellet & OWL reasoner & \url{http://clarkparsia.com/pellet/} \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannE-KRHyper & theorem prover
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann & \url{http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/} \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannReduce & computer algebra system
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann & \url{http://www.reduce-algebra.com/} \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannMaude & rewrite system & \url{http://maude.cs.uiuc.edu/} \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannVSE & theorem prover & (non-public) \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannTwelf & & \url{http://twelf.plparty.org/} \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\section{Analysis of Specifications}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannConsider the following \CASL
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannspecification:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{BIGEXAMPLE}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\I\SPEC \NAME{Strict\_Partial\_Order} =
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{ITEMS}[\PRED]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\I\SORT \( Elem \)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% \COMMENTENDLINE{\PRED abbreviates predicate}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\(\[ \FORALL x,y,z : Elem \\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{COMMENT}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannNote that there may exist \(x, y\) such that\\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannneither \(x < y\) nor \(y < x\).
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\end{BIGEXAMPLE}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\Hets can be used for parsing and
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannchecking static well-formedness of specifications.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \index{parsing}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \index{static!analysis}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \index{analysis, static}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannLet us assume that the example is in a file named
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\texttt{Order.casl} (actually, this file is provided
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannwith the \Hets distribution as \texttt{Hets-lib/UserManual/Chapter3.casl}).
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThen you can check the well-formedness of the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannspecification by typing (into some shell):
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\Hets checks both the correctness of this specification
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann with respect to the \CASL syntax, as
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannwell as its correctness with respect to the static semantics (e.g.\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannwhether all identifiers have been declared before they are used,
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannwhether operators are applied to arguments of the correct sorts,
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannwhether the use of overloaded symbols is unambiguous, and so on).
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe following flags are available in this context:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{description}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann -- the static analysis is skipped and no development is created.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[\texttt{-s}, \texttt{--just-structured}] Do the parsing and the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann static analysis of (heterogeneous) structured specifications, but
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann leave out the analysis of basic specifications. This can be used
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann for prototyping issues, namely to quickly produce a development graph
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann showing the dependencies among the specifications (cf.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Sect.~\ref{sec:DevGraph}) even if the individual specifications are
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann not correct yet.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannUse \texttt{DIR} as a colon separated list of directories for specification libraries (equivalently, you can set the variable \texttt{HETS\_LIB} before
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanncalling \Hets).
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[\texttt{-a ANALYSIS}, \texttt{--casl-amalg=ANALYSIS}]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann For the analysis of architectural specification (a quite advanced
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann amalgamability checking
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann algorithm for \CASL logic; it is a comma-separated list of zero or
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann more of the following options:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \begin{description}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \item[\texttt{sharing}] perform sharing analysis for sorts,
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann operations and predicates.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \item[\texttt{cell}] perform cell condition check; implies
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \texttt{sharing}. With this option on, the subsort embeddings are
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \item[\texttt{colimit-thinness}] perform colimit thinness check;
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann implies \texttt{sharing}. The colimit thinness check is less
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann complete and usually takes longer than the full cell condition
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann check (\texttt{cell} option), but may prove more efficient in case
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann of certain specifications.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \end{description}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann If \texttt{ANALYSIS} is empty then amalgamability analysis for
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \CASL is skipped.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann The default value for \texttt{--casl-amalg} is
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \texttt{cell}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\end{description}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\section{Heterogeneous Specification} \label{sec:HetSpec}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\Hets accepts plain text input files with the following endings:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{tabular}{|l|c|c|}\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannEnding & default logic & structuring language\\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\texttt{.casl} & \CASL & \CASL \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\texttt{.het} & \CASL & \CASL \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\texttt{.hs} & Haskell & Haskell\\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\texttt{.owl} & OWL DL, OWL Lite & OWL\\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\texttt{.elf} & LF & Twelf \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\texttt{.clf} or \texttt{.clif} & CommonLogic & \CASL \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\texttt{.maude} & Maude & Maude \\\hline
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannFurthermore, \texttt{.xml} files are accepted as Catia output if the default
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannlogic is set to DMU before a library import or by the ``\texttt{-l DMU}''
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanncommand line option of \Hets. In all other cases \texttt{.xml} files are
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannassumed to be development graph files as produced by ``\texttt{-o xml}''.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannAlthough the endings \texttt{.casl} and \texttt{.het} are
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanninterchangeable, the former should be used for libraries of
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannhomogeneous \CASL specifications and the latter for \HetCASL libraries
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannof heterogeneous specifications (that use the \CASL structuring
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannconstructs). Within a \HetCASL library, the current logic can be changed e.g.\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannto \HasCASL in the following way:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{verbatim}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\end{verbatim}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe subsequent specifications are then parsed and analysed as
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\HasCASL specifications. Within such specifications,
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannit is possible to use references to named \CASL specifications;
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannthese are then automatically translated along the default
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannembedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann(There are also heterogeneous constructs
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannfor explicit translations between logics, see \cite{Mossakowski04}.)
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannA \CspCASL specification consists of a \CASL specification
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannfor the data part and a \Csp process built over this data part.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannTherefore, \HetCASL provides a heterogeneous language construct
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\texttt{data} as follows:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{verbatim}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannlibrary Buffer
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann free type List[Elem] ::= nil | cons(Elem; List[Elem])
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann ops last: List -> ? Elem;
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann rest: List -> ? List
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann channel read, write : Elem
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann process Buf(List): read, write, List;
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann EmptyBuffer : read,write, List;
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Buf(l)= read? x :: Elem -> Buf(cons(x,nil)) []
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann (if l=nil then STOP else
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann write!last(l) -> Buf(rest(l)))
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann EmptyBuffer = Buf(nil)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\end{verbatim}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannHere, the construct \texttt{data List} refers to the \CASL specification
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\texttt{List}, which is implicitly embedded into \CspCASL.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe ending \texttt{.hs} is available for directly reading in
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannHaskell programs % and HasSLe specifications,
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannand hence supports the Haskell module system.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannthe logic Haskell has to be chosen explicitly, and the \CASL structuring
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannsyntax needs to be used:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{verbatim}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannlibrary Factorial
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannspec Factorial =
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannfac :: Int -> Int
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannfac n = foldl (*) 1 [1..n]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\end{verbatim}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannNote that according to the Haskell syntax, Haskell function
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanndeclarations and definitions need to start with the first column of
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\section{Development Graphs}\label{sec:DevGraph}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannDevelopment graphs are a simple kernel formalism for (heterogeneous)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannstructured theorem proving and proof management.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannA development graph consists of a set of nodes (corresponding to whole
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannstructured specifications or parts thereof), and a set of arrows
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanncalled \emph{definition links}, indicating the dependency of each
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanninvolved structured specification on its subparts. Each node is
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannassociated with a signature and some set of local axioms. The axioms
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannof other nodes are inherited via definition links. Definition links
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannare usually drawn as black solid arrows, denoting an import of another
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannspecification.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannComplementary to definition links, which \emph{define} the theories of
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannrelated nodes, \emph{theorem links} serve for \emph{postulating}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannrelations between different theories. Theorem links are the central
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanndata structure to represent proof obligations arising in formal
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannTheorem links can be \emph{global} (drawn as solid arrows) or
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\emph{local} (drawn as dashed arrows): a global theorem link
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannpostulates that all axioms of the source node (including the inherited
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannones) hold in the target node, while a local theorem link only postulates
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannthat the local axioms of the source node hold in the target node.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannBoth definition and theorem links can be \emph{homogeneous},
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanni.e. stay within the same logic, or \emph{heterogeneous}, i.e.\ %% such that
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannthe logic changes along the arrow. Technically, this is the case
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannfor Grothendieck signature morphisms $(\rho,\sigma)$ where
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann$\rho\not=id$. This case is indicated with double arrows.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannTheorem links are initially displayed in red.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe \emph{proof
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann calculus} for development graphs
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\cite{MossakowskiEtAl05,Habil} is given by rules
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannthat allow for proving global theorem links by decomposing them
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanninto simpler (local and global) ones. Theorem links that have been
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannproved with this calculus are drawn in green. Local theorem links can
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannbe proved by turning them into \emph{local proof goals}. The latter
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanncan be discharged using a logic-specific calculus as given by an
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannentailment system for a specific institution. Open local
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannproof goals are indicated by marking the corresponding node in the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanndevelopment graph as red; if all local implications are proved, the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannnode is turned into green. This implementation ultimately is based
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannon a theorem \cite{Habil} stating soundness and relative completeness
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannof the proof calculus for heterogeneous development graphs.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannand in \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe following options let \Hets show the development graph of
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanna specification library:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{description}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[\texttt{-u}, \texttt{--uncolored}] no colors in shown graphs
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\end{description}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe following additional options also apply typical rules from the development
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanngraph calculus to the final graph and save applying these rule via the GUI.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{description}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[\texttt{-A}, \texttt{--apply-automatic-rule}] apply the automatic
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann strategy to the development graph. This is what you usual want in order to
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann get goals within nodes for proving.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[\texttt{-N}, \texttt{--normal-form}] compute all normal forms for nodes
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann with incoming hiding links. (This may take long and may not be implemented
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann for all logics.)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\end{description}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannLet us extend the above library \texttt{Order.casl}. One use of the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannlibrary might be to express the fact that the natural numbers form a
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannstrict partial order as a view, as follows:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{BIGEXAMPLE}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\end{BIGEXAMPLE}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{EXAMPLE}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\I\SPEC \NAMEDEFN{Natural\_Order\_2} =
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\IEXT{\NAMEREF{Natural}} \THEN
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\I\PRED \( \_\_<\_\_ : Nat \* Nat\)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\(\[ \FORALL x,y:Nat \\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \. 0 < suc(x) \\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \. \neg x < 0 \\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \. suc(x) < suc(y) \IFF x < y
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{EXAMPLE}%[\SLIDESMALL]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\NAMEREF{Natural\_Order\_2} =
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\I{} \( Elem \MAPSTO Nat\)
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannAgain, these specifications can be checked with \Hets. However, this
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannonly checks syntactic and static semantic well-formedness -- it is
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannby a strict partial ordering relation. Checking this requires theorem
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannproving, which will be discussed below.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannHowever, before coming to theorem proving, let us first inspect the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannproof obligations arising from a specification. This can be done with:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\texttt{hets -g Order.casl}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann(assuming that the above two specifications and the view
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannhave been added to the file
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\Hets now displays a so-called development graph
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann(which is just an overview graph showing the overall structure
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannof the specifications in the library), see Fig.~\ref{fig:dg0}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{figure}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{center}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\includegraphics[scale=0.7]{dg-order-0}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\caption{Sample development graph.\label{fig:dg0}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannNodes in a development graph correspond to \CASL specifications.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannArrows show how specifications are related by the structuring
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe black arrow denotes an ordinary import of
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannspecifications (generated by the extension), while the red arrow
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanndenotes a proof obligation (corresponding to the view).
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThis proof obligation needs to be discharged in order to
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannshow that the view is well-formed (then its color turns into green).
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannAs a more complex example, consider the following loose specification
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannof a sorting function, taken from the \CASL User Manual
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\cite{CASL-UM}, Chap.~6:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{BIGEXAMPLE}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\I\SPEC \NAMEREF{List\_Order\_Sorted}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{ITEMS}[\WITHIN]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{ITEMS}[\PRED]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\I\PRED \( \_\_is\_sorted : List \)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\(\[ \FORALL e,e': Elem; L : List \\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \. empty~is\_sorted \\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \. cons(e,empty)~is\_sorted \\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \. cons(e,cons(e',L))~is\_sorted \IFF
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{ITEMS}[\OP]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\I\OP \( order : List \TOTAL List \)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\end{BIGEXAMPLE}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe following specification of sorting by insertion also is taken from
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannthe \CASL User Manual \cite{CASL-UM}, Chap.~6:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{BIGEXAMPLE}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\I\SPEC \NAMEREF{List\_Order}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\phantomsection
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{ITEMS}[\WITHIN]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{ITEMS}[\OP]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\I\OP \( insert : Elem \* List \TOTAL List \)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\(\[ \FORALL e,e':Elem; L:List \\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \. insert(e, empty) = cons(e, empty) \\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \. insert(e, cons(e',L)) = \[ cons(e', insert(e,L)) \WHEN e' < e\\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \ELSE cons(e, cons(e',L)) \] \\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{ITEMS}[\OP]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\I\OP \( order : List \TOTAL List \)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\(\[ \FORALL e:Elem; L:List \\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \. order(empty) = empty \\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \. order(cons(e,L)) = insert(e, order(L)) \]\)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\end{BIGEXAMPLE}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannBoth specifications are related. To see this, we first inspect
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanntheir signatures. This is possible with:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\texttt{hets -g Sorting.casl}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannassuming that \texttt{Sorting.casl} contains the above specifications.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{figure}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{center}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\includegraphics[scale=0.7]{dg-order-1}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\caption{Development graph for the two sorting specifications.\label{fig:dg1}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannIn the above-mentioned development graph, we have two types of nodes.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe named ones correspond to named specifications, but there
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannare also unnamed nodes corresponding to anonymous basic
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannspecifications like the declaration of the $insert$ operation in
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\NAMEREF{List\_Order} above. Basically, there is an
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannunnamed node for each structured specification that is not named.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannAgain, the black arrows denote an ordinary import of specifications
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann(corresponding to the extensions and unions in the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannspecifications), while the blue arrows denote hiding (corresponding to
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannthe local specification).
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannBy clicking on the nodes, one can inspect their signatures.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannIn this way, we can see that both \NAMEREF{List\_Order\_Sorted} and
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\NAMEREF{List\_Order} have the same signature. Hence, it
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannis legal to add a view:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{EXAMPLE}%[\SLIDESMALL]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\I\VIEW \NAMEDEFN{v2}[\NAMEREF{Total\_Order}] ~:~ \NAMEREF{List\_Order\_Sorted}[\NAMEREF{Total\_Order}] \TO
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\NAMEREF{List\_Order}[\NAMEREF{Total\_Order}]
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannWe have already added this view to \texttt{Sorting.casl}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe corresponding
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannproof obligation between \NAMEREF{List\_Order\_Sorted} and
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\NAMEREF{List\_Order} is displayed in Fig.~\ref{fig:dg1}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann as a red arrow.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannHere is a summary of the types of nodes and links occurring in
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanndevelopment graphs:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{description}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Named nodes] correspond to a named specification.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Unnamed nodes] correspond to an anonymous specification.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Elliptic nodes] correspond to a specification in the current library.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Rectangular nodes] are external nodes corresponding to a specification
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann downloaded from another library.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Red nodes] have open proof obligations.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Yellow nodes] have an open conservativity proof obligations.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Green nodes] have all proof obligations resolved.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Black links] correspond to reference to other specifications (definition
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann links in the sense of \cite[IV:4]{CASL/RefManual}).
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Red links] correspond to open proof obligations (theorem links).
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Green links] correspond to proven theorem links.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Yellow links] correspond to proven theorem links with open
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann conservativity or to open hiding theorem links.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Blue links] correspond to hiding, free, or cofree definition links.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Violett links] correspond to a mixture of links becoming visible after
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann ``expand'' or ``Show unnamed nodes with open proofs''.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Solid links] correspond to global (definition or theorem)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannlinks in the sense of \cite[IV:4]{CASL/RefManual}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Dashed links] correspond to local (theorem) links in the sense of
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \cite[IV:4]{CASL/RefManual}. These are usually created after
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann ``Global-Decomposition'' or only be visible after ``Show newly added proven
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Single line links] have homogeneous signature morphisms (staying within
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann one and the same logic).
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Double line links] have heterogeneous signature morphisms (moving
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann between logics).
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\end{description}
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannWe now explain the menus of the development graph window.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannMost of the pull-down menus of the window are uDraw(Graph)-specific
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanntheir function can be looked up in the uDraw(Graph) documentation\footnote{see
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\url{http://www.informatik.uni-bremen.de/uDrawGraph/en/service/uDG31\_doc/}.}.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe exception is the Edit menu. Moreover, the nodes and links
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannof the graph have attached pop-up menus, which appear when
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannclicking with the right mouse button.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{description}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Edit] This menu has the following submenus:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{description}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Undo] Undo the last development graph proof step (see under Proofs)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Redo] Restore the last undone development graph proof step (see
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann under Proofs)
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThe ``Hide/show names/nodes/edges'' menu is a toggle:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannyou can switch on or off the display of node names, unnamed nodes or
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannproven theorem links.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannWith the ``Hide/show internal node names'' option, the nodes that
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannare initially unnamed get derived names.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannWith the ``Hide/show unnamed nodes without open proofs'' option, it is possible
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannto reveal the unnamed nodes which do not have open proof goals.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannInitially, the complexity of the graph is reduced by hiding all these nodes;
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannonly nodes corresponding to named specifications are displayed.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannPaths between named nodes going through unnamed nodes
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannare displayed as edges; these paths are then expanded when showing the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannunnamed nodes.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannWhen applying the development graph calculus rules, theorem links that have
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannbeen proven are removed from the graph. With the ``Hide/Show newly added
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannproven edges'' option, it is possible to re-display these links; they are marked
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannas proven in the link info (see \emph{Pop-up menu for links}, below).
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Focus node]
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThis menu is particularly useful when navigating in a large development graph,
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannwhich does not fit on a single screen. The list of all nodes is displayed:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannthe nodes are identified by the internal node number and the internal node name.
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannOnce a node is selected, the view centers on it.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Select Linktypes]
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannThis menu allows to select the type of links that are displayed in the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanndevelopment graph. A selection window appears, where links are grouped into
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannthree categories: definition links, proven theorem links and unproven
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanntheorem links. It is possible to select/deselect all links or to invert the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanncurrent selection.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Consistency checker]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Checks whether the theories of the nodes of the graph are consistent
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann i.e. have a model. The model finders currently interfaced are
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Isabelle-refute, darwin and E-KRHyper, with best support for darwin.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Proofs] This menu allows to apply some of the deduction rules
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann for development graphs, see Sect. IV:4.4 of the \CASL Reference
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Manual \cite{CASL/RefManual} or one of
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}. While support for
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann local and global (definition or theorem) links is stable, support
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann for hiding links and checking conservativity is still experimental.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann In most cases, it is advisable to use ``Automatic'', which
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann automatically applies the rules in the correct order. As a result,
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann the open theorem links (marked in red) will be reduced to local
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann proof goals, that is, they become green, and instead, some target nodes
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann may get red, indicating open local proof goals.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Besides the deduction rules, the menu contains entries for computing
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann a colimit approximation for the development graph and for
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann computing normal forms of all nodes (needed when dealing with hiding).
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Also, a \CASL-specific normalisation of free links has been
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Dump Development Graph] This option is available only for
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann debugging purposes; it outputs a textual representation
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann of the development graph.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Show Library Graph] This menu displays the library graph, in a separate
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann window, if the library graph window has been closed after \Hets has been
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Save Graph for uDrawGraph] Saves the development graph in a .udg file
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann which can be later read by uDrawGraph.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Save proof-script] This menu saves the proof rules that have been applied
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann to the current development graph in a .hpf file which can be later read by
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \Hets and thus the action performed on the graph are saved.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\end{description}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Pop-up menu for nodes]
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannHere, the number of submenus depends on the type of the node:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\begin{description}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Show node info] Shows the local informations of the node: the internal
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann node name and node number, the xpath that denotes the location of the node
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann within an XML representation, information about consistency of the node,
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann origin of the node and the local theory i.e. axioms declared locally.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\item[Show theory] Shows the theory of the node (including axioms
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimported from other nodes). Notice that axioms imported via hiding links
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannare not part of the theory; they can be made visible only by re-adding
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannthe hidden symbols, using the normal form of the node, by calling
\emph{Proofs/Compute Normal Form}. For such nodes, a warning is displayed.
between them, i.e. translation (blue links) and inclusion (black links).
| graph.(exp.dot|dot)
The \texttt{owl} option \cite{books/sp/Kohlhase06} will produce OWL files in
The \texttt{omdoc} format \cite{books/sp/Kohlhase06} is an XML-based
When the \texttt{comptable.xml} format is selected, \Hets will extract
algebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
available from \texttt{www.cofi.info/Libraries}.
printed \LaTeX\ version of \texttt{Order.casl} by typing:
This will generate a file \texttt{Order.pp.tex}. It can be included
into \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
coming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty}) is used.
The format \texttt{pp.xml} represents a library in XML for our change
The \texttt{tptp} format (\url{http://www.tptp.org}) is a standard
\item[\texttt{-l LOGIC}, \texttt{--logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
\item[\texttt{-m FILE}, \texttt{--modelSparQ=FILE}] model check a qualitative calculus given in SparQ lisp notation \cite{SparQ06} against a \CASL specification
prover, i.e. by using the ``Prove'' menu of a red node.
% http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0
\url{http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0}
\cite{DBLP:conf/tacas/Aspinall00,url:ProofGeneral} in a separate Emacs
The \Isabelle theory file conforms to the Isabelle/Isar syntax
\url{http://www.reduce-algebra.com/}. Installation is possible as follows:
E-KRHyper\footnote{\url{http://www.uni-koblenz.de/~bpelzer/ekrhyper/}}
KRHyper\footnote{\url{http://www.uni-koblenz.de/~wernhard/krhyper/}} by
version, where e.g.\ error handling is ignored. For technical reasons
the static analysis of basic specifications) and/or translates (along
of the \Hets home page at \url{http://www.dfki.de/sks/hets}.
%\input{hets.tex}