UserGuide.tex revision 1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\documentclass{article}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{alltt}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{casl}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{color}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\QUERY}[1]%{}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\eat}[1]{}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\IEXT}[1] {\\#1\I}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\newcommand{\IEND} {\I\END}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newenvironment{EXAMPLEFORMAT} {}{}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%% Added by MB to have some extra vertical space after the ``main'' examples
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%% following the points (and some others in the text):
dc89cfbc150be3b6792f559f57b6e91cd7affacbJonathan von Schroeder\newenvironment{BIGEXAMPLE} {\begin{EXAMPLE}} {\end{EXAMPLE}\medskip}
dc89cfbc150be3b6792f559f57b6e91cd7affacbJonathan von Schroeder\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}
85b227b458a885d075f3934c210c7de0cc89ccffJonathan 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}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\SLIDESMALL} {}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\SLIDESONLY}[1] {}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder% SIMULATING SMALL-CAPS FOR BOLD, EMPH
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%\newcommand {\CoFI}{CoFI\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeELAN} {\largeTEXTSC{E}{LAN}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\HOL}{\normalTEXTSC{H}{OL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\Isabelle}{\normalTEXTSC{I}{SABELLE}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%%%%% Klaus macros
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%%%%% end of Klaus macros
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LCF}{LCF\xspace}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\newcommand{\ASF}{ASF\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan 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}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
85b227b458a885d075f3934c210c7de0cc89ccffJonathan 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}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\begin{document}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\title{{\bf \protect{\LARGEHets} User Guide}\\
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder-- Version 0.7 --}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\author{Till Mossakowski, Christian Maeder, Klaus L\"{u}ttich\\[1em]
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederDFKI Lab Bremen, Bremen, Germany.\\[1em]
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederComments to: hets-users@informatik.uni-bremen.de
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\section{Introduction}
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederThe Heterogeneous Tool Set (\protect\Hets) is the main analysis tool
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederfor the specification language heterogeneous \CASL. Heterogeneous
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\CASL (\HetCASL) combines the specification language \CASL
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\cite{CASL-UM,CASL/RefManual} with \CASL extensions
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederand sublanguages, as well as completely different logics and even
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederprogramming languages such as Haskell. \HetCASL
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederextends the structuring mechanisms of \CASL:
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\emph{Basic specifications} are
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederunstructured specifications or modules written in a specific logic.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThe graph of currently supported logics and logic translations (the
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederlatter are also called comorphisms) is shown in
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederFig.~\ref{fig:LogicGraph}, and the degree of support by \Hets in
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederFig.~\ref{fig:Languages}.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederWith \emph{heterogeneous structured specifications}, it is possible to
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedercombine and rename specifications, hide parts thereof, and also
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedertranslate them to other logics. \emph{Architectural specifications}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederprescribe the structure of implementations. \emph{Specification
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder libraries} are collections of named structured and architectural
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\Hets consists of logic-specific tools for the parsing and static
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederanalysis of the different involved logics, as well as a
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederlogic-independent parsing and static analysis tool for structured and
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederarchitectural specifications and libraries. The latter of course needs
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederto call the logic-specific tools whenever a basic specification is
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\Hets is based on the theory of institutions \cite{GoguenBurstall92},
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederwhich formalize the notion of a logic. The theory behind \Hets is
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederlaid out in \cite{Habil}. A short overview is given in \cite{MossakowskiEA06}.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\section{Logics supported by Hets}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederThe following list of logics (formalized as so-called institutions
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan 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
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederellipse is filled with green, the more stable is the implementation of the logic. Blue indicates a prover-supported logic.}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\label{fig:LogicGraph}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{tabular}{|l|c|c|c|}\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederLanguage & Parser & Static Analysis & Prover \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\CASL & x & x & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\CoCASL & x & x & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\ModalCASL & x & x & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\HasCASL & x & x & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHaskell & x & x & -\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\CspCASL & (x) & - & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederConstraint\CASL & x & (x) & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%Structured specifications & x & x & (x) \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%Architectural specifications & x & x & -\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\CASLDL & x & - & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederOWL DL basic & x & (x) & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederOWL DL structure & x & (x) & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederPropositional & x & x & - \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederSoftFOL & - & - & x \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\Isabelle & - & - & x \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\caption{Current degree of \Hets support for the different languages.\label{fig:Languages}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{description}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan 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
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%Linguistic and Cognitive Engineering), an Upper Ontology for knowledge
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%representation. \cite{Gangemi:2002:SOD} Further it is now used to
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%specify calculi for time and space.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederFor more details on \CASL see \cite{CASL-RM,CASL-UM}.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederWe have implemented the \CASL logic in such a way that much of the
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederimplementation can be re-used for \CASL extensions as well; this
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederis achieved via ``holes'' (realized via polymorphic variables) in the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedertypes for signatures, morphisms, abstract syntax etc. This eases
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederintegration of \CASL extensions and keeps the effort of integrating
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\CASL extensions quite moderate.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item[CoCASL] \cite{MossakowskiEA04} is a coalgebraic extension of \CASL,
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedersuited for the specification of process types and reactive system.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThe central proof method is coinduction.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item[ModalCASL] \cite{ModalCASL}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder is an extension of \CASL with multi-modalities and
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederterm modalities. It allows the specification of modal systems with
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederKripke's possible worlds semantics. It is also possible to express
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedercertain forms of dynamic logic.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\item[HasCASL] is a higher order extension of \CASL allowing
a845310274d5bcd9da2df61599fd58eaf96ded13Jonathan von Schroeder polymorphic datatypes and functions. It is closely related to the
a845310274d5bcd9da2df61599fd58eaf96ded13Jonathan von Schroeder programming language Haskell and allows program constructs being
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder embedded in the specification.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederthe language is summarized in \cite{HasCASL/Summary}, the semantics
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederin \cite{Schroder05b,Schroder-habil}.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\item[Haskell] is a modern, pure and strongly typed functional
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder programming language. It simultaneously is the implementation
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder language of \Hets, such that in the future, \Hets might be applied
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederThe definitive reference for Haskell is \cite{PeytonJones03},
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\item[CspCASL] \cite{Roggenbach:2003:C-CN} is a combination of \CASL
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder with the process algebra CSP.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\item[ConstraintCASL] is an experimental logic for the specification
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederof qualitative constraint calculi.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\item[OWL DL] is the Web Ontology Language (OWL) recommended by the
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder World Wide Web Consortium (W3C, \texttt{http://www.w3c.org}). It is
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder used for knowledge representation and the Semantic Web
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder \cite{berners:2001:SWeb}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHets calls an external OWL DL parser
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder written in JAVA to obtain the abstract syntax for an OWL file and its
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder imports. The JAVA parser is also doing a first analysis classifying
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder the OWL ontology into the sublanguages OWL Full, OWL DL and OWL
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder Hets only supports the last two, more restricted variants.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder structuring of the OWL imports is displayed as Development Graph.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[CASL-DL] \cite{OWL-CASL-WADT2004}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederis an extension of a restriction of \CASL, realizing
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedera strongly typed variant of OWL DL in \CASL syntax.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \CASL with cardinality restrictions for the description of sorts and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder unary predicates. The restrictions are based on the equivalence
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder between \CASLDL, OWL~DL and \SHOIN. Compared to \CASL only unary
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder and binary predicates, predefined datatypes and concepts (subsorts
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder of the topsort Thing) are allowed. It is used to bring OWL DL and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \CASL closer together.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[Propositional] is classical propositional logic, which will
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederbe connected to SAT solvers in the near future.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[SoftFOL] \cite{LuettichEA06a} offers three automated theorem
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder proving systems (ATP) for first-order logic with equality: (1) SPASS
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \cite{WeidenbachEtAl02}; (2) Vampire \cite{RiazanovV02}; and (3)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder MathServ Broker\footnote{which chooses an appropriate ATP upon a
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder classification of the FOL problem} \cite{ZimmerAutexier06}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder These together comprise some of the most advanced theorem provers
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder for first-order logic.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover for higher-order
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\end{description}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederSoftFOL and \Isabelle are currently the only logics coming with a
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederprover. Proof support for the other logics can be obtained by using
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederlogic translations to a prover-supported logic.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederAn introduction to \CASL can be found in the \CASL User Manual
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\cite{CASL-UM}; the detailed language reference is given in
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederthe \CASL Reference Manual \cite{CASL/RefManual}. These documents
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederexplain both the \CASL logic and language of basic specifications as
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederwell as the logic-independent constructs for structured and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederarchitectural specifications. Corresponding documents explaining the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\HetCASL language constructs for \emph{heterogeneous} structured specifications
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederare forthcoming, until then, \cite{Mossakowski:2003:FHS} may serve as a short
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederintroduction. Moreover, the main heterogeneous constructs will be illustrated
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederin Sect.~\ref{sec:HetSpec} below.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\section{Logic translations supported
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\label{comorphisms}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe following list of logic translations (formalized as institution
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercomorphisms \cite{GoguenRosu02}) is currently supported by \Hets:
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{tabular}{|l|p{5cm}|}\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2CoCASL & inclusion \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2CspCASL & inclusion \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2HasCASL & inclusion \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2Modal & inclusion \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2PCFOL & coding of subsorting by injections, see Chap.\ III:3.1 of the CASL Reference Manual \cite{CASL/RefManual}\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2SubCFOL & coding of partial functions by error elements
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder(translation $(4a')$ of \cite{Mossakowski02}, but extended to subsorting) \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL2TopSort & coding of subsorting by a top sort and unary
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederpredicates for the subsorts \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCFOL2IsabelleHOL & coding of \CASL to Isabelle
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder(translation $(7)$ of \cite{Mossakowski02}) \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCoCASL2CoPCFOL & coding of subsorting by injections, similar to CASL2PCFOL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCoCASL2CoSubCFOL & coding of partial functions by error supersorts, similar to CASL2SubCFOL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCoCFOL2IsabelleHOL & coding of \CoCASL to Isabelle, similar to CFOL2IsabelleHOL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%CoPCFOL2CoCFOL & coding of partial functions by error elements,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%similar to PCFOL2CFOL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%%CspCASL2IsabelleHOL & \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%%CspCASL2Modal & \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHasCASL2HasCASL & coding of \HasCASL axiomatic recursive definitions
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederas \HasCASL recursive program definitions \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHasCASL2Haskell & translation of \HasCASL recursive program definitions to Haskell \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHasCASL2IsabelleHOL & coding of HasCASL to Isabelle/HOL \cite{Groening05} \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHaskell2IsabelleHOL & coding of Haskell to Isabelle/HOL \cite{TorriniEtAl07} \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHaskell2IsabelleHOLCF & coding of Haskell to Isabelle/HOLCF \cite{TorriniEtAl07}\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederModal2CASL & the standard translation of modal logic
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederto first-order logic \cite{blackburn_p-etal:2001a} \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%PCFOL2CFOL & coding of partial functions by error elements
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%(translation $(4a')$ of \cite{Mossakowski02}) \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederPCoClTyConsHOL2IsabelleHOL & coding of \HasCASL to Isabelle/HOL\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederSuleCFOL2SoftFOL & coding of CASL to SoftFOL \cite{LuettichEA06a},
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedermapping types to soft types \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederSuleCFOL2SoftFOLIndcuction & dto., but with instances of induction
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederaxioms for all proof goals\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederProp2CASL & inclusion \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederProp2CNF & conversion of propositional formulas to conjunctive normal form\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\section{Getting started}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe latest \Hets version can be obtained from the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\Hets tools home page
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder Since \Hets is being
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederimproved constantly, it is recommended always to use the latest version.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\Hets currently is available for Linux, Solaris and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThere are three possibilities to install \Hets:
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{enumerate}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe Java-based \Hets installer. Download a \texttt{.jar} file and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederjava -jar \texttt{file.jar}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederNote that you need Sun Java 1.4.2 or later. On a Mac, you can just
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdouble-click on the \texttt{.jar} file.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe installer will lead you through the installation with
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedera graphical interface. It will download and install further
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersoftware (if not already installed on your computer):
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{tabular}{|l|l|l|}\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCASL-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederuDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederTcl/Tk & graphics widget system & \url{http://www.scriptics.com/software/tcltk/} \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederSPASS & theorem prover & \texttt{http://spass.mpi-sb.mpg.de/}\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder(X)Emacs & editor (for Isabelle) & (must be installed manually)\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIf you do not have Sun Java, you can just download the hets binary.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederYou have to unpack it with \texttt{bunzip2} and then put it at
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersome place coverd by your \texttt{PATH}. You also have to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederinstall the above mentioned software and set
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederseveral environment variables, as explained on the installation page.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIf you want to compile \Hets from the sources, please follow the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederlink ``Hets: source code and information for developers''
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederon the \Hets web page, download the sources (as tarball or from
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercvs), and follow the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederinstructions in the \texttt{INSTALL} file.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\section{Analysis of Specifications}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederConsider the following \CASL
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{BIGEXAMPLE}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\I\SPEC \NAMEREF{Strict\_Partial\_Order} =
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\begin{ITEMS}[\PRED]
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\I\SORT \( Elem \)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder% \COMMENTENDLINE{\PRED abbreviates predicate}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\(\[ \FORALL x,y,z : Elem \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von SchroederNote that there may exist \(x, y\) such that\\
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroederneither \(x < y\) nor \(y < x\).
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\end{BIGEXAMPLE}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\Hets can be used for parsing and
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederchecking static well-formedness of specifications.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \index{parsing}%
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \index{static!analysis}%
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \index{analysis, static}%
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederLet us assume that the example is in a file named
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\texttt{Order.casl} (actually, this file is provided
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederwith the \Hets distribution).
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederThen you can check the well-formedness of the
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederspecification by typing (into some shell):
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\Hets checks both the correctness of this specification
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder with respect to the \CASL syntax, as
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederwell as its correctness with respect to the static semantics (e.g.\
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederwhether all identifiers have been declared before they are used,
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederwhether operators are applied to arguments of the correct sorts,
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederwhether the use of overloaded symbols is unambiguous, and so on).
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederThe following flags are available in this context:
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\begin{description}
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing -- the static analysis
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item[\texttt{-s}, \texttt{--just-structured}]
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederDo the parsing and the static analysis of (heterogeneous) structured
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederspecifications, but leave out the analysis of basic specifications.
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederThis can be used to quickly produce a development graph
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroedershowing the dependencies among the specifications (cf. Sect.~\ref{sec:DevGraph}).
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederUse \texttt{DIR} as the directory for specification libraries
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder(equivalently, you can set the variable \texttt{HETS\_LIB} before
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\item[\texttt{--casl-amalg=ANALYSIS}]
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder For the analysis of architectural specification (a quite advanced
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder amalgamability checking
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder algorithm for \CASL logic; it is a comma-separated list of zero or
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder more of the following options:
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \begin{description}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \item[\texttt{sharing}] perform sharing analysis for sorts,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder operations and predicates.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \item[\texttt{cell}] perform cell condition check; implies
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \texttt{sharing}. With this option on the subsort embeddings are
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \item[\texttt{colimit-thinness}] perform colimit thinness check;
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder implies \texttt{sharing}. The colimit thinness check is less
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder complete and usually takes longer than the full cell condition
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder check (\texttt{cell} option), but may prove more efficient in case
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder of certain specifications.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \end{description}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder If \texttt{ANALYSIS} is empty then amalgamability analysis for
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \CASL is skipped.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder The default value for \texttt{--casl-amalg} is
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\end{description}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\section{Heterogeneous Specification} \label{sec:HetSpec}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\Hets accepts plain text input files with the following endings:\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{tabular}{|l|c|c|}\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederEnding & default logic & structuring language\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\texttt{.casl} & \CASL & \CASL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\texttt{.het} & \CASL & \CASL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\texttt{.hs} & Haskell/HasSLe & Haskell\\\hline
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\texttt{.owl} & OWL DL, OWL Lite & OWL\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederAlthough the endings \texttt{.casl} and \texttt{.het} are
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederinterchangeable, the former should be used for libraries of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederhomogeneous \CASL specifications and the latter for \HetCASL libraries
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederof heterogeneous specifications (that use the \CASL structuring
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederconstructs). Within a \HetCASL library, the current logic can be changed e.g.\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederto \HasCASL in the following way:
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{verbatim}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe subsequent specifications are then parsed and analysed as
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\HasCASL specifications. Within such specifications,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederit is possible to use references to named \CASL specifications;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederthese are then automatically translated along the default
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederembedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder(There are also heterogeneous constructs
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederfor explicit translations between logics.)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederA \CspCASL specification consists of a \CASL specification
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederfor the data part and a \Csp process built over this data part.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederTherefore, \HetCASL provides a heterogeneous language construct
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\texttt{data} as follows:
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{verbatim}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder free type List[Elem] ::= nil | cons(Elem; List[Elem])
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder channel read, write : Elem
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder let Buf(l:List[Elem]) =
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder read?x -> Buf( cons(x,nil) )
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder [] if l=nil then STOP else write!last(l) -> Buf( rest(l) )
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederHere, the construct \texttt{data List} refers to the \CASL specification
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\texttt{List}, which is implicitly embedded into \CspCASL.
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederThe ending \texttt{.hs} is available for directly reading in
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederHaskell programs and HasSLe specifications,
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederand hence supports the Haskell module system.
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederthe logic Haskell has to be chosen explicitly, and the \CASL structuring
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroedersyntax needs to be used:
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\begin{verbatim}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederlibrary Factorial
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederspec Factorial =
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederfac :: Int -> Int
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederfac n = foldl (*) 1 [1..n]
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederNote that according to the Haskell syntax, Haskell function
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederdeclarations and definitions need to start with the first column of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\section{Development Graphs}\label{sec:DevGraph}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederDevelopment graphs are a simple kernel formalism for (heterogeneous)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederstructured theorem proving and proof management. A development graph
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederconsists of a set of nodes (corresponding to whole structured
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederspecifications or parts thereof), and a set of arrows called
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederdefinition links, indicating the dependency of each involved
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederstructured specification on its subparts. Arising proof obligations
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederare attached as so-called theorem links to this graph.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederand in \cite{Habil,MossakowskiEtAl05}.
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von SchroederThe following options let \Hets show the development graph of
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedera specification library:
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\begin{description}
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window.
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder\item[\texttt{-G}, \texttt{--only-gui}] Shows the development graph in a GUI window,
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroederand suppresses the writing of an output file.
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder\end{description}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederLet us extend the above library \texttt{Order.casl}. One use of the
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederlibrary might be to express the fact that the natural numbers form a
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederstrict partial order as a view, as follows:
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{BIGEXAMPLE}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\end{BIGEXAMPLE}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\I\SPEC \NAMEDEFN{Natural\_Order\_2} =
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\IEXT{\NAMEREF{Natural}} \THEN
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\I\PRED \( \_\_<\_\_ : Nat \* Nat\)
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\(\[ \FORALL x,y:Nat \\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \. 0 < suc(x) \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \. \neg x < 0 \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \. suc(x) < suc(y) \IFF x < y
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroeder\begin{EXAMPLE}%[\SLIDESMALL]
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroeder\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroeder\NAMEREF{Natural\_Order\_2} =
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroeder\I{} \( Elem \MAPSTO Nat\)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederAgain, these specifications can be checked with \Hets. However, this
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederonly checks syntactic and static semantic well-formedness -- it is
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
6df4343f46cc159371dfa671c5943354480f4e1cJonathan 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:
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder(assuming that the above two specifications and the view
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroederhave been added to the file
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder\Hets now displays a so-called development graph
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder(which is just an overview graph showing the overall structure
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan 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}}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederNodes in a development graph correspond to \CASL specifications.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederArrows show how specifications are related by the structuring
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan 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).
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan 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}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{ITEMS}[\WITHIN]
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{ITEMS}[\PRED]
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\I\PRED \( \_\_is\_sorted : List \)
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\(\[ \FORALL e,e': Elem; L : List \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \. empty~is\_sorted \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \. cons(e,empty)~is\_sorted \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \. cons(e,cons(e',L))~is\_sorted \IFF
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{ITEMS}[\OP]
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\I\OP \( order : List \TOTAL List \)
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan 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:
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{BIGEXAMPLE}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\I\SPEC \NAMEREF{List\_Order}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{ITEMS}[\WITHIN]
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{ITEMS}[\OP]
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\I\OP \( insert : Elem \* List \TOTAL List \)
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\(\[ \FORALL e,e':Elem; L:List \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \. insert(e, empty) = cons(e, empty) \\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \. insert(e, cons(e',L)) = \[ cons(e', insert(e,L)) \WHEN e' < e\\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \ELSE cons(e, cons(e',L)) \] \\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{ITEMS}[\OP]
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\I\OP \( order : List \TOTAL List \)
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder\(\[ \FORALL e:Elem; L:List \\
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder \. order(empty) = empty \\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \. order(cons(e,L)) = insert(e, order(L)) \]\)
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\end{BIGEXAMPLE}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederBoth specifications are related. To see this, we first inspect
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedertheir signatures. This is possible with:
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederassuming that \texttt{Sorting.casl} contains the above specifications.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan 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}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\caption{Development graph for the two sorting specifications.\label{fig:dg1}}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederIn the above-mentioned development graph, we have two types of nodes.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederThe named ones correspond to named specifications, but there
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederare also unnamed nodes corresponding to anonymous basic
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederspecifications like the declaration of the $insert$ operation in
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\NAMEREF{List\_Order} above. Basically, there is an
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan 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
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederspecifications), while the blue arrows denote hiding (corresponding to
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederthe local specification).
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederBy clicking on the nodes, one can inspect their signatures.
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von SchroederIn this way, we can see that both \NAMEREF{List\_Order\_Sorted} and
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\NAMEREF{List\_Order} have the same signature. Hence, it
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederis legal to add a view:
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{EXAMPLE}%[\SLIDESMALL]
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan 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}]
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan 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
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\NAMEREF{List\_Order} is displayed in Fig.~\ref{fig:dg1}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan 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:
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{description}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item[Named nodes] correspond to a named specification.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Unnamed nodes] correspond to an anonymous specification.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Elliptic nodes] correspond to a specification in the current library.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Rectangular nodes] are external nodes corresponding
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder to a specification downloaded from
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederanother library.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Red nodes] have open 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
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder(definition links in the sense of \cite[IV:4]{CASL/RefManual}).
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item[Blue links] correspond to hiding (hiding definition links).
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Red links] correspond to open proof obligations (theorem links).
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Green links] correspond to proved proof obligations (theorem links).
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Yellow links] correspond to open proof obligations involving hiding (hiding theorem links).
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Solid links] correspond to global (definition or theorem)
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederlinks in the sense of \cite[IV:4]{CASL/RefManual}.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Dashed links] correspond to local (definition or theorem) links in the sense of \cite[IV:4]{CASL/RefManual}.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Single links] have homogeneous signature morphisms (staying within
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederone and the same logic).
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Double links] have heterogeneous signature morphisms (moving between
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\end{description}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederWe now explain the menus of the development graph window.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederMost of the pull-down menus of the window are uDraw(Graph)-specific
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedertheir function can be looked up in the uDraw(Graph) documentation.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederThe exception is the Edit menu. Moreover, the nodes and links
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederof the graph have attached pop-up menus, which appear when
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederclicking with the right mouse button.
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder\begin{description}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Edit] This menu has the following submenus:
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{description}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Unnamed nodes]
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von SchroederThe ``Hide/show names'' menu is a toggle:
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederyou can switch on or off the display of names for nodes that
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederare initially unnamed. The newly named nodes get names that
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederare derived from named neighbour nodes.
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von SchroederWith the ``Hide nodes'' submenu, it is possible
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederto reduce the complexity of the graph by hiding all unnamed nodes;
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederonly nodes corresponding to named specifications remain displayed.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederPaths between named nodes going through unnamed nodes
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederare displayed as links. With the ``Show nodes'' submenu, the unnamed
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedernodes re-appear.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Proofs] This menu allows to apply some of the deduction rules
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder for development graphs, see Sect. IV:4.4 of the \CASL Reference
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder Manual \cite{CASL/RefManual}. While support for local and global
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder (definition or theorem) links is stable, support for hiding links
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder and checking conservativity is still experimental. In most cases, it is
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder advisable to use ``Automatic'', which automatically applies the
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder rules in the correct order. As a result, the the open theorem links
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder (marked in red) will be reduced to local proof goals, that is, they
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder become green, and instead, some of the node will get red, indicating
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder open local proof goals.
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroeder\item[Translate Graph] translates the whole development graph
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederalong a logic comorphism.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Show Logic Graph] shows the graph of logics and logic comorphisms
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedercurrently supported by \Hets.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Show Library Graph] shows the graph of libraries that have
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederbeen loaded into \Hets, and their dependencies. For library,
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederthe corresponding development graphs can be shown using its node menu.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederAlso, a list of specifications and views can be shown.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\end{description}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Pop-up menu for nodes]
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederHere, the number of submenus depends on the type of the node:
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{description}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Show signature] Shows the signature of the node.
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder\item[Show local axioms] Shows the local axioms of the node.
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder\item[Show theory] Shows the theory of the node (including axioms
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederimported from other nodes). Warning: axioms imported via hiding links
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederare not part of the theory; they can be made visible only by re-adding
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederthe hidden symbols, using the proof rule \emph{Theorem-Hide-Shift}.
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder\item[Translate theory] Translates the theory of a node to another logic.
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von SchroederA menu with the possible translation paths will be displayed.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Taxonomy graphs] (Only available for some logics) Shows the subsort graph of the signature of the node.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Show sublogic] Shows the logic and, within that logic, the minimal sublogic
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederfor the signature and the axioms of the node.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Show origin] Shows the kind of \CASL structuring construct that
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederled to the node.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Show proof status] Show open and proven local proof goals.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Prove] Try to prove the local proof goals. See Section~\ref{sec:Proofs}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Check consistency] Check the consistency of the theory of the node.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Show just subtree] (Only for named nodes) Reduce the complexity
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederof the graph by just showing the subtree below the current node.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Undo show just subtree] (Only for named nodes) Undo the reduction.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Show referenced library] (Only for external nodes) Open a new window
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedershowing the development graph for the library the external node refers to.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder%\item[Show spec] Show the structured specification of the node.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder% (not fully implemented yet)
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Show number of node] Show the internal number of the node.
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder\end{description}
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder\item[Pop-up menu for links]
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederAgain, the number of submenus depends on the type of the node:
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder\begin{description}
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder\item[Show morphism] Shows the signature morphism of the link. It consists
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroederof two components: a logic translation and a signature morphism in the
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroedertarget logic of the logic translation.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederIn the (most frequent) case
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederof an intra-logic signature morphism, the logic translation component is
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederjust the identity.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Show origin] Shows the kind of \CASL structuring construct that
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederled to the link.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Show proof status] (Only for theorem links) Show the proof status.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[Check conservativity] (Experimental) Check whether the
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedertheory of the target node of the link
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederis a conservative extension of the theory of the source node.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item[Show ID of this edge] Shows the internal number of the edge.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThese numbers are also used in the proof status information for
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\end{description}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\end{description}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\section{Reading, Writing and Formatting}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\Hets provides several options controlling the types of files
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederthat are read and written.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{description}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\item[\texttt{-i ITYPE}, \texttt{--input-type=ITYPE}] Specify
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\texttt{ITYPE} as the type of the input file. The default is
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\texttt{het} (\HetCASL plain text). \texttt{ast} is for reading
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederin abstract syntax trees in ATerm format, while \texttt{ast.baf}
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroederreads in the compressed ATerm format.
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von SchroederThe possible input types are:
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder\begin{verbatim}
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder (casl|het|owl|hs|ast[.baf]|[tree.]gen_trm[.baf])
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder\item[\texttt{-O DIR}, \texttt{--output-dir=DIR}]
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von SchroederSpecify \texttt{DIR} as destination directory for output files.
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder\item[\texttt{-o OTYPES}, \texttt{--output-types=OTYPES}]
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder\texttt{OTYPES} is a comma separated list of output types:
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder\begin{verbatim}
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder | pp.(het|tex|html)
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder | graph.(dot|ps|davinci)
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder | ast.(het|trm|taf|html|xml)
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder | (fdg|hdg|dg)[.nax].(het|trm|taf|html|xml)
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von SchroederThe default is \texttt{dg.taf}, which means that the development
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroedergraph of the library is stored in textual ATerm format (\texttt{taf}).
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von SchroederThis format can be read in when a library is downloaded from
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroederanother library, avoiding the need to re-analyse the downloaded library.
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von SchroederThe \texttt{pp} format is for pretty printing, either as plain text
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder(\texttt{het}), \LaTeX input (\texttt{tex}) or HTML (\texttt{html}).
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von SchroederA formatter with pretty-printed output currently is available only for
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroederthe \CASL logic. For example, it is possible to generate a pretty
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroederprinted \LaTeX\ version of \texttt{Order.casl} by typing:
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von SchroederThis will generate a file \texttt{Order.pp.tex}. It can be included
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroederinto \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroedercoming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty)}) is used.
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von SchroederWhen the \texttt{thy} format is selected, \Hets will try to translate
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroedereach specification in the library to \Isabelle, and write one \Isabelle
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder\texttt{.thy} file per specification.
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von SchroederWhen the \texttt{comptable.xml} format is selected, \Hets will extract
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederthe composition and inverse table of a Tarskian relation algebra from
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederspecification(s) (selected with the \texttt{-n} or \texttt{--spec}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederoption). It is assumed that the relation algebra is
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedergenerated by basic relations, and that the specification is written
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederin the \CASL logic. A sample specification of a relation
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederalgebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederavailable from \texttt{www.cofi.info/Libraries}.
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von SchroederThe output format is XML, the URL of the DTD is included in the
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[\texttt{-t TRANS}, \texttt{--translation=TRANS}]
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroederchooses a translation option. \texttt{TRANS} is a colon-separated list
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederwithout blanks of one or more comorphism names (see Sect.~\ref{comorphisms}).
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\item[\texttt{-r RAW} or \texttt{--raw=RAW}] This option allows one
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederto influence the formatting in more detail.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederHere, \texttt{RAW} is \texttt{(ascii|text|(la)?tex)=STRING},
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederand \texttt{STRING} is passed to the appropriate pretty-printer.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederThe details of these options are to be fixed in the future only.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThe other output formats are for future usage.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\end{description}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\section{Miscellaneous Options}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{description}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[\texttt{-v[Int]}, \texttt{--verbose[=Int]}]
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederSet the verbosity level according to \texttt{Int}. Default is 1.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[\texttt{-q}, \texttt{--quiet}]
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederBe quiet -- no diagnostic output at all. Overrides -v.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[\texttt{-V}, \texttt{--version}] Print version number and exit.
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroeder\item[\texttt{-h}, \texttt{--help}, \texttt{--usage}]
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederPrint usage information and exit.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\item[\texttt{+RTS -KIntM -RTS}] Increase the stack size to
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \texttt{Int} megabytes (needed in case of a stack overflow).
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederThis must be the first option.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\item[\texttt{-l LOGIC}, \texttt{--logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederdeclaration. The default is \CASL.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[\texttt{-n SPECS}, \texttt{--spec=SPECS}]
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederchooses a list of named specifications for processing
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\end{description}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\section{Proofs with Hets}\label{sec:Proofs}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThe graphical user interface (GUI) for calling a prover
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederis shown in Fig. \ref{fig:proof_window}. The list on the right
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedershows all goal names prefixed with the proof status in square
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederbrackets. A proved goal is indicated by a '+', a '-' indicates a
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederdisproved goal and a space denotes an open goal.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\includegraphics[width=\textwidth]{proofmanagement1}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\caption{Hets Goal and Prover Interface\label{fig:proof_window}}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederIf you open this GUI when processing the goals of one node for the first
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroedertime, it will show all goals as open. Within this list you can select
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederthose goals that should be inspected or proved. The button 'Display'
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroedershows the selected goals in the ASCII syntax of this theory's logic in
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedera separate window. With the 'Prove' button the actual prover is
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederlaunched. This is described in more detail in the following
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederparagraphs. By pressing the 'Show Proof Details' button a window is
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederopened where for each proved goal the used axioms are shown. The
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder'Status:' shows either 'No prover running' or 'Waiting for prover' in
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederblack or blue. If you press the 'Close' button the window is closed
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederand the status of the goals' list is integrated into the
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederdevelopment graph. If all goals have been proved, the selected node
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederturns from red into green.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederThe list 'Pick Theorem Prover:' lets you choose one of the connected
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederprovers (currently, these are SPASS and \Isabelle, described below). By
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederpressing 'Prove' the selected prover is launched and the theory along
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederwith the selected goals is translated via the shortest possible path
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederof comorphisms into the provers logic. The button 'More fine grained
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederselection...' lets you pick a (composed) comorphism in a separate
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederwindow from where the prover is launched then.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\subsection*{SPASS}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\includegraphics[width=\textwidth]{spassGUI1}
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder\caption{Interface of the SPASS prover\label{fig:SPASS_GUI}}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThe automatic theorem prover SPASS
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\cite{WeidenbachEtAl02} is a resolution-based prover for first-order logic
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederIf you have chosen SPASS, initially, all selected goals are tried in a
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederrow. After this so called batch mode the results are displayed in a
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederwindow which is shown in Fig. \ref{fig:SPASS_GUI}. This GUI for the
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedertheorem prover SPASS is very similar to the 'Select Goal(s) and
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederProve' GUI which lets you choose a prover for some goals. But with the
383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von SchroederSPASS GUI, the actual SPASS prover is launched with the selected
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroedergoal. Further it is possible to set a time-limit and some options for
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederSPASS. The available options are shown in separate window by pressing
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederthe 'Help' button. The status of the selected goal is shown in the
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder'Status:' line with either 'Proved', 'Disproved', 'Open' or 'Open Time
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder(Time is up!)'. If a goal has been proved the labels of the used
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederaxioms are shown in the list on the right. The button 'Show Details'
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedershows the whole output of SPASS. 'Save Prover Configuration allows you
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederto save the configuration and status of each proof for
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederdocumentation. By pressing the button 'Exit Prover' the status of
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroederthese proofs and goals is transferred back to the main 'Select Goal(s)
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroederand Prove' window.
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroeder\subsection*{Isabelle}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\Isabelle \cite{NipPauWen02} is an interactive theorem prover, which is
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroedermore powerful than SPASS, but also requires more user interaction.
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroederhas a very small core guaranteeing correctness, and its provers,
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederlike the simplifier or the tableaux prover, are built on top of this
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedercore. Furthermore, there is over fifteen years of experience with it,
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederand several mathematical textbooks have been partially
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \index{formal!verification}%
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\Isabelle is a tactic based theorem prover implemented in standard ML.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederThe main \Isabelle logic (called Pure) is some weak intuitionistic type
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedertheory with polymorphism. The logic Pure is used to represent a
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedervariety of logics within \Isabelle; one of them being \HOL (higher-order
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederlogic). For example, logical implication in Pure (written
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\texttt{==>}, also called meta-implication), is different from logical
c2356bf325a50171577ca2ffb33cf83bcd0786b1Jonathan von Schroederimplication in \HOL (written \texttt{-->}, also called object
c2356bf325a50171577ca2ffb33cf83bcd0786b1Jonathan von SchroederIt is essential to be aware of the fact that the \Isabelle/\HOL logic
c2356bf325a50171577ca2ffb33cf83bcd0786b1Jonathan von Schroederis different from the logics that are encoded into it via comorphisms.
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroederTherefore, the formulas appearing in subgoals of proofs with \Isabelle
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederwill not conform to the syntax of the original input logic. They may
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroedereven use features of \Isabelle/\HOL such as higher-order functions
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederthat are not present in an input logic like \CASL.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\Isabelle is started with ProofGeneral
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\cite{DBLP:conf/tacas/Aspinall00,url:ProofGeneral} in a separate Emacs
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\cite{url:Emacs,url:XEmacs}.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederThe \Isabelle theory file conforms to the Isabelle/Isar syntax
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\cite{NipPauWen02}. It starts with the theory (encoded along the selected
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder comorphism), followed by a list of theorems. Initially, all the
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder theorems have trivial proofs, using the `oops` command. However, if
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder you have saved earlier proof attempts, \Hets will patch these into
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder the generated \Isabelle theory file, ensuring that your previous work
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder is not lost. (But note that this patching can only be successful
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder if you do not rename specifications, or change their structure.) You
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder now can replace the 'oops' commands with real \Isabelle proofs, and
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder use Proof General to step through the proofs. You finish your session
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder by saving your file (using the Emacs file menu, or the Ctrl-x Ctrl-s
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder key sequence), and pressing a button in a small pop-up window
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder generated by \Hets.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\section{Limits of Hets}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\Hets is still intensively under development. In particular, the
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederfollowing points are still missing:
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item There is no proof support for architectural specifications.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item Distributed libraries are always downloaded from the local disk,
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedernot from the Internet.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item Version numbers of libraries are not considered properly.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item The proof engine for development graphs provides only experimental
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedersupport for hiding links and for conservativity.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\section{Architecture of Hets}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\Hets is written in Haskell. Its parser uses combinator
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \index{parsing}%
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThe user-defined (also known as ``mixfix'') syntax of \CASL
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedercalls for a two-pass approach. In the first pass, the skeleton of a
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\CASL abstract syntax tree is derived, in order to extract user-defined
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedersyntax rules. In a second pass, which is performed during
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederanalysis, these syntax rules are used to parse
8c4e6fae99499cb457b3b38bf248c30ce2f95921Jonathan von Schroederany expressions that
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederuse mixfix notation. The output is stored in the so-called
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \index{ATerms}%
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederATerm format \cite{BJKO00}, which is used as interchange format
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederfor interfacing with other tools.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\Hets provides an abstract interface for
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder \index{institution!independence}%
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \index{independence, institution}%
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederinstitutions, so
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederthat new logics can be integrated smoothly.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederIn order to do so, a parser,
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroedera static checker and a prover for basic specifications in the logic have
%\input{hets.tex}