UserGuide.tex revision 7a8592051724fa46499bde120f44cdc8db270876
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\documentclass{article}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{alltt}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{casl}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{color}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\QUERY}[1]%{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\eat}[1]{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\IEXT}[1] {\\#1\I}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\IEND} {\I\END}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{EXAMPLEFORMAT} {}{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%% Added by MB to have some extra vertical space after the ``main'' examples
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%% following the points (and some others in the text):
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{BIGEXAMPLE} {\begin{EXAMPLE}} {\end{EXAMPLE}\medskip}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{DETAILSFORMAT} {}{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{META}[1][] {#1\begin{METAFORMAT}}{\end{METAFORMAT}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{METAFORMAT} {\medskip\vrule\hspace{1ex}\vrule\hspace{1ex}%
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \begin{minipage}{0.9\textwidth}\it}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski {\end{minipage}\par\medskip}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\SLIDESMALL} {}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\SLIDESONLY}[1] {}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% SIMULATING SMALL-CAPS FOR BOLD, EMPH
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%\newcommand {\CoFI}{CoFI\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeELAN} {\largeTEXTSC{E}{LAN}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HOL}{\normalTEXTSC{H}{OL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Isabelle}{\normalTEXTSC{I}{SABELLE}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%%%%% Klaus macros
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%%%%% end of Klaus macros
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LCF}{LCF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\ASF}{ASF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SDF}{SDF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski%% Do NOT use \ASF+\SDF (it gives a superfluous space in the middle)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CCC}{CCC\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CoCASL}{\normalTEXTSC{C}{O}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CspCASL}{\normalTEXTSC{C}{SP}-\normalTEXTSC{C}{ASL}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{document}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\title{{\bf \protect{\LARGEHets} User Guide}\\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski-- Version 0.7 --}
e91e02579a34e005734059ad09e0d1d1304a03e0Till Mossakowski\author{Till Mossakowski, Christian Maeder, Klaus L\"{u}ttich\\[1em]
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiDFKI Lab Bremen, Bremen, Germany.\\[1em]
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiComments to: hets-users@informatik.uni-bremen.de
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Introduction}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe Heterogeneous Tool Set (\protect\Hets) is the main analysis tool
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor the specification language heterogeneous \CASL. Heterogeneous
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\CASL (\HetCASL) combines the specification language \CASL
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\cite{CASL-UM,CASL/RefManual} with \CASL extensions
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowskiand sublanguages, as well as completely different logics and even
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiprogramming languages such as Haskell. \HetCASL
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowskiextends the structuring mechanisms of \CASL:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{Basic specifications} are
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiunstructured specifications or modules written in a specific logic.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe graph of currently supported logics and logic translations (the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskilatter are also called comorphisms) is shown in
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiFig.~\ref{fig:LogicGraph}, and the degree of support by \Hets in
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiFig.~\ref{fig:Languages}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWith \emph{heterogeneous structured specifications}, it is possible to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicombine and rename specifications, hide parts thereof, and also
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitranslate them to other logics. \emph{Architectural specifications}
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowskiprescribe the structure of implementations. \emph{Specification
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski libraries} are collections of named structured and architectural
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets consists of logic-specific tools for the parsing and static
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskianalysis of the different involved logics, as well as a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogic-independent parsing and static analysis tool for structured and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiarchitectural specifications and libraries. The latter of course needs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito call the logic-specific tools whenever a basic specification is
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\Hets is based on the theory of institutions \cite{GoguenBurstall92},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiwhich formalize the notion of a logic. The theory behind \Hets is
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskilaid out in \cite{Habil}. A short overview is given in \cite{MossakowskiEA06}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\section{Logics supported by Hets}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThe following list of logics (formalized as so-called institutions
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\cite{GoguenBurstall92}) is currently supported by \Hets:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \begin{center}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \includegraphics[scale=0.4]{LogicGraph}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\caption{Graph of logics currently supported by \Hets. The more an
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiellipse is filled with green, the more stable is the implementation of the logic. Blue indicates a prover-supported logic.}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\label{fig:LogicGraph}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{figure}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{center}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{tabular}{|l|c|c|c|}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiLanguage & Parser & Static Analysis & Prover \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CASL & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CoCASL & x & x & - \\\hline
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski\ModalCASL & x & x & - \\\hline
881ab7022a03f9a6fa697d3067d05d61844929cbChristian Maeder\HasCASL & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiHaskell & x & x & -\\\hline
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\CspCASL & (x) & - & - \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiConstraint\CASL & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Structured specifications & x & x & (x) \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Architectural specifications & x & x & -\\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CASLDL & x & - & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiOWL DL basic & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiOWL DL structure & x & (x) & - \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiPropositional & x & x & - \\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiSoftFOL & - & - & x \\\hline
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\Isabelle & - & - & x \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\caption{Current degree of \Hets support for the different languages.\label{fig:Languages}}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{description}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[CASL] extends many sorted first-order logic with partial
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski functions and subsorting. It also provides induction sentences,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski expressing the (free) generation of datatypes.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%It is mainly designed and used for the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%specification of requirements for software systems. But it is also
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%used for the specification of \Dolce (Descriptive Ontology for
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Linguistic and Cognitive Engineering), an Upper Ontology for knowledge
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%representation. \cite{Gangemi:2002:SOD} Further it is now used to
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%specify calculi for time and space.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiFor more details on \CASL see \cite{CASL-RM,CASL-UM}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiWe have implemented the \CASL logic in such a way that much of the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiimplementation can be re-used for \CASL extensions as well; this
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiis achieved via ``holes'' (realized via polymorphic variables) in the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskitypes for signatures, morphisms, abstract syntax etc. This eases
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiintegration of \CASL extensions and keeps the effort of integrating
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CASL extensions quite moderate.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[CoCASL] \cite{MossakowskiEA04} is a coalgebraic extension of \CASL,
7a8592051724fa46499bde120f44cdc8db270876Till Mossakowskisuited for the specification of process types and reactive systems.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe central proof method is coinduction.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[ModalCASL] \cite{ModalCASL}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski is an extension of \CASL with multi-modalities and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiterm modalities. It allows the specification of modal systems with
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiKripke's possible worlds semantics. It is also possible to express
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicertain forms of dynamic logic.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[HasCASL] is a higher order extension of \CASL allowing
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski polymorphic datatypes and functions. It is closely related to the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski programming language Haskell and allows program constructs being
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski embedded in the specification.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskithe language is summarized in \cite{HasCASL/Summary}, the semantics
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiin \cite{Schroder05b,Schroder-habil}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[Haskell] is a modern, pure and strongly typed functional
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski programming language. It simultaneously is the implementation
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski language of \Hets, such that in the future, \Hets might be applied
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe definitive reference for Haskell is \cite{PeytonJones03},
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[CspCASL] \cite{Roggenbach:2003:C-CN} is a combination of \CASL
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski with the process algebra CSP.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[ConstraintCASL] is an experimental logic for the specification
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiof qualitative constraint calculi.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[OWL DL] is the Web Ontology Language (OWL) recommended by the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski World Wide Web Consortium (W3C, \texttt{http://www.w3c.org}). It is
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski used for knowledge representation and the Semantic Web
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \cite{berners:2001:SWeb}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiHets calls an external OWL DL parser
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski written in JAVA to obtain the abstract syntax for an OWL file and its
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski imports. The JAVA parser is also doing a first analysis classifying
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski the OWL ontology into the sublanguages OWL Full, OWL DL and OWL
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Hets only supports the last two, more restricted variants.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski structuring of the OWL imports is displayed as Development Graph.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[CASL-DL] \cite{OWL-CASL-WADT2004}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiis an extension of a restriction of \CASL, realizing
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskia strongly typed variant of OWL DL in \CASL syntax.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \CASL with cardinality restrictions for the description of sorts and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski unary predicates. The restrictions are based on the equivalence
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski between \CASLDL, OWL~DL and \SHOIN. Compared to \CASL only unary
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski and binary predicates, predefined datatypes and concepts (subsorts
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski of the topsort Thing) are allowed. It is used to bring OWL DL and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \CASL closer together.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[Propositional] is classical propositional logic, which will
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskibe connected to SAT solvers in the near future.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[SoftFOL] \cite{LuettichEA06a} offers three automated theorem
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski proving systems (ATP) for first-order logic with equality: (1) SPASS
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \cite{WeidenbachEtAl02}; (2) Vampire \cite{RiazanovV02}; and (3)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski MathServ Broker\footnote{which chooses an appropriate ATP upon a
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski classification of the FOL problem} \cite{ZimmerAutexier06}.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski These together comprise some of the most advanced theorem provers
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski for first-order logic.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover for higher-order
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\end{description}
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiSoftFOL and \Isabelle are currently the only logics coming with a
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiprover. Proof support for the other logics can be obtained by using
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskilogic translations to a prover-supported logic.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiAn introduction to \CASL can be found in the \CASL User Manual
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski\cite{CASL-UM}; the detailed language reference is given in
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithe \CASL Reference Manual \cite{CASL/RefManual}. These documents
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiexplain both the \CASL logic and language of basic specifications as
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiwell as the logic-independent constructs for structured and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiarchitectural specifications. Corresponding documents explaining the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\HetCASL language constructs for \emph{heterogeneous} structured specifications
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiare forthcoming, until then, \cite{Mossakowski:2003:FHS} may serve as a short
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiintroduction. Moreover, the main heterogeneous constructs will be illustrated
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiin Sect.~\ref{sec:HetSpec} below.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\section{Logic translations supported
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\label{comorphisms}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThe following list of logic translations (formalized as institution
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskicomorphisms \cite{GoguenRosu02}) is currently supported by \Hets:
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{tabular}{|l|p{5cm}|}\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2CoCASL & inclusion \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2CspCASL & inclusion \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2HasCASL & inclusion \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2Modal & inclusion \\\hline
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskiCASL2PCFOL & coding of subsorting by injections, see Chap.\ III:3.1 of the CASL Reference Manual \cite{CASL/RefManual}\\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2SubCFOL & coding of partial functions by error elements
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski(translation $(4a')$ of \cite{Mossakowski02}, but extended to subsorting) \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2TopSort & coding of subsorting by a top sort and unary
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskipredicates for the subsorts \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCFOL2IsabelleHOL & coding of \CASL to Isabelle
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski(translation $(7)$ of \cite{Mossakowski02}) \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCoCASL2CoPCFOL & coding of subsorting by injections, similar to CASL2PCFOL \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCoCASL2CoSubCFOL & coding of partial functions by error supersorts, similar to CASL2SubCFOL \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCoCFOL2IsabelleHOL & coding of \CoCASL to Isabelle, similar to CFOL2IsabelleHOL \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%CoPCFOL2CoCFOL & coding of partial functions by error elements,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%similar to PCFOL2CFOL \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%%CspCASL2IsabelleHOL & \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%%CspCASL2Modal & \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiHasCASL2HasCASL & coding of \HasCASL axiomatic recursive definitions
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskias \HasCASL recursive program definitions \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiHasCASL2Haskell & translation of \HasCASL recursive program definitions to Haskell \\\hline
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskiHasCASL2IsabelleHOL & coding of HasCASL to Isabelle/HOL \cite{Groening05} \\\hline
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskiHaskell2IsabelleHOL & coding of Haskell to Isabelle/HOL \cite{TorriniEtAl07} \\\hline
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskiHaskell2IsabelleHOLCF & coding of Haskell to Isabelle/HOLCF \cite{TorriniEtAl07}\\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiModal2CASL & the standard translation of modal logic
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskito first-order logic \cite{blackburn_p-etal:2001a} \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%PCFOL2CFOL & coding of partial functions by error elements
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%(translation $(4a')$ of \cite{Mossakowski02}) \\\hline
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskiPCoClTyConsHOL2IsabelleHOL & coding of \HasCASL to Isabelle/HOL\\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiSuleCFOL2SoftFOL & coding of CASL to SoftFOL \cite{LuettichEA06a},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskimapping types to soft types \\\hline
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskiSuleCFOL2SoftFOLIndcuction & dto., but with instances of induction
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowskiaxioms for all proof goals\\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiProp2CASL & inclusion \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiProp2CNF & conversion of propositional formulas to conjunctive normal form\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Getting started}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe latest \Hets version can be obtained from the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\Hets tools home page
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski Since \Hets is being
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiimproved constantly, it is recommended always to use the latest version.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets currently is available for Linux, Solaris and
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiThere are three possibilities to install \Hets:
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\begin{enumerate}
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiThe Java-based \Hets installer. Download a \texttt{.jar} file and
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskijava -jar \texttt{file.jar}
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiNote that you need Sun Java 1.4.2 or later. On a Mac, you can just
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskidouble-click on the \texttt{.jar} file.
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiThe installer will lead you through the installation with
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskia graphical interface. It will download and install further
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskisoftware (if not already installed on your computer):
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\begin{tabular}{|l|l|l|}\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCASL-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
c5e63ec138b908ac9d15e6843120033bf36a1862Till MossakowskiuDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiTcl/Tk & graphics widget system & \url{http://www.scriptics.com/software/tcltk/} \\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiSPASS & theorem prover & \texttt{http://spass.mpi-sb.mpg.de/}\\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski(X)Emacs & editor (for Isabelle) & (must be installed manually)\\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiIf you do not have Sun Java, you can just download the hets binary.
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiYou have to unpack it with \texttt{bunzip2} and then put it at
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskisome place coverd by your \texttt{PATH}. You also have to
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskiinstall the above mentioned software and set
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskiseveral environment variables, as explained on the installation page.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiIf you want to compile \Hets from the sources, please follow the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskilink ``Hets: source code and information for developers''
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskion the \Hets web page, download the sources (as tarball or from
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicvs), and follow the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiinstructions in the \texttt{INSTALL} file.
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\end{enumerate}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Analysis of Specifications}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiConsider the following \CASL
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecification:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{Strict\_Partial\_Order} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\PRED]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SORT \( Elem \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% \COMMENTENDLINE{\PRED abbreviates predicate}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL x,y,z : Elem \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{COMMENT}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiNote that there may exist \(x, y\) such that\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskineither \(x < y\) nor \(y < x\).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets can be used for parsing and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskichecking static well-formedness of specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{parsing}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{static!analysis}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{analysis, static}%
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiLet us assume that the example is in a file named
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{Order.casl} (actually, this file is provided
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiwith the \Hets distribution).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThen you can check the well-formedness of the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispecification by typing (into some shell):
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets checks both the correctness of this specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski with respect to the \CASL syntax, as
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwell as its correctness with respect to the static semantics (e.g.\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhether all identifiers have been declared before they are used,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhether operators are applied to arguments of the correct sorts,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhether the use of overloaded symbols is unambiguous, and so on).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe following flags are available in this context:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing -- the static analysis
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-s}, \texttt{--just-structured}]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiDo the parsing and the static analysis of (heterogeneous) structured
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecifications, but leave out the analysis of basic specifications.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThis can be used to quickly produce a development graph
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskishowing the dependencies among the specifications (cf. Sect.~\ref{sec:DevGraph}).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiUse \texttt{DIR} as the directory for specification libraries
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(equivalently, you can set the variable \texttt{HETS\_LIB} before
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskicalling \Hets).
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\item[\texttt{--casl-amalg=ANALYSIS}]
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski For the analysis of architectural specification (a quite advanced
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski amalgamability checking
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski algorithm for \CASL logic; it is a comma-separated list of zero or
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski more of the following options:
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \begin{description}
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \item[\texttt{sharing}] perform sharing analysis for sorts,
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski operations and predicates.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \item[\texttt{cell}] perform cell condition check; implies
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \texttt{sharing}. With this option on the subsort embeddings are
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \item[\texttt{colimit-thinness}] perform colimit thinness check;
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski implies \texttt{sharing}. The colimit thinness check is less
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski complete and usually takes longer than the full cell condition
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski check (\texttt{cell} option), but may prove more efficient in case
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski of certain specifications.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \end{description}
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski If \texttt{ANALYSIS} is empty then amalgamability analysis for
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \CASL is skipped.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski The default value for \texttt{--casl-amalg} is
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \texttt{cell}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Heterogeneous Specification} \label{sec:HetSpec}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Hets accepts plain text input files with the following endings:\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{tabular}{|l|c|c|}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiEnding & default logic & structuring language\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.casl} & \CASL & \CASL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.het} & \CASL & \CASL \\\hline
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill Mossakowski\texttt{.hs} & Haskell/HasSLe & Haskell\\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\texttt{.owl} & OWL DL, OWL Lite & OWL\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiAlthough the endings \texttt{.casl} and \texttt{.het} are
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinterchangeable, the former should be used for libraries of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskihomogeneous \CASL specifications and the latter for \HetCASL libraries
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiof heterogeneous specifications (that use the \CASL structuring
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiconstructs). Within a \HetCASL library, the current logic can be changed e.g.\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskito \HasCASL in the following way:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe subsequent specifications are then parsed and analysed as
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\HasCASL specifications. Within such specifications,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiit is possible to use references to named \CASL specifications;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithese are then automatically translated along the default
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiembedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski(There are also heterogeneous constructs
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskifor explicit translations between logics.)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiA \CspCASL specification consists of a \CASL specification
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifor the data part and a \Csp process built over this data part.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiTherefore, \HetCASL provides a heterogeneous language construct
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{data} as follows:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilibrary Buffer
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski free type List[Elem] ::= nil | cons(Elem; List[Elem])
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski channel read, write : Elem
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski let Buf(l:List[Elem]) =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski read?x -> Buf( cons(x,nil) )
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski [] if l=nil then STOP else write!last(l) -> Buf( rest(l) )
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHere, the construct \texttt{data List} refers to the \CASL specification
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{List}, which is implicitly embedded into \CspCASL.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe ending \texttt{.hs} is available for directly reading in
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill MossakowskiHaskell programs and HasSLe specifications,
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill Mossakowskiand hence supports the Haskell module system.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithe logic Haskell has to be chosen explicitly, and the \CASL structuring
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisyntax needs to be used:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilibrary Factorial
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispec Factorial =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifac :: Int -> Int
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifac n = foldl (*) 1 [1..n]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiNote that according to the Haskell syntax, Haskell function
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskideclarations and definitions need to start with the first column of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Development Graphs}\label{sec:DevGraph}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDevelopment graphs are a simple kernel formalism for (heterogeneous)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskistructured theorem proving and proof management. A development graph
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiconsists of a set of nodes (corresponding to whole structured
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecifications or parts thereof), and a set of arrows called
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidefinition links, indicating the dependency of each involved
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskistructured specification on its subparts. Arising proof obligations
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiare attached as so-called theorem links to this graph.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiand in \cite{Habil,MossakowskiEtAl05}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe following options let \Hets show the development graph of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskia specification library:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-G}, \texttt{--only-gui}] Shows the development graph in a GUI window,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiand suppresses the writing of an output file.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiLet us extend the above library \texttt{Order.casl}. One use of the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilibrary might be to express the fact that the natural numbers form a
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskistrict partial order as a view, as follows:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{EXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEDEFN{Natural\_Order\_2} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{Natural}} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\PRED \( \_\_<\_\_ : Nat \* Nat\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL x,y:Nat \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. 0 < suc(x) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. \neg x < 0 \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. suc(x) < suc(y) \IFF x < y
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{EXAMPLE}%[\SLIDESMALL]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{Natural\_Order\_2} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I{} \( Elem \MAPSTO Nat\)
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAgain, these specifications can be checked with \Hets. However, this
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskionly checks syntactic and static semantic well-formedness -- it is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiby a strict partial ordering relation. Checking this requires theorem
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproving, which will be discussed below.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHowever, before coming to theorem proving, let us first inspect the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof obligations arising from a specification. This can be done with:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{hets -g Order.casl}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(assuming that the above two specifications and the view
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskihave been added to the file
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets now displays a so-called development graph
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(which is just an overview graph showing the overall structure
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof the specifications in the library), see Fig.~\ref{fig:dg0}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{center}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\includegraphics[scale=0.7]{dg-order-0}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Sample development graph.\label{fig:dg0}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiNodes in a development graph correspond to \CASL specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiArrows show how specifications are related by the structuring
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe black arrow denotes an ordinary import of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecifications (generated by the extension), while the red arrow
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidenotes a proof obligation (corresponding to the view).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThis proof obligation needs to be discharged in order to
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskishow that the view is well-formed (then its color turns into green).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAs a more complex example, consider the following loose specification
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof a sorting function, taken from the \CASL User Manual
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski\cite{CASL-UM}, Chap.~6:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{List\_Order\_Sorted}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\WITHIN]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\PRED]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\PRED \( \_\_is\_sorted : List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL e,e': Elem; L : List \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. empty~is\_sorted \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. cons(e,empty)~is\_sorted \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. cons(e,cons(e',L))~is\_sorted \IFF
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\OP \( order : List \TOTAL List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following specification of sorting by insertion also is taken from
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowskithe \CASL User Manual \cite{CASL-UM}, Chap.~6:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{List\_Order}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\phantomsection
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\WITHIN]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\OP \( insert : Elem \* List \TOTAL List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL e,e':Elem; L:List \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. insert(e, empty) = cons(e, empty) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. insert(e, cons(e',L)) = \[ cons(e', insert(e,L)) \WHEN e' < e\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ELSE cons(e, cons(e',L)) \] \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\OP \( order : List \TOTAL List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL e:Elem; L:List \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. order(empty) = empty \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. order(cons(e,L)) = insert(e, order(L)) \]\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBoth specifications are related. To see this, we first inspect
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitheir signatures. This is possible with:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{hets -g Sorting.casl}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiassuming that \texttt{Sorting.casl} contains the above specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{center}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\includegraphics[scale=0.7]{dg-order-1}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Development graph for the two sorting specifications.\label{fig:dg1}}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn the above-mentioned development graph, we have two types of nodes.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe named ones correspond to named specifications, but there
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiare also unnamed nodes corresponding to anonymous basic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispecifications like the declaration of the $insert$ operation in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order} above. Basically, there is an
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiunnamed node for each structured specification that is not named.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAgain, the black arrows denote an ordinary import of specifications
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(corresponding to the extensions and unions in the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecifications), while the blue arrows denote hiding (corresponding to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe local specification).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBy clicking on the nodes, one can inspect their signatures.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn this way, we can see that both \NAMEREF{List\_Order\_Sorted} and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order} have the same signature. Hence, it
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis legal to add a view:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{EXAMPLE}%[\SLIDESMALL]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\VIEW \NAMEDEFN{v2}[\NAMEREF{Total\_Order}] ~:~ \NAMEREF{List\_Order\_Sorted}[\NAMEREF{Total\_Order}] \TO
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order}[\NAMEREF{Total\_Order}]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWe have already added this view to \texttt{Sorting.casl}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe corresponding
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof obligation between \NAMEREF{List\_Order\_Sorted} and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order} is displayed in Fig.~\ref{fig:dg1}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski as a red arrow.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHere is a summary of the types of nodes and links occurring in
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidevelopment graphs:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Named nodes] correspond to a named specification.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Unnamed nodes] correspond to an anonymous specification.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Elliptic nodes] correspond to a specification in the current library.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Rectangular nodes] are external nodes corresponding
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski to a specification downloaded from
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskianother library.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Red nodes] have open proof obligations.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Green nodes] have all proof obligations resolved.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Black links] correspond to reference to other specifications
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(definition links in the sense of \cite[IV:4]{CASL/RefManual}).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Blue links] correspond to hiding (hiding definition links).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Red links] correspond to open proof obligations (theorem links).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Green links] correspond to proved proof obligations (theorem links).
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Yellow links] correspond to open proof obligations involving hiding (hiding theorem links).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Solid links] correspond to global (definition or theorem)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilinks in the sense of \cite[IV:4]{CASL/RefManual}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Dashed links] correspond to local (definition or theorem) links in the sense of \cite[IV:4]{CASL/RefManual}.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Single links] have homogeneous signature morphisms (staying within
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskione and the same logic).
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Double links] have heterogeneous signature morphisms (moving between
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiWe now explain the menus of the development graph window.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiMost of the pull-down menus of the window are uDraw(Graph)-specific
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskitheir function can be looked up in the uDraw(Graph) documentation.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe exception is the Edit menu. Moreover, the nodes and links
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof the graph have attached pop-up menus, which appear when
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiclicking with the right mouse button.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Edit] This menu has the following submenus:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[Unnamed nodes]
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe ``Hide/show names'' menu is a toggle:
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiyou can switch on or off the display of names for nodes that
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiare initially unnamed. The newly named nodes get names that
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiare derived from named neighbour nodes.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiWith the ``Hide nodes'' submenu, it is possible
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskito reduce the complexity of the graph by hiding all unnamed nodes;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskionly nodes corresponding to named specifications remain displayed.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiPaths between named nodes going through unnamed nodes
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiare displayed as links. With the ``Show nodes'' submenu, the unnamed
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskinodes re-appear.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Proofs] This menu allows to apply some of the deduction rules
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski for development graphs, see Sect. IV:4.4 of the \CASL Reference
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski Manual \cite{CASL/RefManual}. While support for local and global
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski (definition or theorem) links is stable, support for hiding links
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski and checking conservativity is still experimental. In most cases, it is
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski advisable to use ``Automatic'', which automatically applies the
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski rules in the correct order. As a result, the the open theorem links
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski (marked in red) will be reduced to local proof goals, that is, they
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski become green, and instead, some of the node will get red, indicating
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski open local proof goals.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Translate Graph] translates the whole development graph
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskialong a logic comorphism.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Show Logic Graph] shows the graph of logics and logic comorphisms
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskicurrently supported by \Hets.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Show Library Graph] shows the graph of libraries that have
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskibeen loaded into \Hets, and their dependencies. For library,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskithe corresponding development graphs can be shown using its node menu.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiAlso, a list of specifications and views can be shown.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Pop-up menu for nodes]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHere, the number of submenus depends on the type of the node:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show signature] Shows the signature of the node.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Show local axioms] Shows the local axioms of the node.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Show theory] Shows the theory of the node (including axioms
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiimported from other nodes). Warning: axioms imported via hiding links
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiare not part of the theory; they can be made visible only by re-adding
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskithe hidden symbols, using the proof rule \emph{Theorem-Hide-Shift}.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Translate theory] Translates the theory of a node to another logic.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiA menu with the possible translation paths will be displayed.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Taxonomy graphs] (Only available for some logics) Shows the subsort graph of the signature of the node.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show sublogic] Shows the logic and, within that logic, the minimal sublogic
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifor the signature and the axioms of the node.
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\item[Show origin] Shows the kind of \CASL structuring construct that
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskiled to the node.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Show proof status] Show open and proven local proof goals.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Prove] Try to prove the local proof goals. See Section~\ref{sec:Proofs}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Check consistency] Check the consistency of the theory of the node.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show just subtree] (Only for named nodes) Reduce the complexity
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof the graph by just showing the subtree below the current node.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Undo show just subtree] (Only for named nodes) Undo the reduction.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show referenced library] (Only for external nodes) Open a new window
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskishowing the development graph for the library the external node refers to.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski%\item[Show spec] Show the structured specification of the node.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski% (not fully implemented yet)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Show number of node] Show the internal number of the node.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Pop-up menu for links]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAgain, the number of submenus depends on the type of the node:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show morphism] Shows the signature morphism of the link. It consists
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof two components: a logic translation and a signature morphism in the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitarget logic of the logic translation.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiIn the (most frequent) case
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof an intra-logic signature morphism, the logic translation component is
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskijust the identity.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show origin] Shows the kind of \CASL structuring construct that
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiled to the link.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show proof status] (Only for theorem links) Show the proof status.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Check conservativity] (Experimental) Check whether the
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskitheory of the target node of the link
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiis a conservative extension of the theory of the source node.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Show ID of this edge] Shows the internal number of the edge.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiThese numbers are also used in the proof status information for
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\section{Reading, Writing and Formatting}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Hets provides several options controlling the types of files
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithat are read and written.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-i ITYPE}, \texttt{--input-type=ITYPE}] Specify
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\texttt{ITYPE} as the type of the input file. The default is
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\texttt{het} (\HetCASL plain text). \texttt{ast} is for reading
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiin abstract syntax trees in ATerm format, while \texttt{ast.baf}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskireads in the compressed ATerm format.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe possible input types are:
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{verbatim}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski (casl|het|owl|hs|ast[.baf]|[tree.]gen_trm[.baf])
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{verbatim}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-O DIR}, \texttt{--output-dir=DIR}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiSpecify \texttt{DIR} as destination directory for output files.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-o OTYPES}, \texttt{--output-types=OTYPES}]
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\texttt{OTYPES} is a comma separated list of output types:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{verbatim}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski | pp.(het|tex|html)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski | graph.(dot|ps|davinci)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski | ast.(het|trm|taf|html|xml)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski | (fdg|hdg|dg)[.nax].(het|trm|taf|html|xml)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{verbatim}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe default is \texttt{dg.taf}, which means that the development
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskigraph of the library is stored in textual ATerm format (\texttt{taf}).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThis format can be read in when a library is downloaded from
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskianother library, avoiding the need to re-analyse the downloaded library.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe \texttt{pp} format is for pretty printing, either as plain text
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(\texttt{het}), \LaTeX input (\texttt{tex}) or HTML (\texttt{html}).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiA formatter with pretty-printed output currently is available only for
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithe \CASL logic. For example, it is possible to generate a pretty
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiprinted \LaTeX\ version of \texttt{Order.casl} by typing:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThis will generate a file \texttt{Order.pp.tex}. It can be included
e8f5a6ef56e210093ad852ed147d7f5f0a24cce9Till Mossakowskiinto \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
e8f5a6ef56e210093ad852ed147d7f5f0a24cce9Till Mossakowskicoming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty)}) is used.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiWhen the \texttt{thy} format is selected, \Hets will try to translate
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskieach specification in the library to \Isabelle, and write one \Isabelle
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\texttt{.thy} file per specification.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiWhen the \texttt{comptable.xml} format is selected, \Hets will extract
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskithe composition and inverse table of a Tarskian relation algebra from
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskispecification(s) (selected with the \texttt{-n} or \texttt{--spec}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskioption). It is assumed that the relation algebra is
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskigenerated by basic relations, and that the specification is written
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiin the \CASL logic. A sample specification of a relation
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskialgebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiavailable from \texttt{www.cofi.info/Libraries}.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe output format is XML, the URL of the DTD is included in the
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski\item[\texttt{-t TRANS}, \texttt{--translation=TRANS}]
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowskichooses a translation option. \texttt{TRANS} is a colon-separated list
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiwithout blanks of one or more comorphism names (see Sect.~\ref{comorphisms}).
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-r RAW} or \texttt{--raw=RAW}] This option allows one
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskito influence the formatting in more detail.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHere, \texttt{RAW} is \texttt{(ascii|text|(la)?tex)=STRING},
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskiand \texttt{STRING} is passed to the appropriate pretty-printer.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThe details of these options are to be fixed in the future only.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe other output formats are for future usage.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Miscellaneous Options}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-v[Int]}, \texttt{--verbose[=Int]}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiSet the verbosity level according to \texttt{Int}. Default is 1.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-q}, \texttt{--quiet}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiBe quiet -- no diagnostic output at all. Overrides -v.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-V}, \texttt{--version}] Print version number and exit.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-h}, \texttt{--help}, \texttt{--usage}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiPrint usage information and exit.
a231094086321e19f9a689de4745512c91e00e4bTill Mossakowski\item[\texttt{+RTS -KIntM -RTS}] Increase the stack size to
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \texttt{Int} megabytes (needed in case of a stack overflow).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThis must be the first option.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-l LOGIC}, \texttt{--logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskideclaration. The default is \CASL.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-n SPECS}, \texttt{--spec=SPECS}]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskichooses a list of named specifications for processing
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\section{Proofs with Hets}\label{sec:Proofs}
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe graphical user interface (GUI) for calling a prover
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiis shown in Fig. \ref{fig:proof_window}. The list on the right
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskishows all goal names prefixed with the proof status in square
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskibrackets. A proved goal is indicated by a '+', a '-' indicates a
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskidisproved goal and a space denotes an open goal.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{figure}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\includegraphics[width=\textwidth]{proofmanagement1}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\caption{Hets Goal and Prover Interface\label{fig:proof_window}}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiIf you open this GUI when processing the goals of one node for the first
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskitime, it will show all goals as open. Within this list you can select
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskithose goals that should be inspected or proved. The button 'Display'
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskishows the selected goals in the ASCII syntax of this theory's logic in
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskia separate window. With the 'Prove' button the actual prover is
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskilaunched. This is described in more detail in the following
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiparagraphs. By pressing the 'Show Proof Details' button a window is
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiopened where for each proved goal the used axioms are shown. The
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski'Status:' shows either 'No prover running' or 'Waiting for prover' in
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiblack or blue. If you press the 'Close' button the window is closed
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiand the status of the goals' list is integrated into the
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskidevelopment graph. If all goals have been proved, the selected node
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiturns from red into green.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe list 'Pick Theorem Prover:' lets you choose one of the connected
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiprovers (currently, these are SPASS and \Isabelle, described below). By
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskipressing 'Prove' the selected prover is launched and the theory along
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiwith the selected goals is translated via the shortest possible path
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiof comorphisms into the provers logic. The button 'More fine grained
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiselection...' lets you pick a (composed) comorphism in a separate
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiwindow from where the prover is launched then.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\subsection*{SPASS}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{figure}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\includegraphics[width=\textwidth]{spassGUI1}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\caption{Interface of the SPASS prover\label{fig:SPASS_GUI}}
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe automatic theorem prover SPASS
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\cite{WeidenbachEtAl02} is a resolution-based prover for first-order logic
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiwith equality.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiIf you have chosen SPASS, initially, all selected goals are tried in a
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskirow. After this so called batch mode the results are displayed in a
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiwindow which is shown in Fig. \ref{fig:SPASS_GUI}. This GUI for the
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskitheorem prover SPASS is very similar to the 'Select Goal(s) and
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiProve' GUI which lets you choose a prover for some goals. But with the
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiSPASS GUI, the actual SPASS prover is launched with the selected
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskigoal. Further it is possible to set a time-limit and some options for
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiSPASS. The available options are shown in separate window by pressing
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskithe 'Help' button. The status of the selected goal is shown in the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski'Status:' line with either 'Proved', 'Disproved', 'Open' or 'Open Time
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski(Time is up!)'. If a goal has been proved the labels of the used
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiaxioms are shown in the list on the right. The button 'Show Details'
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskishows the whole output of SPASS. 'Save Prover Configuration allows you
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskito save the configuration and status of each proof for
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskidocumentation. By pressing the button 'Exit Prover' the status of
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskithese proofs and goals is transferred back to the main 'Select Goal(s)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiand Prove' window.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\subsection*{Isabelle}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\Isabelle \cite{NipPauWen02} is an interactive theorem prover, which is
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskimore powerful than SPASS, but also requires more user interaction.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskihas a very small core guaranteeing correctness, and its provers,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskilike the simplifier or the tableaux prover, are built on top of this
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskicore. Furthermore, there is over fifteen years of experience with it,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiand several mathematical textbooks have been partially
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \index{formal!verification}%
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\Isabelle is a tactic based theorem prover implemented in standard ML.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe main \Isabelle logic (called Pure) is some weak intuitionistic type
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskitheory with polymorphism. The logic Pure is used to represent a
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskivariety of logics within \Isabelle; one of them being \HOL (higher-order
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskilogic). For example, logical implication in Pure (written
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\texttt{==>}, also called meta-implication), is different from logical
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiimplication in \HOL (written \texttt{-->}, also called object
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiIt is essential to be aware of the fact that the \Isabelle/\HOL logic
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiis different from the logics that are encoded into it via comorphisms.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiTherefore, the formulas appearing in subgoals of proofs with \Isabelle
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiwill not conform to the syntax of the original input logic. They may
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskieven use features of \Isabelle/\HOL such as higher-order functions
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskithat are not present in an input logic like \CASL.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\Isabelle is started with ProofGeneral
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\cite{DBLP:conf/tacas/Aspinall00,url:ProofGeneral} in a separate Emacs
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\cite{url:Emacs,url:XEmacs}.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe \Isabelle theory file conforms to the Isabelle/Isar syntax
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\cite{NipPauWen02}. It starts with the theory (encoded along the selected
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski comorphism), followed by a list of theorems. Initially, all the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski theorems have trivial proofs, using the `oops` command. However, if
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski you have saved earlier proof attempts, \Hets will patch these into
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski the generated \Isabelle theory file, ensuring that your previous work
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski is not lost. (But note that this patching can only be successful
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski if you do not rename specifications, or change their structure.) You
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski now can replace the 'oops' commands with real \Isabelle proofs, and
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski use Proof General to step through the proofs. You finish your session
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski by saving your file (using the Emacs file menu, or the Ctrl-x Ctrl-s
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski key sequence), and pressing a button in a small pop-up window
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski generated by \Hets.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\section{Limits of Hets}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\Hets is still intensively under development. In particular, the
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskifollowing points are still missing:
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\begin{itemize}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item There is no proof support for architectural specifications.
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\item Distributed libraries are always downloaded from the local disk,
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskinot from the Internet.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\item Version numbers of libraries are not considered properly.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item The proof engine for development graphs provides only experimental
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskisupport for hiding links and for conservativity.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\section{Architecture of Hets}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets is written in Haskell. Its parser uses combinator
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{parsing}%
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe user-defined (also known as ``mixfix'') syntax of \CASL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicalls for a two-pass approach. In the first pass, the skeleton of a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\CASL abstract syntax tree is derived, in order to extract user-defined
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisyntax rules. In a second pass, which is performed during
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskianalysis, these syntax rules are used to parse
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiany expressions that
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiuse mixfix notation. The output is stored in the so-called
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{ATerms}%
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiATerm format \cite{BJKO00}, which is used as interchange format
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor interfacing with other tools.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets provides an abstract interface for
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{institution!independence}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{independence, institution}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinstitutions, so
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithat new logics can be integrated smoothly.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn order to do so, a parser,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskia static checker and a prover for basic specifications in the logic have
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito be provided.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{center}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\includegraphics[scale=0.4]{hets2007}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Architecture of the heterogeneous tool set.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{fig:hets}}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe architecture of \Hets is shown in Fig.~\ref{fig:hets}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIf your favourite logic is missing in \Hets, please tell us
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski(hets-users@informatik.uni-bremen.de). We will take account your feedback when deciding which
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogics and proof tools to integrate next into \Hets. Help with
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiintegration of more logics and proof tools into \Hets is also welcome.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets is mainly maintained by
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiChristian Maeder (Christian.Maeder@dfki.de) and Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski(Till.Mossakowski@dfki.de). The mailing list is
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \url{hets-users@informatik.uni-bremen.de}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskithe homepage is
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\url{http://www.informatik.uni-bremen.de/mailman/listinfo/hets-users}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\paragraph{Acknowledgement}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe heterogeneous tool set \Hets, which shows that the theory outlined
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiin this work can also be brought to practice, would not have possible
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiwithout cooperation with many people.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%Christian Maeder and Klaus L\"uttich.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiBesides the authors, the following people have been involved
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiin the implementation of \Hets:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiKatja Abu-Dib,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiMihai Codescu,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiCarsten Fischer,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiJorina Freya Gerken,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiRainer Grabbe,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiSonja Gr\"{o}ning,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiDaniel Hausmann,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiWiebke Herding,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCui ``Ken'' Jian,
2ef350ad6e8df3c2c1d76bb6a9dca42a267b3eb1Till MossakowskiAnton Kirilov,
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiTina Krausser,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMartin K\"{u}hl,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiDominik L\"{u}cke,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%Klaus L\"{u}ttich,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%Christian Maeder,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMaciek Makowski,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiImmanuel Normann,
2ef350ad6e8df3c2c1d76bb6a9dca42a267b3eb1Till MossakowskiRazvan Pascanu,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiDaniel Pratsch,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiFelix Reckers,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMarkus Roggenbach,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiPascal Schmidt,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiPaolo Torrini,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiRen\'{e} Wagner,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiJian Chun Wang and
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThiemo Wiedemeyer.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\Hets has been built based on experiences with its
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \index{Cats@\Cats}%
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \index{Maya@\MAYA}%
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe \CASL Tool Set (\Cats)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\cite{Mossakowski:2000:CST,Mossakowski:1998:SSA}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiprovides parsing and static analysis for \CASL.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiIt has been developed by the present author with help
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiof Mark van den Brand, Kolyang, Bartek Klin, Pascal Schmidt and
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiFrederic Voisin.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\MAYA \cite{Autexier:2002:IHD,AutexierEtal02} is a proof management
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskitool based on development graphs. \MAYA only supports development
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskigraphs without hiding and without logic translations. \MAYA has been
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskideveloped by Serge Autexier and Dieter Hutter.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiWe also want to thank Agn\`es Arnould, Thibaud Brunet, Pascale LeGall,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiKathrin Hoffmann, Katiane Lopes,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%Klaus L\"uttich, Christian Maeder,
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiStefan Merz, Maria Martins Moreira, Christophe
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiRingeissen, Markus Roggenbach, Dmitri Schamschurko, Lutz Schr\"oder,
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiKonstantin Tchekine and Stefan W\"olfl
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskifor giving feedback about \Cats, HOL-CASL and \Hets. Finally,
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskispecial thanks to Christoph L\"uth and George Russell
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskifor help with connecting \Hets to their UniForM workbench.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\bibliographystyle{plain}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\bibliography{cofibib,cofi-ann,UM,hets,kl}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{document}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% Local Variables:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% mode: latex
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% TeX-master: "UserGuide"