UserGuide.tex revision ab5781bda9fa3062a3a92c4b57fa6bc7b70c745a
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\documentclass{article}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage[hide]{ed} % set to hide for producing a released version
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{alltt}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{casl}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{color}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{url}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{threeparttable,hhline}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{paralist}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\usepackage[pdfborder=0 0 0,bookmarks,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederpdfauthor={Till Mossakowski, Christian Maeder, Mihai Codescu},
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederpdftitle={Hets User Guide}]
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder{hyperref} %% do not load more packages after this line!!
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\QUERY}[1]%{}
dc89cfbc150be3b6792f559f57b6e91cd7affacbJonathan von Schroeder{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
dc89cfbc150be3b6792f559f57b6e91cd7affacbJonathan von Schroeder\newcommand{\eat}[1]{}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\IEXT}[1] {\\#1\I}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\IEND} {\I\END}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newenvironment{EXAMPLEFORMAT} {}{}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%% Added by MB to have some extra vertical space after the ``main'' examples
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%% following the points (and some others in the text):
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newenvironment{BIGEXAMPLE} {\begin{EXAMPLE}} {\end{EXAMPLE}\medskip}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newenvironment{DETAILSFORMAT} {}{}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newenvironment{META}[1][] {#1\begin{METAFORMAT}}{\end{METAFORMAT}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newenvironment{METAFORMAT} {\medskip\vrule\hspace{1ex}\vrule\hspace{1ex}%
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \begin{minipage}{0.9\textwidth}\it}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder {\end{minipage}\par\medskip}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\SLIDESMALL} {}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\SLIDESONLY}[1] {}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder% SIMULATING SMALL-CAPS FOR BOLD, EMPH
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%\newcommand {\CoFI}{CoFI\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeELAN} {\largeTEXTSC{E}{LAN}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\HOL}{\normalTEXTSC{H}{OL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\Isabelle}{\normalTEXTSC{I}{SABELLE}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\newcommand {\SPASS}{\normalTEXTSC{S}{PASS}\xspace}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%%%%% Klaus macros
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\SROIQ}{$\mathcal{SROIQ}$(\textbf{D})\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\DL}{DL\xspace}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder%%%%% end of Klaus macros
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\LCF}{LCF\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\ASF}{ASF\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\SDF}{SDF\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%% Do NOT use \ASF+\SDF (it gives a superfluous space in the middle)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\CCC}{CCC\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\CoCASL}{\normalTEXTSC{C}{O}\normalTEXTSC{C}{ASL}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\CspCASL}{\normalTEXTSC{C}{SP}-\normalTEXTSC{C}{ASL}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\begin{document}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\title{{\bf \protect{\LARGEHets} User Guide}\\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder-- Version 0.98 --}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\author{Till Mossakowski, Christian Maeder,
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder Mihai Codescu\\[1em]
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederDFKI GmbH, Bremen, Germany.\\[1em]
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederComments to: hets-users@informatik.uni-bremen.de \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder(the latter needs subscription to the mailing list)
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\section{Introduction}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThe central idea of the Heterogeneous Tool Set (\protect\Hets) is to
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederprovide an open source general framework for formal methods
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederintegration and proof management. One can think of \Hets acting like a
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedermotherboard where different expansion cards can be plugged in, the
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederexpansion cards here being individual logics (with their analysis and
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederproof tools) as well as logic translations. Individual logics and
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroedertheir analysis and proof tools can be plugged into the \Hets
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroedermotherboard using an object-oriented interface based on institutions
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\cite{GoguenBurstall92}. The \Hets motherboard already has plugged in
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedera number of expansion cards (e.g., the theorem provers Isabelle, SPASS
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederand more, as well as model finders). Hence, a variety of tools is
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederavailable, without the need to hard-wire each tool to the logic at
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \includegraphics[width=0.45\textwidth]{hets-motherboard}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\caption{The \Hets motherboard and some expansion cards}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\Hets supports a number of input languages directly, such as \CASL,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederCommon Logic, OWL-DL, Haskell, and Maude. For heterogeneous
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederspecification, \Hets offers the language heterogeneous \CASL.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederHeterogeneous \CASL (\HetCASL) generalises the structuring
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\CASL \cite{CASL-UM,CASL/RefManual} to arbitrary logics
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder(if they are formalised as institutions and plugged into
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederthe \Hets motherboard), as well as to heterogeneous
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercombination of specification written in different logics.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederFig.~\ref{fig:lang} for a simple subset of the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\HetCASL syntax, where \emph{basic specifications} are unstructured
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederspecifications or modules written in a specific logic. The graph of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercurrently supported logics and logic translations (the latter are also
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercalled comorphisms) is shown in Fig.~\ref{fig:LogicGraph}, and the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdegree of support by \Hets in Fig.~\ref{fig:Languages}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{figure}[ht]
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{verbatim}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederSPEC ::= BASIC-SPEC
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder | SPEC then SPEC
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder | SPEC then %implies SPEC
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder | SPEC with SYMBOL-MAP
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder | SPEC with logic ID
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederDEFINITION ::= logic ID
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder | spec ID = SPEC end
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder | view ID : SPEC to SPEC = SYMBOL-MAP end
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder | view ID : SPEC to SPEC = with logic ID end
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederLIBRARY = DEFINITION*
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\caption{Syntax of a simple subset of the heterogeneous
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederspecification language.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\texttt{BASIC-SPEC} and \texttt{SYMBOL-MAP} have a logic
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederspecific syntax, while \texttt{ID} stands for some form of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederidentifiers.\label{fig:lang}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederWith \emph{heterogeneous structured specifications}, it is possible to
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedercombine and rename specifications, hide parts thereof, and also
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedertranslate them to other logics. \emph{Architectural specifications}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederprescribe the structure of implementations. \emph{Specification
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder libraries} are collections of named structured and architectural
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\Hets consists of logic-specific tools for the parsing and static
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederanalysis of the different involved logics, as well as a
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederlogic-independent parsing and static analysis tool for structured and
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederarchitectural specifications and libraries. The latter of course needs
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederto call the logic-specific tools whenever a basic specification is
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\Hets is based on the theory of institutions \cite{GoguenBurstall92},
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederwhich formalize the notion of a logic. The theory behind \Hets is laid
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederout in \cite{Habil}. A short overview of \Hets is given in
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\cite{MossakowskiEA06,MossakowskiEtAl07b}.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\section{Logics supported by Hets}
a845310274d5bcd9da2df61599fd58eaf96ded13Jonathan von SchroederThe following list of logics (formalized as so-called institutions
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\cite{GoguenBurstall92}) is currently supported by \Hets:
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \includegraphics[scale=0.4]{LogicGraph}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\caption{Graph of logics currently supported by \Hets. The more an
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederellipse is filled with green, the more stable is the implementation of the logic. Blue indicates a prover-supported logic.}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\label{fig:LogicGraph}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\begin{tabular}{|l|c|c|c|}\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederLanguage & Parser & Static Analysis & Prover \\\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\CASL & x & x & - \\\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\CoCASL & x & x & - \\\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\ModalCASL & x & x & - \\\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\HasCASL & x & x & - \\\hline
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederHaskell & (x) & x & - \\\hline
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederCspCASL & x & x & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCspCASL\_Trace & - & - & x \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCspCASL\_Failure & - & - & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCommonLogic & x & x & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederConstraint\CASL & x & (x) & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederTemporal & x & (x) & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederRelScheme & x & (x) & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederDFOL & x & (x) & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederExtModal & x & (x) & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederLF & x & (x) & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%Structured specifications & x & x & (x) \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%Architectural specifications & x & x & -\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\CASLDL & x & - & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederDMU & x & - & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederFreeCAD & - & - & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederOWL DL & x & x & x \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederPropositional & x & x & x \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederQBF & x & x & x \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederSoftFOL & x & - & x \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederMaude & x & x & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederVSE & x & x & x \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\Isabelle & (x) & - & x \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHolLight & (x) & - & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederAdl & x & x & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederFpl & x & x & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederEnCL & x & x & x \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\caption{Current degree of \Hets support for the different languages. Languages without prover can still ``borrow'' provers
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedervia logic translations.\label{fig:Languages}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{description}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[CASL] extends many sorted first-order logic with partial
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder functions and subsorting. It also provides induction sentences,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder expressing the (free) generation of datatypes.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%It is mainly designed and used for the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%specification of requirements for software systems. But it is also
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%used for the specification of \Dolce (Descriptive Ontology for
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%Linguistic and Cognitive Engineering), an Upper Ontology for knowledge
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%representation. \cite{Gangemi:2002:SOD} Further it is now used to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%specify calculi for time and space.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederFor more details on \CASL see \cite{CASL/RefManual,CASL-UM}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederWe have implemented the \CASL logic in such a way that much of the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederimplementation can be re-used for \CASL extensions as well; this
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederis achieved via ``holes'' (realized via polymorphic variables) in the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedertypes for signatures, morphisms, abstract syntax etc. This eases
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederintegration of \CASL extensions and keeps the effort of integrating
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\CASL extensions quite moderate.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[CoCASL] \cite{MossakowskiEA04} is a coalgebraic extension of \CASL,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersuited for the specification of process types and reactive systems.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe central proof method is coinduction.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[ModalCASL] \cite{ModalCASL}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder is an extension of \CASL with multi-modalities and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederterm modalities. It allows the specification of modal systems with
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederKripke's possible worlds semantics. It is also possible to express
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercertain forms of dynamic logic.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[ExtModal] is an extended modal logic, currently in an experimental state.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[HasCASL] is a higher order extension of \CASL allowing
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder polymorphic datatypes and functions. It is closely related to the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder programming language Haskell and allows program constructs being
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder embedded in the specification.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederthe language is summarized in \cite{HasCASL/Summary}, the semantics
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederin \cite{Schroder05b,Schroder-habil}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[Haskell] is a modern, pure and strongly typed functional
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder programming language. It simultaneously is the implementation
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder language of \Hets, such that in the future, \Hets might be applied
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe definitive reference for Haskell is \cite{PeytonJones03},
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[CspCASL] \cite{Roggenbach06} is a combination of \CASL
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder with the process algebra \Csp.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[CommonLogic] \url{http://en.wikipedia.org/wiki/Common_logic}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[ConstraintCASL] is an experimental logic for the specification
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederof qualitative constraint calculi.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[OWL DL] is the Web Ontology Language (OWL) recommended by the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder World Wide Web Consortium (W3C, \url{http://www.w3c.org}). It is
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder used for knowledge representation and the Semantic Web
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \cite{berners:2001:SWeb}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHets calls an external OWL DL parser
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder written in JAVA to obtain the abstract syntax for an OWL file and its
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder imports. The JAVA parser is also doing a first analysis classifying
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder the OWL ontology into the sublanguages OWL Full, OWL DL and OWL
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder Hets only supports the last two, more restricted variants.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder structuring of the OWL imports is displayed as Development Graph.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[CASL-DL] \cite{OWL-CASL-WADT2004}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederis an extension of a restriction of \CASL, realizing
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedera strongly typed variant of OWL DL in \CASL syntax.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \CASL with cardinality restrictions for the description of sorts and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder unary predicates. The restrictions are based on the equivalence
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder between \CASLDL, OWL~DL and \SHOIN. Compared to \CASL only unary
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder and binary predicates, predefined datatypes and concepts (subsorts
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder of the topsort Thing) are allowed. It is used to bring OWL DL and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \CASL closer together.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[Propositional] is classical propositional logic, with
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederthe zChaff SAT solver \cite{Herbstritt03} connected to it.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[QBF] are quantified boolean formulas, with
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederDepQBF \url{http://fmv.jku.at/depqbf/} connected to it.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[RelScheme] is a logic for relational databases \cite{DBLP:journals/ao/SchorlemmerK08}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[SoftFOL] \cite{LuettichEA06a} offers several automated theorem
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder proving (ATP) systems for first-order logic with equality: \begin{inparaenum}[(1)]\item \SPASS
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \cite{WeidenbachEtAl02}, see \url{http://www.spass-prover.org};
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item Vampire \cite{RiazanovV02} see \url{http://www.vprover.org};
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item Darwin \cite{Baumgartner:etal:Darwin:IJAIT:2005}, see \url{http://combination.cs.uiowa.edu/Darwin};
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item Eprover \cite{Schulz:AICOM-2002}, see {http://www.eprover.org};
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item E-KRHyper \cite{DBLP:conf/cade/PelzerW07}, see {http://www.uni-koblenz.de/~bpelzer/ekrhyper}, and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder MathServe Broker\footnote{which chooses an appropriate ATP upon a
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder classification of the FOL problem} \cite{ZimmerAutexier06}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\end{inparaenum}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder These together comprise some of the most advanced theorem provers
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder for first-order logic. SoftFOL is essentially the first-order
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder interchange language TPTP \cite{DBLP:conf/lpar/Sutcliffe10},
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder for higher-order logic.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[HolLight] \url{http://www.cl.cam.ac.uk/~jrh13/hol-light/}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder is John Harrison's interactive theorem prover
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder for higher-order logic.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[VSE] is an interactive theorem prover, see \ref{subsec:VSE}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[DMU] is a dummy logic to read output of ``Computer Aided
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder Three-dimensional Interactive Application'' (Catia).
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[FreeCAD] is a logic to read design files of the CAD system
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder FreeCAD\\\url{http://sourceforge.net/projects/free-cad}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[Maude] is a rewrite system \url{http://maude.cs.uiuc.edu/} for
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder first-order logic. In order to use this logic the environment variable
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \verb+HETS_MAUDE_LIB+ must be set to a directory containing the files
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \verb+full-maude.maude+, \verb+hets.prj+, \verb+maude2haskell.maude+ and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[DFOL] is an extension of first-order logic with dependent types \cite{rabe:dfol:06}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item [LF] is the dependent type theory of Twelf \url{http://twelf.plparty.org/}. Hets
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder calls Twelf on \verb+.elf+ files (for this, the environment variable
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \verb+TWELF_LIB+ must be set) and reads in the OMDoc generated by Twelf.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder Moreover, LF can be used as a logical framework to add new logics in Hets \cite{CHK+2011a}.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder Logic definitions in LF are based in the logic atlas of the Latin project \cite{project:latin}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder and therefore the environment variable \verb+LATIN_LIB+ must be set to the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder repository with the Latin logic definitions.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\item[Framework] is a dummy logic added for declarative logic definitions \cite{CHK+2011a}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[Adl] is ``A Description Language'' based on relational algebra originally
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder designed for requirements engineering of business rules
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \url{https://lab.cs.ru.nl/BusinessRules/Requirements_engineering}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[Fpl] is a ``logic for functional programs'' as an extension of a
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder restriction of \CASL. (\CASL predicates are disabled.)
dc89cfbc150be3b6792f559f57b6e91cd7affacbJonathan von Schroeder A detailed description of FPL will appear elsewhere.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\item[EnCL] is an ``engineering calculation language'' based on first
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder order theory of real numbers with some predefined binders
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \cite{logic:EnCL}. It allows the formulation of executable
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder specifications of engineering calculation methods. For the execution
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder of these specifications Hets provides connections to the computer
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder algebra systems Mathematica, Maple and Reduce.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\item[THF] is an interchange language for higher-order logic
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \cite{DBLP:conf/cade/BenzmullerRS08}, similar to what TPTP
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder is for first-order logic. \Hets connects THF to the automated
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder higher-order prover Leo-II.
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\end{description}
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederVarious logics are supported with proof tools. Proof support for the
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederother logics can be obtained by using logic translations to a
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederprover-supported logic.
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederAn introduction to \CASL can be found in the \CASL User Manual
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\cite{CASL-UM}; the detailed language reference is given in
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederthe \CASL Reference Manual \cite{CASL/RefManual}. These documents
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederexplain both the \CASL logic and language of basic specifications as
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederwell as the logic-independent constructs for structured and
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederarchitectural specifications. The corresponding document explaining the
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\HetCASL language constructs for \emph{heterogeneous} structured specifications
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederis the \HetCASL language summary \cite{Mossakowski04}; a formal
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroedersemantics as well as a user manual with more examples are in preparation.
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederSome of \HetCASL's heterogeneous constructs will be illustrated
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederin Sect.~\ref{sec:HetSpec} below.
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\section{Logic translations supported
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\label{comorphisms}
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederLogic translations (formalized as institution comorphisms
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\cite{GoguenRosu02}) translate from a given source logic to a given
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedertarget logic. More precisely, one and the same logic translation
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedermay have several source and target \emph{sub}logics: for
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedereach source sublogic, the corresponding sublogic of the target
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederlogic is indicated.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederA graph of the most important logics and sublogics, together with their
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedercomorphisms, is shown in Fig.~\ref{fig:SublogicGraph}.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \includegraphics[scale=0.4]{SublogicGraph}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\caption{Graph of most important sublogics currently supported by \Hets,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedertogether with their comorphisms.}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\label{fig:SublogicGraph}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederIn more detail, the following list of logic translations is currently
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedersupported by \Hets:
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\begin{tabular}{|l|p{8cm}|}\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederAdl2CASL & inclusion taking relations to CASL predicates \\\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederCASL2CoCASL & inclusion \\\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederCASL2CspCASL & inclusion \\\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederCASL2HasCASL & inclusion \\\hline
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederCASL2Isabelle & inclusion on sublogic CFOL=
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder(translation $(7)$ of \cite{Mossakowski02}) \\\hline
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederCASL2Modal & inclusion \\\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederCASL2PCFOL & coding of subsorting (SubPCFOL=) by injections, see Chap.\ III:3.1 of the CASL Reference Manual \cite{CASL/RefManual} \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2PCFOLTopSort & coding of subsorting (SulPeCFOL=) by a top sort and unary
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederpredicates for the subsorts \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2Propositional & translation of propositional FOL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2SoftFOL & coding of CASL.SuleCFOL=E to SoftFOL \cite{LuettichEA06a},
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedermapping types to soft types \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2SoftFOLInduction & same as CASL2SoftFOL but with instances of induction
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederaxioms for all proof goals \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2SoftFOLInduction2 & similar to CASL2SoftFOLInduction but replaces goals with induction premises \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2SubCFOL & coding of partial functions by error elements
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder(translation $(4a')$ of \cite{Mossakowski02}, but extended to subsorting, i.e. sublogic SubPCFOL=) \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2VSE & inclusion on sublogic CFOL= \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2VSEImport & inclusion on sublogic CFOL= \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2VSERefine & refining translation of CASL.CFOL= to VSE \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL\_DL2CASL & inclusion \\\hline
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederCoCASL2CoPCFOL & coding of subsorting by injections, similar to CASL2PCFOL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCoCASL2CoSubCFOL & coding of partial functions by error supersorts, similar to CASL2SubCFOL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCoCASL2Isabelle & extended translation similar to CASL2Isabelle \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCommonLogic2CASL & Coding Common Logic to \CASL.Module elimination
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder is applied before translating to \CASL. \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCommonLogic2CASLCompact & Coding compact Common Logic to \CASL.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder Compact Common Logic is a sublogic of Common Logic
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder where no sequence markers occur. Module elimination
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder is applied before translating to \CASL. We recommend
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder using this comorphism whenever possible because it
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder results in simpler specifications.\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCommonLogicModuleElimination & Eliminating modules from a Common Logic theory
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder resulting in an equivalent specification without
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder modules. \\\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederCspCASL2CspCASL\_Failure & inclusion \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCspCASL2CspCASL\_Trace & inclusion \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCspCASL2Modal & translating the CASL data part to ModalCASL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederDFOL2CASL & translating dependent types \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederDMU2OWL & interpreting Catia output as OWL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{tabular}{|l|p{7cm}|}\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHasCASL2HasCASLNoSubtypes & coding out subtypes \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHasCASL2HasCASLPrograms & coding of \HasCASL axiomatic recursive definitions
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederas \HasCASL recursive program definitions \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHasCASL2Haskell & translation of \HasCASL recursive program definitions to Haskell \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHasCASL2IsabelleOption & coding of HasCASL to Isabelle/HOL \cite{Groening05} \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHaskell2Isabelle & coding of Haskell to Isabelle/HOL \cite{TorriniEtAl07} \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHaskell2IsabelleHOLCF & coding of Haskell to Isabelle/HOLCF \cite{TorriniEtAl07} \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHolLight2Isabelle & coding of HolLight to Isabelle/HOL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederMaude2CASL & encoding of rewrites as predicates \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederModal2CASL & the standard translation of modal logic
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederto first-order logic \cite{blackburn_p-etal:2001a} \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederOWL2CASL & inclusion \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederOWL2CommonLogic & inclusion \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederPropositional2CASL & inclusion \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederPropositional2QBF & inclusion \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederQBF2Propositional & inclusion \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederRelScheme2CASL & inclusion \\\hline
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\section{Getting started}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederThe latest \Hets version can be obtained from the
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\Hets tools home page
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder Since \Hets is being
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederimproved constantly, it is recommended always to use the latest version.
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\Hets is currently available (on Intel architectures only) for Linux
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederThere are several possibilities to install \Hets.
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\begin{enumerate}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederThe best support is currently given via Ubuntu packages.
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\begin{verbatim}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroedersudo apt-add-repository ppa:hets/hets
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroedersudo apt-add-repository \
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder "deb http://archive.canonical.com/ubuntu lucid partner"
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroedersudo apt-get update
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroedersudo apt-get install hets
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederThis will also install quite a couple of tools for proving requiring about
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder800 MB of disk space. For a minimal installation \texttt{apt-get install
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder hets-core} instead of \texttt{hets}.
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\item For Mac OSX 10.6 (Snow Leopard) we provide a meta package
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder \texttt{Hets.mpkg} based on MacPorts that will be extended by further tools
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder for proving in the future.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThen we have Java based \Hets installer that we may drop in the future.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederDownload a \texttt{.jar} file and start it with
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederjava -jar \texttt{file.jar}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederNote that you need Sun Java 1.4.2 or later. On a Mac, you can just
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederdouble-click on the \texttt{.jar} file, but you have to install the MacPorts
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\texttt{libglade2} package (and all its dependencies) yourself. In order to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederspeed this up we provide a meta package \texttt{libglade2.mpkg}, too.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThe installer will lead you through the installation with
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedera graphical interface. It will download and install further
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedersoftware (if not already installed on your computer):
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{tabular}{|l|l|p{5cm}|}\hline
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederHets-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederuDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederTcl/Tk & graphics widget system & (version 8.4 or 8.5 must be installed before)\\\hline
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\SPASS & theorem prover & \url{http://spass.mpi-sb.mpg.de/}\\\hline
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederDarwin & theorem prover & should be installed manually from \url{http://combination.cs.uiowa.edu/Darwin/}\\\hline
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder(X)Emacs & editor (for Isabelle) & (must be installed manually)\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIf you do not have Sun Java, you can just download the hets binary.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederYou have to unpack it with \texttt{bunzip2} and then put it at
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersome place coverd by your \texttt{PATH}. You also have to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederinstall the above mentioned software and set
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederseveral environment variables, as explained on the installation page.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederYou may compile \Hets from the sources (they are licensed under GPL),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederplease follow the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederlink ``Hets: source code and information for developers''
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederon the \Hets web page, download the sources (as tarball or from
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroedersvn), and follow the
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroederinstructions in the \texttt{INSTALL} file, but be prepared to take some time.
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von SchroederDepending on your application further tools are supported and may be
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederinstalled in addition:
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{tabular}{|l|l|p{5cm}|}\hline
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederzChaff & SAT solver & \url{http://www.princeton.edu/~chaff/zchaff.html} \\\hline
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederminisat & SAT solver & \url{http://minisat.se/} \\\hline
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederPellet & OWL reasoner & \url{http://clarkparsia.com/pellet/} \\\hline
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederE-KRHyper & theorem prover
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & \url{http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/} \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederReduce & computer algebra system
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder & \url{http://www.reduce-algebra.com/} \\\hline
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederMaude & rewrite system & \url{http://maude.cs.uiuc.edu/} \\\hline
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederVSE & theorem prover & (non-public) \\\hline
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederTwelf & & \url{http://twelf.plparty.org/} \\\hline
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\section{Analysis of Specifications}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederConsider the following \CASL
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{BIGEXAMPLE}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\I\SPEC \NAME{Strict\_Partial\_Order} =
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{ITEMS}[\PRED]
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\I\SORT \( Elem \)
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder% \COMMENTENDLINE{\PRED abbreviates predicate}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\(\[ \FORALL x,y,z : Elem \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederNote that there may exist \(x, y\) such that\\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederneither \(x < y\) nor \(y < x\).
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\end{BIGEXAMPLE}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\Hets can be used for parsing and
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederchecking static well-formedness of specifications.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \index{parsing}%
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \index{static!analysis}%
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \index{analysis, static}%
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederLet us assume that the example is in a file named
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\texttt{Order.casl} (actually, this file is provided
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederwith the \Hets distribution as \texttt{Hets-lib/UserManual/Chapter3.casl}).
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederThen you can check the well-formedness of the
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederspecification by typing (into some shell):
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\Hets checks both the correctness of this specification
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder with respect to the \CASL syntax, as
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederwell as its correctness with respect to the static semantics (e.g.\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederwhether all identifiers have been declared before they are used,
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederwhether operators are applied to arguments of the correct sorts,
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederwhether the use of overloaded symbols is unambiguous, and so on).
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederThe following flags are available in this context:
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{description}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder -- the static analysis is skipped and no development is created.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\item[\texttt{-s}, \texttt{--just-structured}] Do the parsing and the
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder static analysis of (heterogeneous) structured specifications, but
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder leave out the analysis of basic specifications. This can be used
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder for prototyping issues, namely to quickly produce a development graph
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder showing the dependencies among the specifications (cf.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder Sect.~\ref{sec:DevGraph}) even if the individual specifications are
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder not correct yet.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederUse \texttt{DIR} as a colon separated list of directories for specification libraries (equivalently, you can set the variable \texttt{HETS\_LIB} before
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\item[\texttt{-a ANALYSIS}, \texttt{--casl-amalg=ANALYSIS}]
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder For the analysis of architectural specification (a quite advanced
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder amalgamability checking
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder algorithm for \CASL logic; it is a comma-separated list of zero or
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder more of the following options:
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \begin{description}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \item[\texttt{sharing}] perform sharing analysis for sorts,
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder operations and predicates.
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder \item[\texttt{cell}] perform cell condition check; implies
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder \texttt{sharing}. With this option on, the subsort embeddings are
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \item[\texttt{colimit-thinness}] perform colimit thinness check;
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder implies \texttt{sharing}. The colimit thinness check is less
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder complete and usually takes longer than the full cell condition
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder check (\texttt{cell} option), but may prove more efficient in case
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder of certain specifications.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \end{description}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder If \texttt{ANALYSIS} is empty then amalgamability analysis for
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \CASL is skipped.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder The default value for \texttt{--casl-amalg} is
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder\end{description}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\section{Heterogeneous Specification} \label{sec:HetSpec}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\Hets accepts plain text input files with the following endings:
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{tabular}{|l|c|c|}\hline
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederEnding & default logic & structuring language\\\hline
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\texttt{.casl} & \CASL & \CASL \\\hline
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\texttt{.het} & \CASL & \CASL \\\hline
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\texttt{.hol} & HolLight & HolLight \\\hline
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\texttt{.hs} & Haskell & Haskell \\\hline
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\texttt{.owl} & OWL DL, OWL Lite & OWL \\\hline
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\texttt{.elf} & LF & Twelf \\\hline
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\texttt{.clf} or \texttt{.clif} & CommonLogic & \CASL \\\hline
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\texttt{.maude} & Maude & Maude \\\hline
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederFurthermore, \texttt{.xml} files are accepted as Catia output if the default
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederlogic is set to DMU before a library import or by the ``\texttt{-l DMU}''
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedercommand line option of \Hets. In all other cases \texttt{.xml} files are
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederassumed to be development graph files as produced by ``\texttt{-o xml}''.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederAlthough the endings \texttt{.casl} and \texttt{.het} are
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederinterchangeable, the former should be used for libraries of
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederhomogeneous \CASL specifications and the latter for \HetCASL libraries
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederof heterogeneous specifications (that use the \CASL structuring
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederconstructs). Within a \HetCASL library, the current logic can be changed e.g.\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederto \HasCASL in the following way:
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{verbatim}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThe subsequent specifications are then parsed and analysed as
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\HasCASL specifications. Within such specifications,
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederit is possible to use references to named \CASL specifications;
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederthese are then automatically translated along the default
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederembedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder(There are also heterogeneous constructs
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederfor explicit translations between logics, see \cite{Mossakowski04}.)
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederA \CspCASL specification consists of a \CASL specification
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederfor the data part and a \Csp process built over this data part.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederTherefore, \HetCASL provides a heterogeneous language construct
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\texttt{data} as follows:
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{verbatim}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder free type List[Elem] ::= nil | cons(Elem; List[Elem])
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder ops last: List -> ? Elem;
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder rest: List -> ? List
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder channel read, write : Elem
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder process Buf(List): read, write, List;
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder EmptyBuffer : read,write, List;
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder Buf(l)= read? x :: Elem -> Buf(cons(x,nil)) []
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder (if l=nil then STOP else
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder write!last(l) -> Buf(rest(l)))
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder EmptyBuffer = Buf(nil)
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von SchroederHere, the construct \texttt{data List} refers to the \CASL specification
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder\texttt{List}, which is implicitly embedded into \CspCASL.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederThe ending \texttt{.hs} is available for directly reading in
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederHaskell programs % and HasSLe specifications,
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederand hence supports the Haskell module system.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederthe logic Haskell has to be chosen explicitly, and the \CASL structuring
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedersyntax needs to be used:
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder\begin{verbatim}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederlibrary Factorial
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederspec Factorial =
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederfac :: Int -> Int
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederfac n = foldl (*) 1 [1..n]
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von SchroederNote that according to the Haskell syntax, Haskell function
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroederdeclarations and definitions need to start with the first column of
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\section{Development Graphs}\label{sec:DevGraph}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederDevelopment graphs are a simple kernel formalism for (heterogeneous)
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederstructured theorem proving and proof management.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederA development graph consists of a set of nodes (corresponding to whole
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederstructured specifications or parts thereof), and a set of arrows
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedercalled \emph{definition links}, indicating the dependency of each
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederinvolved structured specification on its subparts. Each node is
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederassociated with a signature and some set of local axioms. The axioms
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederof other nodes are inherited via definition links. Definition links
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederare usually drawn as black solid arrows, denoting an import of another
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederComplementary to definition links, which \emph{define} the theories of
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederrelated nodes, \emph{theorem links} serve for \emph{postulating}
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederrelations between different theories. Theorem links are the central
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederdata structure to represent proof obligations arising in formal
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederTheorem links can be \emph{global} (drawn as solid arrows) or
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\emph{local} (drawn as dashed arrows): a global theorem link
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederpostulates that all axioms of the source node (including the inherited
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederones) hold in the target node, while a local theorem link only postulates
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederthat the local axioms of the source node hold in the target node.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederBoth definition and theorem links can be \emph{homogeneous},
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederi.e. stay within the same logic, or \emph{heterogeneous}, i.e.\ %% such that
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederthe logic changes along the arrow. Technically, this is the case
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederfor Grothendieck signature morphisms $(\rho,\sigma)$ where
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder$\rho\not=id$. This case is indicated with double arrows.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederTheorem links are initially displayed in red.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederThe \emph{proof calculus} for development graphs
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\cite{MossakowskiEtAl05,Habil} is given by rules
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederthat allow for proving global theorem links by decomposing them
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederinto simpler (local and global) ones. Theorem links that have been
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederproved with this calculus are drawn in green. Local theorem links can
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederbe proved by turning them into \emph{local proof goals}. The latter
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedercan be discharged using a logic-specific calculus as given by an
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederentailment system for a specific institution. Open local
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederproof goals are indicated by marking the corresponding node in the
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederdevelopment graph as red; if all local implications are proved, the
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedernode is turned into green. This implementation ultimately is based
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederon a theorem \cite{Habil} stating soundness and relative completeness
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederof the proof calculus for heterogeneous development graphs.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederand in \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThe following options let \Hets show the development graph of
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedera specification library:
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{description}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[\texttt{-u}, \texttt{--uncolored}] no colors in shown graphs
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\end{description}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederThe following additional options also apply typical rules from the development
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroedergraph calculus to the final graph and save applying these rule via the GUI.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{description}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\item[\texttt{-A}, \texttt{--apply-automatic-rule}] apply the automatic
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder strategy to the development graph. This is what you usually want in order to
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder get goals within nodes for proving.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[\texttt{-N}, \texttt{--normal-form}] compute all normal forms for nodes
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder with incoming hiding links. (This may take long and may not be implemented
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder for all logics.)
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\end{description}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederLet us extend the above library \texttt{Order.casl}. One use of the
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederlibrary might be to express the fact that the natural numbers form a
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederstrict partial order as a view, as follows:
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{BIGEXAMPLE}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\end{BIGEXAMPLE}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\I\SPEC \NAMEDEFN{Natural\_Order\_2} =
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\IEXT{\NAMEREF{Natural}} \THEN
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\I\PRED \( \_\_<\_\_ : Nat \* Nat\)
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\(\[ \FORALL x,y:Nat \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \. 0 < suc(x) \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \. \neg x < 0 \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \. suc(x) < suc(y) \IFF x < y
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{EXAMPLE}%[\SLIDESMALL]
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\NAMEREF{Natural\_Order\_2} =
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\I{} \( Elem \MAPSTO Nat\)
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederAgain, these specifications can be checked with \Hets. However, this
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederonly checks syntactic and static semantic well-formedness -- it is
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederby a strict partial ordering relation. Checking this requires theorem
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederproving, which will be discussed below.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederHowever, before coming to theorem proving, let us first inspect the
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederproof obligations arising from a specification. This can be done with:
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder(assuming that the above two specifications and the view
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederhave been added to the file
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\Hets now displays a so-called development graph
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder(which is just an overview graph showing the overall structure
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederof the specifications in the library), see Fig.~\ref{fig:dg0}.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\includegraphics[scale=0.7]{dg-order-0}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\caption{Sample development graph.\label{fig:dg0}}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederNodes in a development graph correspond to \CASL specifications.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederArrows show how specifications are related by the structuring
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederThe black arrow denotes an ordinary import of
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederspecifications (generated by the extension), while the red arrow
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederdenotes a proof obligation (corresponding to the view).
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederThis proof obligation needs to be discharged in order to
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroedershow that the view is well-formed (then its color turns into green).
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederAs a more complex example, consider the following loose specification
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederof a sorting function, taken from the \CASL User Manual
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\cite{CASL-UM}, Chap.~6:
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{BIGEXAMPLE}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\I\SPEC \NAMEREF{List\_Order\_Sorted}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{ITEMS}[\WITHIN]
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{ITEMS}[\PRED]
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\I\PRED \( \_\_is\_sorted : List \)
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\(\[ \FORALL e,e': Elem; L : List \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \. empty~is\_sorted \\
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder \. cons(e,empty)~is\_sorted \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \. cons(e,cons(e',L))~is\_sorted \IFF
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{ITEMS}[\OP]
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\I\OP \( order : List \TOTAL List \)
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\end{BIGEXAMPLE}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederThe following specification of sorting by insertion also is taken from
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederthe \CASL User Manual \cite{CASL-UM}, Chap.~6:
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{BIGEXAMPLE}
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder\I\SPEC \NAMEREF{List\_Order}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{ITEMS}[\WITHIN]
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\begin{ITEMS}[\OP]
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\I\OP \( insert : Elem \* List \TOTAL List \)
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroeder\(\[ \FORALL e,e':Elem; L:List \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \. insert(e, empty) = cons(e, empty) \\
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroeder \. insert(e, cons(e',L)) = \[ cons(e', insert(e,L)) \WHEN e' < e\\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \ELSE cons(e, cons(e',L)) \] \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{ITEMS}[\OP]
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\I\OP \( order : List \TOTAL List \)
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\(\[ \FORALL e:Elem; L:List \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \. order(empty) = empty \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \. order(cons(e,L)) = insert(e, order(L)) \]\)
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\end{BIGEXAMPLE}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederBoth specifications are related. To see this, we first inspect
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroedertheir signatures. This is possible with:
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederassuming that \texttt{Sorting.casl} contains the above specifications.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\includegraphics[scale=0.7]{dg-order-1}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\caption{Development graph for the two sorting specifications.\label{fig:dg1}}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederIn the above-mentioned development graph, we have two types of nodes.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThe named ones correspond to named specifications, but there
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederare also unnamed nodes corresponding to anonymous basic
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederspecifications like the declaration of the $insert$ operation in
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\NAMEREF{List\_Order} above. Basically, there is an
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederunnamed node for each structured specification that is not named.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederAgain, the black arrows denote an ordinary import of specifications
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder(corresponding to the extensions and unions in the
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederspecifications), while the blue arrows denote hiding (corresponding to
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederthe local specification).
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederBy clicking on the nodes, one can inspect their signatures.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederIn this way, we can see that both \NAMEREF{List\_Order\_Sorted} and
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder\NAMEREF{List\_Order} have the same signature. Hence, it
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederis legal to add a view:
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\begin{EXAMPLE}%[\SLIDESMALL]
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\I\VIEW \NAMEDEFN{v2}[\NAMEREF{Total\_Order}] ~:~ \NAMEREF{List\_Order\_Sorted}[\NAMEREF{Total\_Order}] \TO
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\NAMEREF{List\_Order}[\NAMEREF{Total\_Order}]
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederWe have already added this view to \texttt{Sorting.casl}.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThe corresponding
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederproof obligation between \NAMEREF{List\_Order\_Sorted} and
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\NAMEREF{List\_Order} is displayed in Fig.~\ref{fig:dg1}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder as a red arrow.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederHere is a summary of the types of nodes and links occurring in
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederdevelopment graphs:
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\begin{description}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item[Named nodes] correspond to a named specification.
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder\item[Unnamed nodes] correspond to an anonymous specification.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item[Elliptic nodes] correspond to a specification in the current library.
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder\item[Rectangular nodes] are external nodes corresponding to a specification
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder downloaded from another library.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item[Red nodes] have open proof obligations.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Yellow nodes] have an open conservativity proof obligations.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Green nodes] have all proof obligations resolved.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item[Black links] correspond to reference to other specifications (definition
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder links in the sense of \cite[IV:4]{CASL/RefManual}).
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item[Red links] correspond to open proof obligations (theorem links).
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item[Green links] correspond to proven theorem links.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Yellow links] correspond to proven theorem links with open
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder conservativity or to open hiding theorem links.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item[Blue links] correspond to hiding, free, or cofree definition links.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item[Violett links] correspond to a mixture of links becoming visible after
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder ``expand'' or ``Show unnamed nodes with open proofs''.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Solid links] correspond to global (definition or theorem)
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederlinks in the sense of \cite[IV:4]{CASL/RefManual}.
\cite[IV:4]{CASL/RefManual}. These are usually created after
With the ``Hide/show internal node names'' option, the nodes that
With the ``Hide/show unnamed nodes without open proofs'' option, it is possible
been proven are removed from the graph. With the ``Hide/Show newly added
theorem links. It is possible to select/deselect all links or to invert the
i.e. have a model. The model finders currently interfaced are
Manual \cite{CASL/RefManual} or one of
origin of the node and the local theory i.e. axioms declared locally.
\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{omn} 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}.
\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 just a parsed library in XML.
The \texttt{tptp} format (\url{http://www.tptp.org}) is a standard
(i.e.\ \texttt{-d LogicGraph} lists the logics and comorphisms)
\url{http://pollux.informatik.uni-bremen.de:8000/}. It allows to browse the
and the slash of the URL, i.e.\
\url{http://localhost:8000/Basic/Numbers.casl}. Once a development has been
session id for a development graph that is given by a file name, i.e.\
\url{http://localhost:8000/Basic/Numbers.casl?session}. These session ids must
\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{-e ENCODING}, \texttt{--encoding=ENCODING}] Read input files using latin1 or utf8 encoding. The default is still latin1.
\item[\texttt{--relative-positions}] Just uses the relative library name in positions of warning or errors.
\item[\texttt{-U FILE}, \texttt{--xupdate=FILE}] update a development graph according to special xml update information (still experimental).
\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}