UserGuide.tex revision f8a33e72909e67885a9ecbae881fc75134c362cb
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\documentclass{article}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{alltt}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{casl}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{color}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{url}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{threeparttable,hhline}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage[pdfborder=0 0 0,bookmarks,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskipdfauthor={Till Mossakowski, Christian Maeder, Klaus Lüttich},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskipdftitle={Hets User Guide}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{hyperref} %% do not load more packages after this line!!
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}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \begin{minipage}{0.9\textwidth}\it}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski {\end{minipage}\par\medskip}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SLIDESMALL} {}
5277e290ad70afdf97f359019afd8fb5816f4102Till 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}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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}
5277e290ad70afdf97f359019afd8fb5816f4102Till 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}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand {\Isabelle}{\normalTEXTSC{I}{SABELLE}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand {\SPASS}{\normalTEXTSC{S}{PASS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%%%% Klaus macros
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till 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}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till 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}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till 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}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}
53eb610e03705ac6499371cde16cc37482fb3313Till 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}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{document}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\title{{\bf \protect{\LARGEHets} User Guide}\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski-- Version 0.73 --}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\author{Till Mossakowski, Christian Maeder, Klaus L\"{u}ttich\\[1em]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDFKI Lab Bremen, Bremen, Germany.\\[1em]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiComments to: hets@informatik.uni-bremen.de\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskior to: hets-users@informatik.uni-bremen.de \\
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski(the latter needs subscription to the mailing list)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Introduction}
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe Heterogeneous Tool Set (\protect\Hets) is the main analysis tool
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskifor the specification language heterogeneous \CASL. Heterogeneous
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\CASL (\HetCASL) combines the specification language \CASL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{CASL-UM,CASL/RefManual} with \CASL extensions
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand sublanguages, as well as completely different logics and even
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiprogramming languages such as Haskell. \HetCASL
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski(see Fig.~\ref{fig:lang} for a simple subset)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiextends the structuring mechanisms of \CASL:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\emph{Basic specifications} are
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiunstructured specifications or modules written in a specific logic.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe graph of currently supported logics and logic translations (the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilatter are also called comorphisms) is shown in
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFig.~\ref{fig:LogicGraph}, and the degree of support by \Hets in
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFig.~\ref{fig:Languages}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}[ht]
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiSPEC ::= BASIC-SPEC
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski | SPEC then SPEC
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski | SPEC then %implies SPEC
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski | SPEC with SYMBOL-MAP
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski | SPEC with logic ID
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiDEFINITION ::= logic ID
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | spec ID = SPEC end
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | view ID : SPEC to SPEC = SYMBOL-MAP end
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski | view ID : SPEC to SPEC = with logic ID end
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiLIBRARY = DEFINITION*
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{verbatim}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\caption{Syntax of a simple subset of the heterogeneous
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskispecification language.
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski\texttt{BASIC-SPEC} and \texttt{SYMBOL-MAP} have a logic
881ab7022a03f9a6fa697d3067d05d61844929cbChristian Maederspecific syntax, while \texttt{ID} stands for some form of
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiidentifiers.\label{fig:lang}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiWith \emph{heterogeneous structured specifications}, it is possible to
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicombine and rename specifications, hide parts thereof, and also
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskitranslate them to other logics. \emph{Architectural specifications}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiprescribe the structure of implementations. \emph{Specification
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski libraries} are collections of named structured and architectural
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecifications.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets consists of logic-specific tools for the parsing and static
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskianalysis of the different involved logics, as well as a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogic-independent parsing and static analysis tool for structured and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiarchitectural specifications and libraries. The latter of course needs
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskito call the logic-specific tools whenever a basic specification is
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\Hets is based on the theory of institutions \cite{GoguenBurstall92},
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiwhich formalize the notion of a logic. The theory behind \Hets is laid
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiout in \cite{Habil}. A short overview of \Hets is given in
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\cite{MossakowskiEA06,MossakowskiEtAl07b}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\section{Logics supported by Hets}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe following list of logics (formalized as so-called institutions
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\cite{GoguenBurstall92}) is currently supported by \Hets:
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till 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
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till 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}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{figure}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{center}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{tabular}{|l|c|c|c|}\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiLanguage & Parser & Static Analysis & Prover \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CASL & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CoCASL & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\ModalCASL & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\HasCASL & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiHaskell & x & x & -\\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CspCASL & (x) & - & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till 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
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiPropositional & x & x & x \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiSoftFOL & - & - & x \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\Isabelle & - & - & x \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till 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/RefManual,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,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskisuited for the specification of process types and reactive systems.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe central proof method is coinduction.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[ModalCASL] \cite{ModalCASL}
53eb610e03705ac6499371cde16cc37482fb3313Till 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
53eb610e03705ac6499371cde16cc37482fb3313Till 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
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski embedded in the specification.
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithe language is summarized in \cite{HasCASL/Summary}, the semantics
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiin \cite{Schroder05b,Schroder-habil}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Haskell] is a modern, pure and strongly typed functional
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski programming language. It simultaneously is the implementation
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski language of \Hets, such that in the future, \Hets might be applied
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe definitive reference for Haskell is \cite{PeytonJones03},
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[CspCASL] \cite{Roggenbach06} is a combination of \CASL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski with the process algebra CSP.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[ConstraintCASL] is an experimental logic for the specification
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskiof qualitative constraint calculi.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\item[OWL DL] is the Web Ontology Language (OWL) recommended by the
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski World Wide Web Consortium (W3C, \url{http://www.w3c.org}). It is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski used for knowledge representation and the Semantic Web
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \cite{berners:2001:SWeb}.
5277e290ad70afdf97f359019afd8fb5816f4102Till 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.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[CASL-DL] \cite{OWL-CASL-WADT2004}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till 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
a8ce558d09f304be325dc89458c9504d3ff7fe80Till 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
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski \CASL closer together.
7e7c1b5990145d02f8abb7c74d3c0d609735b54cTill Mossakowski\item[Propositional] is classical propositional logic, with
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithe zChaff SAT solver \cite{Herbstritt03} connected to it.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[SoftFOL] \cite{LuettichEA06a} offers three automated theorem
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski proving (ATP) systems for first-order logic with equality: (1) \SPASS
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski \cite{WeidenbachEtAl02}; (2) Vampire \cite{RiazanovV02}; and (3)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski MathServe Broker\footnote{which chooses an appropriate ATP upon a
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski classification of the FOL problem} \cite{ZimmerAutexier06}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski These together comprise some of the most advanced theorem provers
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski for first-order logic.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski for higher-order logic.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiPropositional, SoftFOL and \Isabelle are currently the only logics
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicoming with a prover. Proof support for the other logics can be
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiobtained by using logic translations to a prover-supported logic.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiAn introduction to \CASL can be found in the \CASL User Manual
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\cite{CASL-UM}; the detailed language reference is given in
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithe \CASL Reference Manual \cite{CASL/RefManual}. These documents
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiexplain both the \CASL logic and language of basic specifications as
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiwell as the logic-independent constructs for structured and
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiarchitectural specifications. The corresponding document explaining the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\HetCASL language constructs for \emph{heterogeneous} structured specifications
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiis the \HetCASL language summary \cite{Mossakowski04}; a formal
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskisemantics as well as a user manual with more examples are in preparation.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiSome of \HetCASL's heterogeneous constructs will be illustrated
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiin Sect.~\ref{sec:HetSpec} below.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\section{Logic translations supported
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\label{comorphisms}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiLogic translations (formalized as institution comorphisms
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\cite{GoguenRosu02}) translate from a given source logic to a given
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskitarget logic. More precisely, one and the same logic translation
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskimay have several source and target \emph{sub}logics: for
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskieach source sublogic, the corresponding sublogic of the target
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogic is indicated.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiA graph of the most important logics and sublogics, together with their
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicomorphisms, is shown in Fig.~\ref{fig:SublogicGraph}.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \begin{center}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \includegraphics[scale=0.4]{SublogicGraph}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Graph of most important sublogics currently supported by \Hets,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskitogether with their comorphisms.}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\label{fig:SublogicGraph}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn more detail, the following list of logic translations is currently
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisupported by \Hets:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{tabular}{|l|p{5cm}|}\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCASL2CoCASL & inclusion \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCASL2CspCASL & inclusion \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCASL2HasCASL & inclusion \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCASL2Modal & inclusion \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCASL2PCFOL & coding of subsorting by injections, see Chap.\ III:3.1 of the CASL Reference Manual \cite{CASL/RefManual}\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCASL2SubCFOL & coding of partial functions by error elements
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(translation $(4a')$ of \cite{Mossakowski02}, but extended to subsorting) \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCASL2TopSort & coding of subsorting by a top sort and unary
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskipredicates for the subsorts \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCFOL2IsabelleHOL & coding of \CASL to Isabelle
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(translation $(7)$ of \cite{Mossakowski02}) \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCoCASL2CoPCFOL & coding of subsorting by injections, similar to CASL2PCFOL \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCoCASL2CoSubCFOL & coding of partial functions by error supersorts, similar to CASL2SubCFOL \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCoCFOL2IsabelleHOL & coding of \CoCASL to Isabelle, similar to CFOL2IsabelleHOL \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%CoPCFOL2CoCFOL & coding of partial functions by error elements,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%similar to PCFOL2CFOL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%%CspCASL2IsabelleHOL & \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%%CspCASL2Modal & \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHasCASL2HasCASL & coding of \HasCASL axiomatic recursive definitions
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskias \HasCASL recursive program definitions \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHasCASL2Haskell & translation of \HasCASL recursive program definitions to Haskell \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHasCASL2IsabelleHOL & coding of HasCASL to Isabelle/HOL \cite{Groening05} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHaskell2IsabelleHOL & coding of Haskell to Isabelle/HOL \cite{TorriniEtAl07} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHaskell2IsabelleHOLCF & coding of Haskell to Isabelle/HOLCF \cite{TorriniEtAl07}\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiModal2CASL & the standard translation of modal logic
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskito first-order logic \cite{blackburn_p-etal:2001a} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%PCFOL2CFOL & coding of partial functions by error elements
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%(translation $(4a')$ of \cite{Mossakowski02}) \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiPCoClTyConsHOL2IsabelleHOL & coding of \HasCASL to Isabelle/HOL\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiSuleCFOL2SoftFOL & coding of CASL to SoftFOL \cite{LuettichEA06a},
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimapping types to soft types \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiSuleCFOL2SoftFOLIndcuction & dto., but with instances of induction
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiaxioms for all proof goals\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiProp2CASL & inclusion \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiProp2CNF & conversion of propositional formulas to conjunctive normal form\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Getting started}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe latest \Hets version can be obtained from the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets tools home page
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Since \Hets is being
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiimproved constantly, it is recommended always to use the latest version.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Hets currently is available for Linux, Solaris and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThere are three possibilities to install \Hets:
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{enumerate}
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiThe Java-based \Hets installer. Download a \texttt{.jar} file and
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskijava -jar \texttt{file.jar}
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiNote that you need Sun Java 1.4.2 or later. On a Mac, you can just
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskidouble-click on the \texttt{.jar} file.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiThe installer will lead you through the installation with
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskia graphical interface. It will download and install further
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskisoftware (if not already installed on your computer):
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\begin{tabular}{|l|l|l|}\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiCASL-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiuDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiTcl/Tk & graphics widget system & \url{http://www.scriptics.com/software/tcltk/} \\\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\SPASS & theorem prover & \url{http://spass.mpi-sb.mpg.de/}\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski(X)Emacs & editor (for Isabelle) & (must be installed manually)\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiIf you do not have Sun Java, you can just download the hets binary.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiYou have to unpack it with \texttt{bunzip2} and then put it at
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill Mossakowskisome place coverd by your \texttt{PATH}. You also have to
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiinstall the above mentioned software and set
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiseveral environment variables, as explained on the installation page.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiIf you want to compile \Hets from the sources, please follow the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilink ``Hets: source code and information for developers''
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskion the \Hets web page, download the sources (as tarball or from
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisvn), and follow the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinstructions in the \texttt{INSTALL} file.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{enumerate}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Analysis of Specifications}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiConsider the following \CASL
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecification:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{BIGEXAMPLE}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\I\SPEC \NAME{Strict\_Partial\_Order} =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{ITEMS}[\PRED]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\I\SORT \( Elem \)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski% \COMMENTENDLINE{\PRED abbreviates predicate}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\(\[ \FORALL x,y,z : Elem \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{COMMENT}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiNote that there may exist \(x, y\) such that\\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskineither \(x < y\) nor \(y < x\).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{BIGEXAMPLE}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets can be used for parsing and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskichecking static well-formedness of specifications.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \index{parsing}%
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \index{static!analysis}%
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \index{analysis, static}%
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill 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).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThen you can check the well-formedness of the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecification by typing (into some shell):
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets checks both the correctness of this specification
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski with respect to the \CASL syntax, as
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskiwell as its correctness with respect to the static semantics (e.g.\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiwhether all identifiers have been declared before they are used,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiwhether operators are applied to arguments of the correct sorts,
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill Mossakowskiwhether the use of overloaded symbols is unambiguous, and so on).
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill 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}] Do the parsing and the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski static analysis of (heterogeneous) structured specifications, but
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski leave out the analysis of basic specifications. This can be used
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski for prototyping issues, namely to quickly produce a development graph
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski showing the dependencies among the specifications (cf.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Sect.~\ref{sec:DevGraph}) even if the individual specifications are
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski not correct yet.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiUse \texttt{DIR} as the directory for specification libraries
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski(equivalently, you can set the variable \texttt{HETS\_LIB} before
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskicalling \Hets).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{--casl-amalg=ANALYSIS}]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski For the analysis of architectural specification (a quite advanced
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski amalgamability checking
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski algorithm for \CASL logic; it is a comma-separated list of zero or
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski more of the following options:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \item[\texttt{sharing}] perform sharing analysis for sorts,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski operations and predicates.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \item[\texttt{cell}] perform cell condition check; implies
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \texttt{sharing}. With this option on, the subsort embeddings are
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \item[\texttt{colimit-thinness}] perform colimit thinness check;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski implies \texttt{sharing}. The colimit thinness check is less
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski complete and usually takes longer than the full cell condition
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski check (\texttt{cell} option), but may prove more efficient in case
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski of certain specifications.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski If \texttt{ANALYSIS} is empty then amalgamability analysis for
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \CASL is skipped.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski The default value for \texttt{--casl-amalg} is
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \texttt{cell}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\section{Heterogeneous Specification} \label{sec:HetSpec}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets accepts plain text input files with the following endings:\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{tabular}{|l|c|c|}\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiEnding & default logic & structuring language\\\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\texttt{.casl} & \CASL & \CASL \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.het} & \CASL & \CASL \\\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\texttt{.hs} & Haskell & Haskell\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.owl} & OWL DL, OWL Lite & OWL\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAlthough the endings \texttt{.casl} and \texttt{.het} are
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinterchangeable, the former should be used for libraries of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskihomogeneous \CASL specifications and the latter for \HetCASL libraries
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof heterogeneous specifications (that use the \CASL structuring
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiconstructs). Within a \HetCASL library, the current logic can be changed e.g.\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito \HasCASL in the following way:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe subsequent specifications are then parsed and analysed as
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\HasCASL specifications. Within such specifications,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiit is possible to use references to named \CASL specifications;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithese are then automatically translated along the default
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiembedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(There are also heterogeneous constructs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor explicit translations between logics, see \cite{Mossakowski04}.)
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiA \CspCASL specification consists of a \CASL specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor the data part and a \Csp process built over this data part.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTherefore, \HetCASL provides a heterogeneous language construct
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{data} as follows:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilibrary Buffer
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski free type List[Elem] ::= nil | cons(Elem; List[Elem])
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski channel read, write : Elem
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let Buf(l:List[Elem]) =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski read?x -> Buf( cons(x,nil) )
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski [] if l=nil then STOP else write!last(l) -> Buf( rest(l) )
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHere, the construct \texttt{data List} refers to the \CASL specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{List}, which is implicitly embedded into \CspCASL.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe ending \texttt{.hs} is available for directly reading in
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHaskell programs % and HasSLe specifications,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiand hence supports the Haskell module system.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe logic Haskell has to be chosen explicitly, and the \CASL structuring
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisyntax needs to be used:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilibrary Factorial
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispec Factorial =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifac :: Int -> Int
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifac n = foldl (*) 1 [1..n]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiNote that according to the Haskell syntax, Haskell function
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskideclarations and definitions need to start with the first column of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Development Graphs}\label{sec:DevGraph}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDevelopment graphs are a simple kernel formalism for (heterogeneous)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskistructured theorem proving and proof management.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiA development graph consists of a set of nodes (corresponding to whole
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskistructured specifications or parts thereof), and a set of arrows
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicalled \emph{definition links}, indicating the dependency of each
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinvolved structured specification on its subparts. Each node is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiassociated with a signature and some set of local axioms. The axioms
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof other nodes are inherited via definition links. Definition links
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowskiare usually drawn as black solid arrows, denoting an import of another
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispecification.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiComplementary to definition links, which \emph{define} the theories of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirelated nodes, \emph{theorem links} serve for \emph{postulating}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirelations between different theories. Theorem links are the central
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidata structure to represent proof obligations arising in formal
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTheorem links can be \emph{global} (drawn as solid arrows) or
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{local} (drawn as dashed arrows): a global theorem link
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskipostulates that all axioms of the source node (including the inherited
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiones) hold in the target node, while a local theorem link only postulates
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithat the local axioms of the source node hold in the target node.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBoth definition and theorem links can be \emph{homogeneous},
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskii.e. stay within the same logic, or \emph{heterogeneous}, i.e.\ %% such that
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe logic changes along the arrow. Technically, this is the case
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor Grothendieck signature morphisms $(\rho,\sigma)$ where
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$\rho\not=id$. This case is indicated with double arrows.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTheorem links are initially displayed in red.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe \emph{proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski calculus} for development graphs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{MossakowskiEtAl05,Habil} is given by rules
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithat allow for proving global theorem links by decomposing them
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinto simpler (local and global) ones. Theorem links that have been
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproved with this calculus are drawn in green. Local theorem links can
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskibe proved by turning them into \emph{local proof goals}. The latter
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskican be discharged using a logic-specific calculus as given by an
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskientailment system for a specific institution. Open local
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof goals are indicated by marking the corresponding node in the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidevelopment graph as red; if all local implications are proved, the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskinode is turned into green. This implementation ultimately is based
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskion a theorem \cite{Habil} stating soundness and relative completeness
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof the proof calculus for heterogeneous development graphs.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand in \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following options let \Hets show the development graph of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskia specification library:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-G}, \texttt{--only-gui}] Shows the development graph in a GUI window,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand suppresses the writing of an output file.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiLet us extend the above library \texttt{Order.casl}. One use of the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilibrary might be to express the fact that the natural numbers form a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskistrict partial order as a view, as follows:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\NAMEREF{Natural\_Order\_2} =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\I{} \( Elem \MAPSTO Nat\)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAgain, these specifications can be checked with \Hets. However, this
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskionly checks syntactic and static semantic well-formedness -- it is
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiby a strict partial ordering relation. Checking this requires theorem
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiproving, which will be discussed below.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHowever, before coming to theorem proving, let us first inspect the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiproof obligations arising from a specification. This can be done with:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\texttt{hets -g Order.casl}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(assuming that the above two specifications and the view
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskihave been added to the file
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Hets now displays a so-called development graph
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(which is just an overview graph showing the overall structure
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof the specifications in the library), see Fig.~\ref{fig:dg0}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{figure}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{center}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\includegraphics[scale=0.7]{dg-order-0}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\caption{Sample development graph.\label{fig:dg0}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiNodes in a development graph correspond to \CASL specifications.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiArrows show how specifications are related by the structuring
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe black arrow denotes an ordinary import of
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskispecifications (generated by the extension), while the red arrow
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidenotes a proof obligation (corresponding to the view).
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThis proof obligation needs to be discharged in order to
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskishow that the view is well-formed (then its color turns into green).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAs a more complex example, consider the following loose specification
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof a sorting function, taken from the \CASL User Manual
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\cite{CASL-UM}, Chap.~6:
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{BIGEXAMPLE}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\I\SPEC \NAMEREF{List\_Order\_Sorted}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{ITEMS}[\WITHIN]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{ITEMS}[\PRED]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\I\PRED \( \_\_is\_sorted : List \)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\(\[ \FORALL e,e': Elem; L : List \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \. empty~is\_sorted \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. cons(e,empty)~is\_sorted \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. cons(e,cons(e',L))~is\_sorted \IFF
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{ITEMS}[\OP]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\I\OP \( order : List \TOTAL List \)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{BIGEXAMPLE}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe following specification of sorting by insertion also is taken from
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithe \CASL User Manual \cite{CASL-UM}, Chap.~6:
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\begin{BIGEXAMPLE}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\I\SPEC \NAMEREF{List\_Order}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\phantomsection
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{ITEMS}[\WITHIN]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{ITEMS}[\OP]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\I\OP \( insert : Elem \* List \TOTAL List \)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\(\[ \FORALL e,e':Elem; L:List \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. insert(e, empty) = cons(e, empty) \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. insert(e, cons(e',L)) = \[ cons(e', insert(e,L)) \WHEN e' < e\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ELSE cons(e, cons(e',L)) \] \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{ITEMS}[\OP]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\I\OP \( order : List \TOTAL List \)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\(\[ \FORALL e:Elem; L:List \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. order(empty) = empty \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. order(cons(e,L)) = insert(e, order(L)) \]\)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{BIGEXAMPLE}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiBoth specifications are related. To see this, we first inspect
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitheir signatures. This is possible with:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\texttt{hets -g Sorting.casl}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiassuming that \texttt{Sorting.casl} contains the above specifications.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{figure}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{center}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\includegraphics[scale=0.7]{dg-order-1}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\caption{Development graph for the two sorting specifications.\label{fig:dg1}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiIn the above-mentioned development graph, we have two types of nodes.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe named ones correspond to named specifications, but there
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiare also unnamed nodes corresponding to anonymous basic
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecifications like the declaration of the $insert$ operation in
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\NAMEREF{List\_Order} above. Basically, there is an
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskiunnamed node for each structured specification that is not named.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiAgain, the black arrows denote an ordinary import of specifications
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski(corresponding to the extensions and unions in the
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskispecifications), while the blue arrows denote hiding (corresponding to
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskithe local specification).
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiBy clicking on the nodes, one can inspect their signatures.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiIn this way, we can see that both \NAMEREF{List\_Order\_Sorted} and
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\NAMEREF{List\_Order} have the same signature. Hence, it
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiis legal to add a view:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{EXAMPLE}%[\SLIDESMALL]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\I\VIEW \NAMEDEFN{v2}[\NAMEREF{Total\_Order}] ~:~ \NAMEREF{List\_Order\_Sorted}[\NAMEREF{Total\_Order}] \TO
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\NAMEREF{List\_Order}[\NAMEREF{Total\_Order}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiWe have already added this view to \texttt{Sorting.casl}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe corresponding
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiproof obligation between \NAMEREF{List\_Order\_Sorted} and
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\NAMEREF{List\_Order} is displayed in Fig.~\ref{fig:dg1}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski as a red arrow.
e8f5a6ef56e210093ad852ed147d7f5f0a24cce9Till MossakowskiHere is a summary of the types of nodes and links occurring in
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidevelopment graphs:
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{description}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Named nodes] correspond to a named specification.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Unnamed nodes] correspond to an anonymous specification.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Elliptic nodes] correspond to a specification in the current library.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Rectangular nodes] are external nodes corresponding
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski to a specification downloaded from
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskianother library.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Red nodes] have open proof obligations.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Green nodes] have all proof obligations resolved.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Black links] correspond to reference to other specifications
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski(definition links in the sense of \cite[IV:4]{CASL/RefManual}).
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Blue links] correspond to hiding (hiding definition links).
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Red links] correspond to open proof obligations (theorem links).
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Green links] correspond to proved proof obligations (theorem links).
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Yellow links] correspond to open proof obligations involving hiding (hiding theorem links).
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill 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}.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\item[Single links] have homogeneous signature morphisms (staying within
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskione and the same logic).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Double links] have heterogeneous signature morphisms (moving between
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWe now explain the menus of the development graph window.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiMost of the pull-down menus of the window are uDraw(Graph)-specific
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitheir function can be looked up in the uDraw(Graph) documentation\footnote{see
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\url{http://www.informatik.uni-bremen.de/uDrawGraph/en/service/uDG31\_doc/}.}.
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}
a231094086321e19f9a689de4745512c91e00e4bTill Mossakowski\item[Edit] This menu has the following submenus:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[undo] Undo the last development graph proof step (see under Proofs)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[redo] Restore the last undone development graph proof step (see
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski under Proofs)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[reload] Reload the specification library (Attention! all proofs are lost. A change management keep proofs is in preparation.)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Unnamed nodes]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe ``Hide/show names'' menu is a toggle:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiyou can switch on or off the display of names for nodes that
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiare initially unnamed. The newly named nodes get names that
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiare derived from named neighbour nodes.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiWith the ``Hide nodes'' submenu, it is possible
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskito reduce the complexity of the graph by hiding all unnamed nodes;
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskionly nodes corresponding to named specifications remain displayed.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiPaths between named nodes going through unnamed nodes
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiare displayed as links. With the ``Show nodes'' submenu, the unnamed
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskinodes re-appear.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Proofs] This menu allows to apply some of the deduction rules
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski for development graphs, see Sect. IV:4.4 of the \CASL Reference
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski Manual \cite{CASL/RefManual} or one of
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}. While support for
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski local and global (definition or theorem) links is stable, support
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski for hiding links and checking conservativity is still experimental.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski In most cases, it is advisable to use ``Automatic'', which
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski automatically applies the rules in the correct order. As a result,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski the the open theorem links (marked in red) will be reduced to local
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski proof goals, that is, they become green, and instead, some of the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski node will get red, indicating open local proof goals.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Translate Graph] translates the whole development graph
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskialong a logic comorphism.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Show Logic Graph] shows the graph of logics and logic comorphisms
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskicurrently supported by \Hets.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Show Library Graph] shows the graph of libraries that have
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskibeen loaded into \Hets, and their dependencies. For library,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskithe corresponding development graphs can be shown using its node menu.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiAlso, a list of specifications and views can be shown.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\end{description}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Pop-up menu for nodes]
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiHere, the number of submenus depends on the type of the node:
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{description}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Show signature] Shows the signature of the node.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Show local axioms] Shows the local axioms of the node.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Show theory] Shows the theory of the node (including axioms
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiimported from other nodes). Warning: axioms imported via hiding links
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiare not part of the theory; they can be made visible only by re-adding
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskithe hidden symbols, using the proof rule \emph{Theorem-Hide-Shift}.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Translate theory] Translates the theory of a node to another logic.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiA menu with the possible translation paths will be displayed.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Taxonomy graphs] (Only available for some logics) Shows the subsort graph of the signature of the node.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Show sublogic] Shows the logic and, within that logic, the minimal sublogic
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskifor the signature and the axioms of the node.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Show origin] Shows the kind of \CASL structuring construct that
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiled to the node.
53eb610e03705ac6499371cde16cc37482fb3313Till 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}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Check consistency] Check the consistency of the theory of the node.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Show just subtree] (Only for named nodes) Reduce the complexity
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiof the graph by just showing the subtree below the current node.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Undo show just subtree] (Only for named nodes) Undo the reduction.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Show referenced library] (Only for external nodes) Open a new window
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskishowing the development graph for the library the external node refers to.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski%\item[Show spec] Show the structured specification of the node.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski% (not fully implemented yet)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Show number of node] Show the internal number of the node.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\end{description}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Pop-up menu for links]
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiAgain, the number of submenus depends on the type of the link:
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{description}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Show morphism] Shows the signature morphism of the link. It consists
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiof two components: a logic translation and a signature morphism in the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskitarget logic of the logic translation.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiIn the (most frequent) case
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiof an intra-logic signature morphism, the logic translation component is
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskijust the identity.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Show origin] Shows the kind of \CASL structuring construct that
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiled to the link.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Show proof status] (Only for theorem links) Show the proof status.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Check conservativity] (Experimental) Check whether the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskitheory of the target node of the link
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiis a conservative extension of the theory of the source node.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Show ID of this edge] Shows the internal number of the edge.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThese numbers are also used in the proof status information for
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\end{description}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\end{description}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\section{Reading, Writing and Formatting}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\Hets provides several options controlling the types of files
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskithat are read and written.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{description}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{-i ITYPE}, \texttt{--input-type=ITYPE}] Specify
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\texttt{ITYPE} as the type of the input file. The default is
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\texttt{het} (\HetCASL plain text). \texttt{ast} is for reading
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiin abstract syntax trees in ATerm format, while \texttt{ast.baf}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskireads in the compressed ATerm format.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe possible input types are:
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{verbatim}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (casl|het|owl|hs|ast[.baf]|[tree.]gen_trm[.baf])
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\end{verbatim}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{-O DIR}, \texttt{--output-dir=DIR}]
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiSpecify \texttt{DIR} as destination directory for output files.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{-o OTYPES}, \texttt{--output-types=OTYPES}]
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\texttt{OTYPES} is a comma separated list of output types:
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{verbatim}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski | (sig|th)[.delta]
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski | pp.(het|tex|html)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski | graph.(exp.dot|dot|ps|davinci)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski | ast.(het|trm|taf|html|xml)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski | (fdg|hdg|dg)[.nax].(het|trm|taf|html|xml)
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\end{verbatim}
47af295501ed5f407848f61b9943d58ccb43be29Till MossakowskiThe default is \texttt{prf} (a synonym for \texttt{dg.taf}), which
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskimeans that the development graph of the library is stored in textual
47af295501ed5f407848f61b9943d58ccb43be29Till MossakowskiATerm format (\texttt{taf}). This format can be read in when a
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskilibrary is downloaded from another library, avoiding the need to
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskire-analyse the downloaded library. You can also directly read in
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskithe \texttt{prf} format (both from the command line, by calling
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\Hets on the \texttt{prf} file, and from the GUI, using the
47af295501ed5f407848f61b9943d58ccb43be29Till MossakowskiFile-Open menu.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe \texttt{env} format is currently not used.
47af295501ed5f407848f61b9943d58ccb43be29Till MossakowskiThe \texttt{omdoc} format \cite{books/sp/Kohlhase06} is an XML-based
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskimarkup format and data model for Open Mathematical Documents. It
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiserves as semantics-oriented representation format and ontology
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilanguage for mathematical knowledge. Currently, \CASL specifications
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskican be output in this format; support for further logics is planned.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe \texttt{hs} format is used for Haskell modules. Executable \CASL or
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\HasCASL specifications can be translated to Haskell.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWhen the \texttt{thy} format is selected, \Hets will try to translate
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskieach specification in the library to \Isabelle, and write one \Isabelle
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.thy} file per specification.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWhen the \texttt{comptable.xml} format is selected, \Hets will extract
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe composition and inverse table of a Tarskian relation algebra from
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispecification(s) (selected with the \texttt{-n} or \texttt{--spec}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskioption). It is assumed that the relation algebra is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskigenerated by basic relations, and that the specification is written
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiin the \CASL logic. A sample specification of a relation
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskialgebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiavailable from \texttt{www.cofi.info/Libraries}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe output format is XML, the URL of the DTD is included in the
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe \texttt{pp} format is for pretty printing, either as plain text
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(\texttt{het}), \LaTeX input (\texttt{tex}) or HTML (\texttt{html}).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiA formatter with pretty-printed output currently is available only for
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe \CASL logic. For example, it is possible to generate a pretty
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiprinted \LaTeX\ version of \texttt{Order.casl} by typing:
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThis will generate a file \texttt{Order.pp.tex}. It can be included
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinto \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicoming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty}) is used.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe \texttt{dfg} format is used by the \SPASS theorem prover
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{WeidenbachEtAl02}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe \texttt{tptp} format (\url{http://www.tptp.org}) is a standard
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiformat for first-order theorem provers.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-t TRANS}, \texttt{--translation=TRANS}]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskichooses a translation option. \texttt{TRANS} is a colon-separated list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwithout blanks of one or more comorphism names (see Sect.~\ref{comorphisms}).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-r RAW} or \texttt{--raw=RAW}] This option allows one
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskito influence the formatting in more detail.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiHere, \texttt{RAW} is \texttt{(ascii|text|(la)?tex)=STRING},
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiand \texttt{STRING} is passed to the appropriate pretty-printer.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe details of these options are to be fixed in the future only.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-R}, \texttt{--recursive}] output also imported libraries.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe other output formats are for future usage.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Miscellaneous Options}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-v[Int]}, \texttt{--verbose[=Int]}]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiSet the verbosity level according to \texttt{Int}. Default is 1.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-q}, \texttt{--quiet}]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiBe quiet -- no diagnostic output at all. Overrides -v.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-V}, \texttt{--version}] Print version number and exit.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-h}, \texttt{--help}, \texttt{--usage}]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiPrint usage information and exit.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{+RTS -KIntM -RTS}] Increase the stack size to
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \texttt{Int} megabytes (needed in case of a stack overflow).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThis must be the first option.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill 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}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskideclaration. The default is \CASL.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-n SPECS}, \texttt{--spec=SPECS}]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskichooses a list of named specifications for processing
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-m FILE}, \texttt{--modelSparQ=FILE}] model check a qualitative calculus given in SparQ lisp notation \cite{SparQ06} against a \CASL specification
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-I}, \texttt{--interactive}] run \Hets in interactive mode (experimental)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{description}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\section{Proofs with \Hets}\label{sec:Proofs}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe proof calculus for development graphs (Sect.~\ref{sec:DevGraph})
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskireduces global theorem links to local proof goals. Local proof goals
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski(indicated by red nodes in the development graph) can be eventually
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskidischarged using a theorem prover, using the ``Prove'' menu of a red node.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe graphical user interface (GUI) for calling a prover is shown in
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiFig. \ref{fig:proof_window} --- we call it ``Proof Management GUI''.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe list on the left shows all goal names prefixed with the proof
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskistatus in square brackets. A proved goal is indicated by a `+', a `-'
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiindicates a disproved goal, a space denotes an open goal, and a
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski`$\times$' denotes an inconsistent specification (aka a fallen `+';
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskisee below for details).
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{figure}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\includegraphics[width=\textwidth]{proofmanagement1}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\caption{Hets Goal and Prover Interface\label{fig:proof_window}}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiIf you open this GUI when processing the goals of one node for the
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskifirst time, it will show all goals as open. Within this list you can
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiselect those goals that should be inspected or proved. The button
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski`Display' shows the selected goals in the ASCII syntax of this
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitheory's logic in a separate window. With the `Prove' button the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiactual prover is launched. This is described in more detail in the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiparagraphs below. By pressing the `Show Proof Details' button a window
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis opened where for each proved goal the used axioms, its proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiscript, and its proof are shown --- the level of detail depends on the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiused theorem prover. The `Status:' shows either `No prover running' or
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski`Waiting for prover' in black or blue. If you press the `Close' button
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe window is closed and the status of the goals' list is integrated
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinto the development graph. If all goals have been proved, the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiselected node turns from red into green.
% http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0
\url{http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0}
\cite{DBLP:conf/tacas/Aspinall00,url:ProofGeneral} in a separate Emacs
The \Isabelle theory file conforms to the Isabelle/Isar syntax
version, where e.g.\ error handling is ignored. For technical reasons
the static analysis of basic specifications) and/or translates (along
of the \Hets home page at \url{http://www.dfki.de/sks/hets}.
%\input{hets.tex}