UserGuide.tex revision 5277e290ad70afdf97f359019afd8fb5816f4102
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\documentclass{article}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{alltt}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{casl}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% SIMULATING SMALL-CAPS FOR BOLD, EMPH
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
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 {\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%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LCF}{LCF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\ASF}{ASF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SDF}{SDF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% Do NOT use \ASF+\SDF (it gives a superflous 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{\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\begin{document}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\title{{\bf \Hets User Guide}\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski-- Version 0.3 --}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\author{Till Mossakowski\\[1em]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDepartment of Computer Science\\ and Bremen
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiInstitute for Safe Systems,\\ University of Bremen, Germany.\\[1em]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiComments to: hets@tzi.de
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Introduction}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe Heterogeneous Tool Set (\protect\Hets) is the main analysis tool
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor the specification language heterogeneous \CASL. Heterogeneous
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\CASL combines the specification langauage \CASL with \CASL extensions
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand sublanguages, as well as comletely different logics and even
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiprogramming languages such as Haskell. Heterogeneous \CASL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiextends the strucruting mechanisms of \CASL:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{Basic specifications} are
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiunstructured specifications or modules written in a specific logic.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(The graph of currently supported logics is shown in Fig.~\ref{fig:LogicGraph}.)
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 Mossakowskiprecsribe the structure of implementations.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{Specification libraries} are collections of named structured
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand architectural specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets consists of logic-specific tools for the parsing and static
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskianalysis of the different involved logics, as well as a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogic-independent parsing and static analysis tool for structured and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiarchitectural specifications and libraries. The latter of course needs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito call the logic-specific tools whenever a basic specification is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Text{Haskell}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Text{\HasCASL}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Text{\CspCASL} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Graph of logics currently supported by \Hets.\label{fig:LogicGraph}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Getting started}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe latest \Hets version can be obtained from the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\CoFI tools home page \cite{CoFITools}. Since \Hets is being
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiimproved constantly, it is recommended always to use the latest version.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets currently is available for Linux, Solaris and
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThis README belongs to a Hets release (and does not apply to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisources directly obtained via cvs).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe aim of this release is a binary "hets" that is able to analyse
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiheterogeneous and in particular CASL specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe output of hets, if the input is successfully accepted, can be
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidisplayed by "daVinci".
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskidaVinci is maintained by b-novative and b-novative holds all rights.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThis release may be accompanied with free binary releases of daVinci
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiVersion 2.1, but daVinci 2.1 is no longer supported or maintained!
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHowever, you are encouraged to obtain the latest version of daVinci
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiPresenter (currently 3.0.5) from http://www.b-novative.com that is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifree for academic purposes.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiLinux: the linux binary release of daVinci 2.1 relies on the old
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskishlibs5 that must be installed on your system (if ./daVinci cannot be
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifound/executed, then shlibs5 are missing)
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiSolaris: the solaris binary release of daVinci 2.1 should work without
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiMacintosh (Darwin): there is no release of daVinci for Macintosh, but
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskib-novative may have one in the mean time
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor best quality, get the latest version of daVinci from b-novative.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor hets to find daVinci, the environment variables DAVINCIHOME and
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiUNIDAVINCI must be set to the installation directory of daVinci and to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe actual executable, respectively.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiexport DAVINCIHOME=<path>/daVinci_V2.1
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiexport UNIDAVINCI=<path>/daVinci_V2.1/daVinci
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiA typical call of hets is then: <path>/hets -g Basic/Numbers.casl
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Analysis of Specifications}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiConsider the first example in this book:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{Strict\_Partial\_Order} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\PRED]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SORT \( Elem \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% \COMMENTENDLINE{\PRED abbreviates predicate}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL x,y,z : Elem \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{COMMENT}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiNote that there may exist \(x, y\) such that\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskineither \(x < y\) nor \(y < x\).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\POINT{\protect\Hets can be used for parsing and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskichecking static well-formedness of specifications.}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{parsing}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{static!analysis}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{analysis, static}%
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiLet us assume that the example is in a file named
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{Order.casl} (actually, this file is provided on the web
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand on the CD-ROM coming with this volume).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThen you can check the well-formedness of the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispecification by typing (into some shell):
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets checks both the correctness of this specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski with respect to the \CASL syntax, as
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwell as its correctness with respect to the static semantics (e.g.\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhether all identifiers have been declared before they are used,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhether operators are applied to arguments of the correct sorts,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhether the use of overloaded symbols is unambiguous, and so on).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski -p --just-parse skip static analysis - just parse
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski -s --just-structured skip basic analysis - just do structured analysis
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski -L DIR --casl-libdir=DIR CASL library directory
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Heterogeneous Specification}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Formatting}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIt is also possible to generate a pretty printed \LaTeX\ version
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof \texttt{Order.casl} by typing:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski -r RAW --raw=RAW raw options passed to the pretty-printer
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski RAW is (ascii|text|(la)?tex)=STRING where STRING is passed to the appropiate pretty-printer
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Development Graphs}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski -g --gui show graphical output in a GUI window
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski -G --only-gui show graphical output in a GUI window - don't write Output to file
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiOne use of \texttt{Order.casl} might be to express the fact that
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe natural numbers form a strict partial order as a view, as follows:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{EXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEDEFN{Natural\_Order\_2} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{Natural}} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\PRED \( \_\_<\_\_ : Nat \* Nat\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL x,y:Nat \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. 0 < suc(x) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. \neg x < 0 \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. suc(x) < suc(y) \IFF x < y
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{EXAMPLE}%[\SLIDESMALL]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{Natural\_Order\_2} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I{} \( Elem \MAPSTO Nat\)
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAgain, these specifications can be checked with \Hets. However, this
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskionly checks syntactic and static semantic well-formedness -- it is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiby a strict partial ordering relation. Checking this requires theorem
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproving, which will be discussed below.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\POINT{\protect\Hets also displays and manages
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof obligations, using development graphs.}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{proof!obligation}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{development graph}%
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHowever, before coming to theorem proving, let us first inspect the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof obligations arising from a specification. This can be done with:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{hets -g Order.casl}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(assuming that the above two specifications and the view
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskihave been added to the file
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets now displays a so-called development graph
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(which is just an overview graph showing the overall structure
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof the specifications in the library), see Fig.~\ref{fig:dg0}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{center}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\includegraphics[scale=0.7]{dg-order-0}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Sample development graph.\label{fig:dg0}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\POINT{Nodes in a development graph correspond to \CASL specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiArrows show how specifications are related by the structuring
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe solid arrow denotes an ordinary import of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispecifications (generated by the extension), while the dashed\FOOTNOTE
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski{Actually, the dashed arrow will be displayed as solid and in red by \Hets;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwe do not have colors available here.} arrow
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidenotes a proof obligation (corresponding to the view).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThis proof obligation needs to be discharged in order to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskishow that the view is well-formed.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAs a more complex example, consider the following loose specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof a sorting function, taken from Chap.~\ref{UM--structuring}:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{List\_Order\_Sorted}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\WITHIN]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\PRED]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\PRED \( \_\_is\_sorted : List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL e,e': Elem; L : List \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. empty~is\_sorted \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. cons(e,empty)~is\_sorted \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. cons(e,cons(e',L))~is\_sorted \IFF
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\OP \( order : List \TOTAL List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following specification of sorting by insertion also is taken from
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiChap.~\ref{UM--structuring}:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{List\_Order}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\phantomsection
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\WITHIN]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\OP \( insert : Elem \* List \TOTAL List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL e,e':Elem; L:List \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. insert(e, empty) = cons(e, empty) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. insert(e, cons(e',L)) = \[ cons(e', insert(e,L)) \WHEN e' < e\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ELSE cons(e, cons(e',L)) \] \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\OP \( order : List \TOTAL List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL e:Elem; L:List \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. order(empty) = empty \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. order(cons(e,L)) = insert(e, order(L)) \]\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBoth specifications are related. To see this, we first inspect
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitheir signatures. This is possible with:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{hets -g Sorting.casl}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiassuming that \texttt{Sorting.casl} contains the above specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{center}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\includegraphics[scale=0.7]{dg-order-1}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Development graph for the two sorting specifications.\label{fig:dg1}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\POINT{Internal nodes in a development graph correspond
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito unnamed parts of a structured specification.}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn the above-mentioned development graph, we have two types of nodes.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe named ones correspond to named specifications, but there
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiare also unnamed nodes corresponding to anonymous basic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispecifications like the declaration of the $insert$ operation in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order} above. Basically, there is an
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinternal node for each structured specification that is not named.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAgain, the simple solid arrows denote an ordinary import of specifications
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(corresponding to the extensions and unions in the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispecifications), while the double 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 dotted arrow.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NOPOINT{Proof obligations can be discharged in various ways.}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTrivial proof obligations can be discharged
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiby \Hets alone using the ``Proofs'' menu.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe proof obligation in Fig.~\ref{fig:dg1},
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiindicated by the lower dotted
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiarrow between \NAMEREF{List\_Order\_Sorted} and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order}, states that insertion sort,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskias defined by the operation \(order\) in \NAMEREF{List\_Order},
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiactually has the properties of a sorting algorithm. Here, one has to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskichoose a theorem prover that
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis to be used to discharge the proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiobligation, which is then done by using commands specific to the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitheorem prover (cf. e.g.\ Section~\ref{sec:HOLCASL}). Alternatively,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskione can state that one just conjectures the obligation to be true.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn order to be able to tackle proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiobligations occurring in (statically well-formed) specifications, \Hets
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis interfaced with various logic-specific theorem proving, rewriting
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand consistency checking tools. On top of this, there is a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogic-independent proof engine called \MAYA, which manages the proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiobligations. \MAYA uses so-called \emph{development graphs}, a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskigraphical representation of \CASL structured specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Input, Output}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski -i ITYPE --input-type=ITYPE ITYPE of input file:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (tree.)?gen_trm(.baf)? | het(casl)? | casl | ast(.baf)?
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski -O DIR --output-dir=DIR destination directory for output files
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski -o OTYPES --output-types=OTYPES OTYPES of output files, a comma seperated list of OTYPE
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski OTYPE is (pp.(het|tex|html))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |(ast|[fh]?dg(.nax)?).(het|trm|taf|html|xml)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |(graph.(dot|ps|davinci))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Miscellaneous Options}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski -v[Int] --verbose[=Int] chatty output to stderr
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski -q --quiet no output at all to stderr. overrides --verbose!
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski -V --version print version number and exit
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski -h --help, --usage print usage information and exit
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
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisyntax rules. In a second pass, which is performed during
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskianalysis, these syntax rules are used to parse
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiany expressions that
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiuse mixfix notation. The output is stored in the so-called
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{ATerms}%
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiATerm format \cite{BJKO00}, which is used as interchange format
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor interfacing with other tools.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets provides an abstract interface for
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{institution!independence}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{independence, institution}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinstitutions, so
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithat new logics can be integrated smoothly.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn order to do so, a parser,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskia static checker and a prover for basic specifications in the logic have
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito be provided.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\includegraphics[scale=0.44]{hets}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Architecture of the heterogeneous tool set.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{fig:hets}}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe architecture of \Hets is shown in Fig.~\ref{fig:hets}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIf your favourite logic is missing in \Hets, please tell us
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(hets@tzide.). We will take account your feedback when deciding which
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogics and proof tools to integrate next into \Hets. Help with
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiintegration of more logics and proof tools into \Hets is also welcome.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets< is mainly maintained by
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiChristian Maeder (maeder@tzi.de) and Till Mossakowski
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(till@tzi.de). The mailing list is hets@tzi.de.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Precursors of \Hets}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets has been built based on experiences with its
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{Cats@\Cats}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{Maya@\MAYA}%
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe \CASL Tool Set (\Cats)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{Mossakowski:2000:CST,Mossakowski:1998:SSA}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicomes with roughly the same analysis tools as \Hets.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%but neither supports extensions nor does it identify
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%sublanguages of \CASL (and the tools to be used with
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%sublanguages only).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe management of development graphs is not integrated
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskibut is provided with a stand-alone version of the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitool \MAYA \cite{Autexier:2002:IHD,AutexierEtal02}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%(which only supports part of \CASL's
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%structuring constructs; in particular, hiding is not supported).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Cats and \MAYA
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%are mainly important in the current transition phase,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%since \Hets does not support full \CASL (e.g. architectural
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%specifications) yet.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski can be obtained from the \CoFI tools home page \cite{CoFITools}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{document}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% Local Variables:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% mode: latex
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% TeX-master: "UserGuide"