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