UserGuide.tex revision 881ab7022a03f9a6fa697d3067d05d61844929cb
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\documentclass{article}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\usepackage{alltt}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\usepackage{casl}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\usepackage{xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{color}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\newcommand{\QUERY}[1]%{}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\newcommand{\eat}[1]{}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\IEXT}[1] {\\#1\I}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\IEND} {\I\END}
5277e290ad70afdf97f359019afd8fb5816f4102Till 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}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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}
5277e290ad70afdf97f359019afd8fb5816f4102Till 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}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LCF}{LCF\xspace}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\newcommand{\ASF}{ASF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\SDF}{SDF\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till 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}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\begin{document}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\title{{\bf \protect{\LARGEHets} User Guide}\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski-- Version 0.50 --}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\author{Till Mossakowski\\[1em]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDepartment of Computer Science\\ and Bremen
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiInstitute for Safe Systems,\\ University of Bremen, Germany.\\[1em]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiComments to: hets-devel@tzi.de
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski\section{Introduction}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe Heterogeneous Tool Set (\protect\Hets) is the main analysis tool
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor the specification language heterogeneous \CASL. Heterogeneous
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\CASL (\HetCASL) combines the specification language \CASL with \CASL extensions
c488ac18796ad6383b1edf7fa2820edc8296c89eChristian Maederand sublanguages, as well as completely different logics and even
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederprogramming languages such as Haskell. \HetCASL
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederextends the structuring mechanisms of \CASL:
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\emph{Basic specifications} are
464c78620a182d2e8fbd125098045eae8788e2bdTill Mossakowskiunstructured specifications or modules written in a specific logic.
12a1614014912501fbfc30a74242d6f3a5c97e80Till MossakowskiThe graph of currently supported logics is shown in Fig.~\ref{fig:LogicGraph},
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand the degree of support by \Hets in Fig.~\ref{fig:Languages}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWith \emph{heterogeneous structured specifications}, it is possible to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicombine and rename specifications, hide parts thereof, and also
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitranslate them to other logics. \emph{Architectural specifications}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiprescribe the structure of implementations. \emph{Specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski libraries} are collections of named structured and architectural
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskispecifications.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\Hets consists of logic-specific tools for the parsing and static
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskianalysis of the different involved logics, as well as a
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskilogic-independent parsing and static analysis tool for structured and
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiarchitectural specifications and libraries. The latter of course needs
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskito call the logic-specific tools whenever a basic specification is
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\section{Logics supported by \Hets}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{figure}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \begin{center}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \includegraphics[scale=0.4]{LogicGraph}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\caption{Graph of logics currently supported by \Hets. The more an
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeellipse is filled, the more stable is the implementation of the logic.}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\label{fig:LogicGraph}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{figure}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{center}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{tabular}{|l|c|c|c|}\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiLanguage & Parser & Static Analysis & Prover \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\CASL & x & x & - \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\CoCASL & x & x & - \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\ModalCASL & x & x & - \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\HasCASL & x & x & - \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiHaskell & x & x & -\\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\CspCASL & (x) & - & - \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski%Structured specifications & x & x & (x) \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski%Architectural specifications & x & x & -\\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\CASLDL & x & - & - \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiOWL DL basic & x & (x) & - \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiOWL DL structure & x & (x) & - \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiSPASS & - & - & x \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiIsabelle & - & - & x \\\hline
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\caption{Current degree of \Hets support for the different languages.\label{fig:Languages}}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{description}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[CASL] extends many sorted first-order logic with partial
30256573a343132354b122097b0ee1215dda1364Till Mossakowski functions and subsorting. It also provides induction sentences,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski expressing the (free) generation of datatypes.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski%It is mainly designed and used for the
30256573a343132354b122097b0ee1215dda1364Till Mossakowski%specification of requirements for software systems. But it is also
30256573a343132354b122097b0ee1215dda1364Till Mossakowski%used for the specification of \Dolce (Descriptive Ontology for
30256573a343132354b122097b0ee1215dda1364Till Mossakowski%Linguistic and Cognitive Engineering), an Upper Ontology for knowledge
30256573a343132354b122097b0ee1215dda1364Till Mossakowski%representation. \cite{Gangemi:2002:SOD} Further it is now used to
30256573a343132354b122097b0ee1215dda1364Till Mossakowski%specify calculi for time and space.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiFor more details on \CASL see \cite{CASL-RM,CASL-UM}.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederWe have implemented the \CASL logic in such a way that much of the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiimplementation can be re-used for \CASL extensions as well; this
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiis achieved via ``holes'' (realized via polymorphic variables) in the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitypes for signatures, morphisms, abstract syntax etc. This eases
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiintegration of \CASL extensions and keeps the effort of integrating
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\CASL extensions quite moderate.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[CoCASL] \cite{MossakowskiEA04} is a coalgebraic extension of \CASL,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisuited for the specification of process types and reactive system.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe central proof method is coinduction.
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski\item[ModalCASL] is an extension of \CASL with multi-modalities and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiterm modalities. It allows the specification of modal systems with
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederKripke's possible worlds semantics. It is also possible to express
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicertain forms of dynamic logic.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[HasCASL] is a higher order extension of \CASL allowing
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski polymorphic datatypes and functions. It is closely related to the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski programming language Haskell and allows program constructs being
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski embedded in the specification.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe language is summarized in \cite{HasCASL/Summary}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThe latter document is also available on the CD-ROM
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[Haskell] is a modern, pure and strongly typed functional
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski programming language. It simultaneously is the implementation
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski language of \Hets, such that in the future, \Hets might be applied
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThe definitive reference for Haskell is \cite{PeytonJones03},
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[CspCASL] \cite{Roggenbach:2003:C-CN} is a combination of \CASL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski with the process algebra CSP.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[OWL DL] is the Web Ontology Language (OWL) recommended by the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski World Wide Web Consortium (W3C, \texttt{http://www.w3c.org}). It is
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder used for knowledge representation and the Semantic Web
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \cite{berners:2001:SWeb}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiHets calls an external OWL DL parser
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski written in JAVA to obtain the abstract syntax for an OWL file and its
5277e290ad70afdf97f359019afd8fb5816f4102Till 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.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill 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
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowskia strongly typed variant of OWL DL in \CASL syntax.
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder \CASL with cardinality restrictions for the description of sorts and
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder unary predicates. The restrictions are based on the equivalence
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder between \CASLDL, OWL~DL and \SHOIN. Compared to \CASL only unary
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder and binary predicates, predefined datatypes and concepts (subsorts
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski of the topsort Thing) are allowed. It is used to bring OWL DL and
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder \CASL closer together.
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder\item[SPASS] \cite{WeidenbachEtAl02} is an automatic theorem prover for first-order logic
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederwith equality.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[Isabelle] \cite{NipPauWen02} is an interactive theorem prover for higher-order
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\end{description}
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederSPASS and Isabelle are the only logics coming with a prover. Proof
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maedersupport for the other logics can be obtained by using logic translations
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskito a prover-supported logic.
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederAn introduction to \CASL can be found in the \CASL User Manual
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder\cite{CASL/UserManual}; the detailed language reference is given in
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithe \CASL Reference Manual \cite{CASL/RefManual}. These documents
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiexplain both the \CASL logic and language of basic specifications as
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiwell as the logic-independent constructs for structured and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiarchitectural specifications. Corresponding documents explaining the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\HetCASL language constructs for \emph{heterogeneous} structured specifications
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiare forthcoming, until then, \cite{Mossakowski:2003:FHS} may serve as a short
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederintroduction. Moreover, the main heterogeneous constructs will be illustrated
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiin Sect.~\ref{sec:HetSpec} below.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\section{Getting started}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe latest \Hets version can be obtained from the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\Hets tools home page
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski 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.
7a8592051724fa46499bde120f44cdc8db270876Till 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)}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederFor 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
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\url{http://www.scriptics.com/software/tcltk/}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiBut Tcl/Tk probably has been already installed
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskion your computer anyway.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiSet the environment variable \texttt{\$UNIWISH} to the wish binary
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski(which is part of Tcl/Tk), and \texttt{\$UNIDAVINCI} to the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederuDraw(Graph) binary. Furthermore, uDraw(Graph) requires that
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\texttt{DAVINCIHOME} is set to the installation directory of
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\subsection*{Isabelle}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiFor theorem proving with Isabelle, you need to install Isabelle,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiwhich is available freely from
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederWe recommend to use the latest version (Isabelle 2005), together
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiwith Proof General, a proof interface that comes with the Isabelle
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidistribution. Proof General uses the Eamcs or Xemacs editor.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiSet the environment variable
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\texttt{\$HETS\_ISABELLE} to the Isabelle (or Emacs, for use with proof general) binary, and set \texttt{\$LC\_CTYPE} to \texttt{C}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\subsection*{SPASS}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiFor theorem proving with SPASS, obtain SPASS freely from
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\subsection*{Libraries of specifications}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiA repository of libraries of specifications for use with \Hets
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiis available under \url{http://www.cofi.info/Libraries}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe environment variable \texttt{HETS\_LIB} should be set to
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskia location where the specification libraries are stored.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder%\QUERY{This should be done by the install script!}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\section{Analysis of Specifications}
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus LuettichConsider the following \CASL
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskispecification:
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{BIGEXAMPLE}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\I\SPEC \NAMEREF{Strict\_Partial\_Order} =
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{ITEMS}[\PRED]
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\I\SORT \( Elem \)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski% \COMMENTENDLINE{\PRED abbreviates predicate}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\(\[ \FORALL x,y,z : Elem \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{COMMENT}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiNote that there may exist \(x, y\) such that\\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskineither \(x < y\) nor \(y < x\).
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\end{BIGEXAMPLE}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\Hets can be used for parsing and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskichecking static well-formedness of specifications.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \index{parsing}%
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \index{static!analysis}%
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \index{analysis, static}%
30256573a343132354b122097b0ee1215dda1364Till MossakowskiLet us assume that the example is in a file named
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\texttt{Order.casl} (actually, this file is provided
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiwith the \Hets distribution).
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThen you can check the well-formedness of the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskispecification by typing (into some shell):
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\Hets checks both the correctness of this specification
30256573a343132354b122097b0ee1215dda1364Till Mossakowski with respect to the \CASL syntax, as
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiwell as its correctness with respect to the static semantics (e.g.\
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiwhether all identifiers have been declared before they are used,
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiwhether operators are applied to arguments of the correct sorts,
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiwhether the use of overloaded symbols is unambiguous, and so on).
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe following flags are available in this context:
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{description}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing -- the static analysis
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[\texttt{-s}, \texttt{--just-structured}]
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederDo the parsing and the static analysis of (heterogeneous) structured
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskispecifications, but leave out the analysis of basic specifications.
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederThis can be used to quickly produce a development graph
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maedershowing the dependencies among the specifications (cf. Sect.~\ref{sec:DevGraph}).
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiUse \texttt{DIR} as the directory for specification libraries
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder(equivalently, you can set the variable \texttt{HETS\_LIB} before
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maedercalling \Hets).
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[\texttt{--casl-amalg=ANALYSIS}]
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder For the analysis of architectural specification (a quite advanced
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski amalgamability checking
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder algorithm for \CASL logic; it is a comma-separated list of zero or
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder more of the following options:
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder \begin{description}
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder \item[\texttt{sharing}] perform sharing analysis for sorts,
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder operations and predicates.
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder \item[\texttt{cell}] perform cell condition check; implies
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder \texttt{sharing}. With this option on the subsort embeddings are
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder \item[\texttt{colimit-thinness}] perform colimit thinness check;
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder implies \texttt{sharing}. The colimit thinness check is less
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder complete and usually takes longer than the full cell condition
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski check (\texttt{cell} option), but may prove more efficient in case
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski of certain specifications.
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder \end{description}
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder If \texttt{ANALYSIS} is empty then amalgamability analysis for
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder \CASL is skipped.
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder The default value for \texttt{--casl-amalg} is
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder \texttt{cell}.
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\end{description}
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\section{Heterogeneous Specification} \label{sec:HetSpec}
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\Hets accepts plain text input files with the following endings:\\
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\begin{tabular}{|l|c|c|}\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiEnding & default logic & structuring language\\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\texttt{.casl} & \CASL & \CASL \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\texttt{.het} & \CASL & \CASL \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\texttt{.hs} & Haskell/HasSLe & Haskell\\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\texttt{.owl} & OWL DL, OWL Lite & OWL\\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederAlthough the endings \texttt{.casl} and \texttt{.het} are
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederinterchangeable, the former should be used for libraries of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskihomogeneous \CASL specifications and the latter for \HetCASL libraries
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiof heterogeneous specifications (that use the \CASL structuring
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiconstructs). Within a \HetCASL library, the current logic can be changed e.g.\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederto \HasCASL in the following way:
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{verbatim}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till 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;
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederthese are then automatically translated along the default
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederembedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski(Heterogeneous constructs
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskifor explicit translations between logics will be made available
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskiin the future.)
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiA \CspCASL specification consists of a \CASL specification
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskifor the data part and a \Csp process built over this data part.
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiTherefore, \HetCASL provides a heterogeneous language construct
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\texttt{data} as follows:
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\begin{verbatim}
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskilibrary Buffer
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski free type List[Elem] ::= nil | cons(Elem; List[Elem])
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder channel read, write : Elem
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski let Buf(l:List[Elem]) =
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski read?x -> Buf( cons(x,nil) )
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski [] if l=nil then STOP else write!last(l) -> Buf( rest(l) )
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\end{verbatim}
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiHere, the construct \texttt{data List} refers to the \CASL specification
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\texttt{List}, which is implicitly embedded into \CspCASL.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe ending \texttt{.hs} is available for directly reading in
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiHaskell programs and HasSLe specifications,
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederand hence supports the Haskell module system.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskithe logic Haskell has to be chosen explicitly, and the \CASL structuring
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisyntax needs to be used:
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\begin{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilibrary Factorial
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederspec Factorial =
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederfac :: Int -> Int
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederfac n = foldl (*) 1 [1..n]
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\end{verbatim}
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederNote that according to the Haskell syntax, Haskell function
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederdeclarations and definitions need to start with the first column of
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\section{Development Graphs}\label{sec:DevGraph}
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederDevelopment graphs are a simple kernel formalism for (heterogeneous)
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederstructured theorem proving and proof management. A development graph
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederconsists of a set of nodes (corresponding to whole structured
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispecifications or parts thereof), and a set of arrows called
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidefinition links, indicating the dependency of each involved
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskistructured specification on its subparts. Arising proof obligations
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiare attached as so-called theorem links to this graph.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe following options let \Hets show the development graph of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskia specification library:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\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:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{EXAMPLE}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill 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) \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \. \neg x < 0 \\
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder \. suc(x) < suc(y) \IFF x < y
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{EXAMPLE}%[\SLIDESMALL]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{Natural\_Order\_2} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I{} \( Elem \MAPSTO Nat\)
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAgain, these specifications can be checked with \Hets. However, this
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskionly checks syntactic and static semantic well-formedness -- it is
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederby a strict partial ordering relation. Checking this requires theorem
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiproving, which will be discussed below.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiHowever, before coming to theorem proving, let us first inspect the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiproof obligations arising from a specification. This can be done with:
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\texttt{hets -g Order.casl}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski(assuming that the above two specifications and the view
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederhave been added to the file
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\Hets now displays a so-called development graph
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski(which is just an overview graph showing the overall structure
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiof the specifications in the library), see Fig.~\ref{fig:dg0}.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\begin{figure}
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\begin{center}
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\includegraphics[scale=0.7]{dg-order-0}
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\caption{Sample development graph.\label{fig:dg0}}
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiNodes in a development graph correspond to \CASL specifications.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiArrows show how specifications are related by the structuring
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe black arrow denotes an ordinary import of
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskispecifications (generated by the extension), while the red arrow
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskidenotes a proof obligation (corresponding to the view).
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThis proof obligation needs to be discharged in order to
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskishow that the view is well-formed (then its color turns into green).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAs a more complex example, consider the following loose specification
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiof a sorting function, taken from the \CASL User Manual
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{BIGEXAMPLE}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\I\SPEC \NAMEREF{List\_Order\_Sorted}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{ITEMS}[\WITHIN]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{ITEMS}[\PRED]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\I\PRED \( \_\_is\_sorted : List \)
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\(\[ \FORALL e,e': Elem; L : List \\
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder \. empty~is\_sorted \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \. cons(e,empty)~is\_sorted \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \. cons(e,cons(e',L))~is\_sorted \IFF
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\begin{ITEMS}[\OP]
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\I\OP \( order : List \TOTAL List \)
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{BIGEXAMPLE}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe following specification of sorting by insertion also is taken from
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithe \CASL User Manual \cite{CASL/UserManual}, Chap.~6:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{BIGEXAMPLE}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\I\SPEC \NAMEREF{List\_Order}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\phantomsection
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{ITEMS}[\WITHIN]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{ITEMS}[\OP]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\I\OP \( insert : Elem \* List \TOTAL List \)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\(\[ \FORALL e,e':Elem; L:List \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. insert(e, empty) = cons(e, empty) \\
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski \. insert(e, cons(e',L)) = \[ cons(e', insert(e,L)) \WHEN e' < e\\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \ELSE cons(e, cons(e',L)) \] \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{ITEMS}[\OP]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\OP \( order : List \TOTAL List \)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\(\[ \FORALL e:Elem; L:List \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. order(empty) = empty \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \. order(cons(e,L)) = insert(e, order(L)) \]\)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{BIGEXAMPLE}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiBoth specifications are related. To see this, we first inspect
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskitheir signatures. This is possible with:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{hets -g Sorting.casl}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiassuming that \texttt{Sorting.casl} contains the above specifications.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{figure}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{center}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\includegraphics[scale=0.7]{dg-order-1}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\caption{Development graph for the two sorting specifications.\label{fig:dg1}}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiIn the above-mentioned development graph, we have two types of nodes.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiThe named ones correspond to named specifications, but there
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiare also unnamed nodes corresponding to anonymous basic
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecifications like the declaration of the $insert$ operation in
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\NAMEREF{List\_Order} above. Basically, there is an
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill Mossakowskiunnamed node for each structured specification that is not named.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiAgain, the black arrows denote an ordinary import of specifications
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski(corresponding to the extensions and unions in the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecifications), while the blue arrows denote hiding (corresponding to
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithe local specification).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiBy clicking on the nodes, one can inspect their signatures.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiIn this way, we can see that both \NAMEREF{List\_Order\_Sorted} and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order} have the same signature. Hence, it
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiis legal to add a view:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{EXAMPLE}%[\SLIDESMALL]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\I\VIEW \NAMEDEFN{v2}[\NAMEREF{Total\_Order}] ~:~ \NAMEREF{List\_Order\_Sorted}[\NAMEREF{Total\_Order}] \TO
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\NAMEREF{List\_Order}[\NAMEREF{Total\_Order}]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiWe have already added this view to \texttt{Sorting.casl}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe corresponding
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiproof obligation between \NAMEREF{List\_Order\_Sorted} and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\NAMEREF{List\_Order} is displayed in Fig.~\ref{fig:dg1}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski as a red arrow.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHere is a summary of the types of nodes and links occurring in
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederdevelopment graphs:
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{description}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[Named nodes] correspond to a named specification.
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[Unnamed nodes] correspond to an anonymous specification.
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[Elliptic nodes] correspond to a specification in the current library.
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[Rectangular nodes] are external nodes corresponding
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski to a specification downloaded from
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskianother library.
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[Black links] correspond to reference to other specifications
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski(definition links in the sense of \cite[IV:4]{CASL/RefManual}).
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[Blue links] correspond to hiding (hiding definition links).
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[Red links] correspond to open proof obligations (theorem links).
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[Green links] correspond to proved proof obligations (theorem links).
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[Solid links] correspond to global (definition or theorem)
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskilinks in the sense of \cite[IV:4]{CASL/RefManual}.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Dashed links] correspond to local (definition or theorem) links in the sense of \cite[IV:4]{CASL/RefManual}.
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\end{description}
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiWe now explain the menus of the development graph window.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiMost of the pull-down menus of the window are uDraw(Graph)-specific
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskitheir function can be looked up in the uDraw(Graph) documentation.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe exception is the Edit menu. Moreover, the nodes and links
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiof the graph have attached pop-up menus, which appear when
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiclicking with the right mouse button.
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{description}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[Edit] This menu has two submenus:
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{description}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[Unnamed nodes]
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiThe ``Hide/show names'' menu is a toggle:
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiyou can switcn on or off the display of names for nodes that
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiare initially unnamed. The newly named nodes get names that
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiare derived from named neighbour nodes.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiWith the ``Hide nodes'' submenu, it is possible
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskito reduce the complexity of the graph by hiding all unnamed nodes;
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskionly nodes corresponding to named specifications remain displayed.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiPaths between named nodes going through unnamed nodes
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiare displayed as links. With the ``Show nodes'' submenu, the unnamed
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskinodes re-appear.
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[Proofs] This menu allows to apply some of the deduction rules
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski for development graphs, see Sect. IV:4.4 of the \CASL Reference
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski Manual \cite{CASL/RefManual}. While support for local and global
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (definition or theorem) links is stable, support for hiding links
30256573a343132354b122097b0ee1215dda1364Till Mossakowski and checking conservativity is still experimental. In most cases, it is
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski advisable to use ``Automatic'', which automatically applies the
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski rules in the correct order. As a result, the the open theorem links
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (marked in red) will be reduced to local proof goals, that is, they
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski become green, and instead, some of the node will get red, indicating
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder open local proof goals.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Pop-up menu for nodes]
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederHere, the number of submenus depends on the type of the node:
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\begin{description}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Show signature] Shows the signature of the node.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Show local axioms] Shows the local axioms of the node.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Show theory] Shows the theory of the node (including axioms
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederimported from other nodes). Warning: axioms imported via hiding links
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederare not part of the theory; they can be made visible only by re-adding
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederthe hidden symbols, using the proof rule \emph{Theorem-Hide-Shift}.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Translate theory] Translates the theory of a node to another logic.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederA menu with the possible translation paths will be displayed.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Show taxonomy graphs] (Only available for some logics) Shows the subsort graph of the signature of the node.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show sublogic] Shows the logic and, within that logic, the minimal sublogic
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifor the signature and the axioms of the node.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show origin] Shows the kind of \CASL structuring construct that
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiled to the node.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Prove] Try to prove the local proof goals.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedertheory 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.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\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])
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\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}]
5277e290ad70afdf97f359019afd8fb5816f4102Till 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)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe default is \texttt{dg.taf}, which means that the development
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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}).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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 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 Mossakowski\item[\texttt{-r RAW} or \texttt{--raw=RAW}] This option allows one
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito influence the formatting in more detail.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHere, \texttt{RAW} is \texttt{(ascii|text|(la)?tex)=STRING},
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowskiand \texttt{STRING} is passed to the appropriate pretty-printer.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe deatils of these options are to be fixed in the future only.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe other output formats are for future usage.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Miscellaneous Options}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-v[Int]}, \texttt{--verbose[=Int]}]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiSet the verbosity level according to \texttt{Int}. Default is 1.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-q}, \texttt{--quiet}]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBe quiet -- no diagnostic output at all. Overrides -v.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-V}, \texttt{--version}] Print version number and exit.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-h}, \texttt{--help}, \texttt{--usage}]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiPrint usage information and exit.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{+RTS -KIntM -RTS}] Increase the stack size to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \texttt{Int} megabytes (needed in case of a stack overflow).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThis must be the first option.
5277e290ad70afdf97f359019afd8fb5816f4102Till 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}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidecelation. The default is \CASL.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-n SPECS}, \texttt{--spec=SPECS}]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskichooses a list of named specifications for processing
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Limits of \Hets}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets is still intensively under development. In particular, the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifollowing points are still missing:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{itemize}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item There is no proof support for architectural specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item Distributed libraries are always downloaded from the local disk,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskinot from the Internet.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item Version numbers of libraries are not considered properly.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item The proof engine for development graphs provides only experimental
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisupport for hiding links and for conservativity.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Architecture of \Hets}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets is written in Haskell. Its parser uses combinator
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{parsing}%
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe user-defined (also known as ``mixfix'') syntax of \CASL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicalls for a two-pass approach. In the first pass, the skeleton of a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\CASL abstract syntax tree is derived, in order to extract user-defined
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedersyntax rules. In a second pass, which is performed during
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskianalysis, these syntax rules are used to parse
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiany expressions that
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiuse mixfix notation. The output is stored in the so-called
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{ATerms}%
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederATerm format \cite{BJKO00}, which is used as interchange format
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor interfacing with other tools.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets provides an abstract interface for
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{institution!independence}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{independence, institution}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinstitutions, so
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithat new logics can be integrated smoothly.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederIn order to do so, a parser,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskia static checker and a prover for basic specifications in the logic have
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito be provided.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{figure}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder%\includegraphics[scale=0.44]{hets}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\caption{Architecture of the heterogeneous tool set.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\label{fig:hets}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe architecture of \Hets is shown in Fig.~\ref{fig:hets}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiIf your favourite logic is missing in \Hets, please tell us
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(hets@tzi.de). We will take account your feedback when deciding which
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederlogics and proof tools to integrate next into \Hets. Help with
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederintegration of more logics and proof tools into \Hets is also welcome.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\Hets is mainly maintained by
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiChristian Maeder (maeder@tzi.de) and Till Mossakowski
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder(till@tzi.de). The mailing list is \url{hets@tzi.de},
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederthe homepage is
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\url{http://www.informatik.uni-bremen.de/mailman/listinfo/hets-devel}.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\paragraph{Acknowledgement}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederThe heterogeneous tool set \Hets, which shows that the theory outlined
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederin this work can also be brought to practice, would not have possible
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederwithout cooperation with Christian Maeder and Klaus L\"uttich.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederBesides the author, the following people have been involved
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederin the implementation of \Hets:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiKatja Abu-Dib,
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederCarsten Fischer,
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederJorina Freya Gerken,
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederSonja Gr\"{o}ning,
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederWiebke Herding,
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederTina Krausser,
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederMartin K\"{u}hl,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiKlaus L\"{u}ttich,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiChristian Maeder,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiMaciek Makowski,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiDaniel Pratsch,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiFelix Reckers,
30256573a343132354b122097b0ee1215dda1364Till MossakowskiMarkus Roggenbach,
30256573a343132354b122097b0ee1215dda1364Till MossakowskiPascal Schmidt and
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiPaolo Torrini.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Hets has been built based on experiences with its
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \index{Cats@\Cats}%
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \index{Maya@\MAYA}%
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuThe \CASL Tool Set (\Cats)
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\cite{Mossakowski:2000:CST,Mossakowski:1998:SSA}
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiprovides parsing and static analysis for \CASL.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuIt has been developed by the present author with help
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuof Mark van den Brand, Kolyang, Bartek Klin, Pascal Schmidt and
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederFrederic Voisin.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\MAYA \cite{Autexier:2002:IHD,AutexierEtal02} is a proof management
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescutool based on development graphs. \MAYA only supports development
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescugraphs without hiding and without logic translations. \MAYA has been
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskideveloped by Serge Autexier and Dieter Hutter.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuI also want to thank Agn\`es Arnould, Thibaud Brunet, Pascale LeGalle,
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuKathrin Hoffmann, Katiane Lopes, Klaus L\"uttich, Christian Maeder,
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuStefan Merz, Maria Martins Moreira, Christophe
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuRingeissen, Markus Roggenbach, Dmitri Schamschurko, Lutz Schr\"oder,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiKonstantin Tchekine and Stefan W\"olfl
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederfor giving feedback about \Cats, HOL-CASL and \Hets. Finally,
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuspecial thanks to Christoph L\"uth and George Russell
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescufor help with connecting \Hets to their UniForM workbench.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\bibliographystyle{plain}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\bibliography{cofibib,cofi-ann,UM,hets,kl}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\end{document}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder%%% Local Variables:
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu%%% mode: latex
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder%%% TeX-master: "UserGuide"