UserGuide.tex revision a8ce558d09f304be325dc89458c9504d3ff7fe80
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\documentclass{article}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{alltt}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{casl}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{color}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\QUERY}[1]%{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\eat}[1]{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\IEXT}[1] {\\#1\I}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\IEND} {\I\END}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{EXAMPLEFORMAT} {}{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%% Added by MB to have some extra vertical space after the ``main'' examples
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%% following the points (and some others in the text):
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{BIGEXAMPLE} {\begin{EXAMPLE}} {\end{EXAMPLE}\medskip}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{DETAILSFORMAT} {}{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{META}[1][] {#1\begin{METAFORMAT}}{\end{METAFORMAT}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{METAFORMAT} {\medskip\vrule\hspace{1ex}\vrule\hspace{1ex}%
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \begin{minipage}{0.9\textwidth}\it}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski {\end{minipage}\par\medskip}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\SLIDESMALL} {}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\SLIDESONLY}[1] {}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% SIMULATING SMALL-CAPS FOR BOLD, EMPH
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%\newcommand {\CoFI}{CoFI\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeELAN} {\largeTEXTSC{E}{LAN}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HOL}{\normalTEXTSC{H}{OL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Isabelle}{\normalTEXTSC{I}{SABELLE}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LCF}{LCF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\ASF}{ASF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SDF}{SDF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski%% Do NOT use \ASF+\SDF (it gives a superfluous space in the middle)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CCC}{CCC\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CoCASL}{\normalTEXTSC{C}{O}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CspCASL}{\normalTEXTSC{C}{SP}-\normalTEXTSC{C}{ASL}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{document}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\title{{\bf \protect{\LARGEHets} 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
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\CASL (\HetCASL) combines the specification language \CASL with \CASL extensions
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowskiand sublanguages, as well as completely different logics and even
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiprogramming languages such as Haskell. \HetCASL
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowskiextends the structuring mechanisms of \CASL:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{Basic specifications} are
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiunstructured specifications or modules written in a specific logic.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe graph of currently supported logics is shown in Fig.~\ref{fig:LogicGraph},
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill 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}
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowskiprescribe the structure of implementations. \emph{Specification
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski libraries} are collections of named structured and architectural
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets consists of logic-specific tools for the parsing and static
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskianalysis of the different involved logics, as well as a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogic-independent parsing and static analysis tool for structured and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiarchitectural specifications and libraries. The latter of course needs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito call the logic-specific tools whenever a basic specification is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Text{Haskell}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Text{\HasCASL}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Text{\CspCASL} \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Text{\CASL} \ar[u] \ar[ur]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Graph of logics currently supported by \Hets.\label{fig:LogicGraph}}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{figure}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{tabular}{|l|c|c|c|}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiLanguage & Parser & Static Analysis & Prover \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\CASL & x & x & - \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\HasCASL & x & (x) & - \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHaskell & x & x & -\\\hline
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\CspCASL & (x) & - & - \\\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiStructured specifications & x & x & (x) \\\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiArchitectural specifications & x & - & -\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\caption{Current degree of \Hets support for the different languages.\label{fig:Languages}}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiAn introduction to \CASL can be found in the \CASL User Manual
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\cite{CASL/UserManual}; the detailed language reference is given in
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithe \CASL Reference Manual \cite{CASL/RefManual}. These documents
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiexplain both the \CASL logic and language of basic specifications as
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiwell as the logic-independent constructs for structured and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiarchitectural specifications. Corresponding documents explaining the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\HetCASL language constructs for \emph{heterogeneous} structured specifications
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiare forthcoming, until then, \cite{Mossakowski:2003:FHS} may serve as a short
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiintroduction. Moreover, the main heterogeneous constructs will be illustrated
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiin Sect.~\ref{sec:HetSpec} below.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiAn overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithe language is summarized in \cite{HasCASL/Summary}.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiThe latter document is also available on the CD-ROM
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe definitive reference for Haskell is \cite{PeytonJones03},
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisee also \url{www.haskell.org}. An introduction to \CspCASL
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiis given in \cite{Roggenbach:2003:CCN}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Getting started}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe latest \Hets version can be obtained from the
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\CoFI tools home page
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski Since \Hets is being
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiimproved constantly, it is recommended always to use the latest version.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets currently is available for Linux, Solaris and
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiMac OS-X. You can either start the script \texttt{Tools/Hets/hets}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski(the script automatically finds the binary for your architecture).
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiOr you can install \Hets on your local file system by \texttt{cd}ing
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskiinto \texttt{Tools/Hets}on the CD-ROM and then calling
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\texttt{./install <dir>}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskiwhere \texttt{<dir>} is an existing directory where \Hets should be
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiMacIntosh users need to install some libraries from
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski tar xzf Haskell-libs.tgz -C /Library/Frameworks
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiThe \texttt{install} script installs these automatically for you.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiNote that you may have to be \texttt{root} in order to be able to
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski%After downloading your platform specific distribution,
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski%you have to unpack it as follows (note that the filenames will
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski%be slightly different, depending on your platform):
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski%\begin{verbatim}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski%tar zxf hets.tgz # gtar under Solaris
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski%\end{verbatim}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiIf you want to compile \Hets from the sources, please follow the
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskiinstructions of the \texttt{Tools/Hets/src/INSTALL} file.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\subsection*{daVinci}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiFor the display of development graphs, \Hets uses 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
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill 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
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiPresenter (currently 3.0.5) from \url{http://www.b-novative.com}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiIt needs a license key, but is free for academic purposes.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till 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)
a8ce558d09f304be325dc89458c9504d3ff7fe80Till 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.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\subsection*{Environment variables}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiThe script in \texttt{Tools/Hets/hets} sets the following environment
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiFor \Hets to find daVinci, the environment variables \texttt{DAVINCIHOME} and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{UNIDAVINCI} 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}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe environment variable \texttt{HETS\_LIB} should be set to
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskia location where specification libraries are stored. By default,
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskiit is set to the \texttt{Libraries} directory on the CD-ROM
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski(or the corresponding copy on your local file system).
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski%\QUERY{This should be done by the install script!}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Analysis of Specifications}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiConsider the following \CASL
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecification:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{Strict\_Partial\_Order} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\PRED]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SORT \( Elem \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% \COMMENTENDLINE{\PRED abbreviates predicate}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL x,y,z : Elem \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{COMMENT}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiNote that there may exist \(x, y\) such that\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskineither \(x < y\) nor \(y < x\).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets can be used for parsing and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskichecking static well-formedness of specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{parsing}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{static!analysis}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{analysis, static}%
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiLet us assume that the example is in a file named
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{Order.casl} (actually, this file is provided
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiwith the \Hets distribution).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThen you can check the well-formedness of the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispecification by typing (into some shell):
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets checks both the correctness of this specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski with respect to the \CASL syntax, as
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwell as its correctness with respect to the static semantics (e.g.\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhether all identifiers have been declared before they are used,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhether operators are applied to arguments of the correct sorts,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhether the use of overloaded symbols is unambiguous, and so on).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe following flags are available in this context:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing -- the static analysis
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-s}, \texttt{--just-structured}]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiDo the parsing and the static analysis of (heterogeneous) structured
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecifications, but leave out the analysis of basic specifications.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThis can be used to quickly produce a development graph
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskishowing the dependencies among the specifications (cf. Sect.~\ref{sec:DevGraph}).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiUse \texttt{DIR} as the directory for specification libraries
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(equivalently, you can set the variable \texttt{HETS\_LIB} before
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskicalling \Hets).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Heterogeneous Specification} \label{sec:HetSpec}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Hets accepts plain text input files with the following endings:\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{tabular}{|l|c|c|}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiEnding & default logic & structuring language\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.casl} & \CASL & \CASL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.het} & \CASL & \CASL \\\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\texttt{.hs} & Haskell & Haskell\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiAlthough the endings \texttt{.casl} and \texttt{.het} are
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinterchangeable, the former should be used for libraries of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskihomogeneous \CASL specifications and the latter for \HetCASL libraries
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiof heterogeneous specifications (that use the \CASL structuring
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiconstructs). Within a \HetCASL library, the current logic can be changed e.g.\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskito \HasCASL in the following way:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe subsequent specifications are then parsed and analysed as
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\HasCASL specifications. Within such specifications,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiit is possible to use references to named \CASL specifications;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithese are then automatically translated along the default
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiembedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(Heterogeneous constructs
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifor explicit translations between logics will be made available
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiin the future.)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiA \CspCASL specification consists of a \CASL specification
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifor the data part and a \Csp process built over this data part.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiTherefore, \HetCASL provides a heterogeneous language construct
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{data} as follows:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilibrary Buffer
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski free type List[Elem] ::= nil | cons(Elem; List[Elem])
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski channel read, write : Elem
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski let Buf(l:List[Elem]) =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski read?x -> Buf( cons(x,nil) )
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski [] if l=nil then STOP else write!last(l) -> Buf( rest(l) )
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHere, the construct \texttt{data List} refers to the \CASL specification
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{List}, which is implicitly embedded into \CspCASL.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe ending \texttt{.hs} is available for directly reading in
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHaskell programs, and hence supports the Haskell module system.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithe logic Haskell has to be chosen explicitly, and the \CASL structuring
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisyntax needs to be used:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilibrary Factorial
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispec Factorial =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifac :: Int -> Int
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifac n = foldl (*) 1 [1..n]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiNote that according to the Haskell syntax, Haskell function
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskideclarations and definitions need to start with the first column of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Development Graphs}\label{sec:DevGraph}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDevelopment graphs are a simple kernel formalism for (heterogeneous)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskistructured theorem proving and proof management. A development graph
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiconsists of a set of nodes (corresponding to whole structured
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecifications or parts thereof), and a set of arrows called
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidefinition links, indicating the dependency of each involved
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskistructured specification on its subparts. Arising proof obligations
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiare attached as so-called theorem links to this graph.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe following options let \Hets show the development graph of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskia specification library:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-G}, \texttt{--only-gui}] Shows the development graph in a GUI window,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiand suppresses the writing of an output file.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiLet us extend the above library \texttt{Order.casl}. One use of the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilibrary might be to express the fact that the natural numbers form a
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskistrict partial order as a view, as follows:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{EXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEDEFN{Natural\_Order\_2} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{Natural}} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\PRED \( \_\_<\_\_ : Nat \* Nat\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL x,y:Nat \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. 0 < suc(x) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. \neg x < 0 \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. suc(x) < suc(y) \IFF x < y
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{EXAMPLE}%[\SLIDESMALL]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{Natural\_Order\_2} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I{} \( Elem \MAPSTO Nat\)
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAgain, these specifications can be checked with \Hets. However, this
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskionly checks syntactic and static semantic well-formedness -- it is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiby a strict partial ordering relation. Checking this requires theorem
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproving, which will be discussed below.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHowever, before coming to theorem proving, let us first inspect the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof obligations arising from a specification. This can be done with:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{hets -g Order.casl}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(assuming that the above two specifications and the view
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskihave been added to the file
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets now displays a so-called development graph
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(which is just an overview graph showing the overall structure
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof the specifications in the library), see Fig.~\ref{fig:dg0}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{center}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\includegraphics[scale=0.7]{dg-order-0}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Sample development graph.\label{fig:dg0}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiNodes in a development graph correspond to \CASL specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiArrows show how specifications are related by the structuring
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe black arrow denotes an ordinary import of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecifications (generated by the extension), while the red arrow
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidenotes a proof obligation (corresponding to the view).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThis proof obligation needs to be discharged in order to
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskishow that the view is well-formed (then its color turns into green).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAs a more complex example, consider the following loose specification
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof a sorting function, taken from the \CASL User Manual
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
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithe \CASL User Manual \cite{CASL/UserManual}, Chap.~6:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{List\_Order}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\phantomsection
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\WITHIN]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\OP \( insert : Elem \* List \TOTAL List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL e,e':Elem; L:List \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. insert(e, empty) = cons(e, empty) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. insert(e, cons(e',L)) = \[ cons(e', insert(e,L)) \WHEN e' < e\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ELSE cons(e, cons(e',L)) \] \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\OP \( order : List \TOTAL List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL e:Elem; L:List \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. order(empty) = empty \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. order(cons(e,L)) = insert(e, order(L)) \]\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBoth specifications are related. To see this, we first inspect
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitheir signatures. This is possible with:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{hets -g Sorting.casl}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiassuming that \texttt{Sorting.casl} contains the above specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{center}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\includegraphics[scale=0.7]{dg-order-1}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Development graph for the two sorting specifications.\label{fig:dg1}}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn the above-mentioned development graph, we have two types of nodes.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe named ones correspond to named specifications, but there
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiare also unnamed nodes corresponding to anonymous basic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispecifications like the declaration of the $insert$ operation in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order} above. Basically, there is an
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiunnamed node for each structured specification that is not named.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAgain, the black arrows denote an ordinary import of specifications
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(corresponding to the extensions and unions in the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecifications), while the blue arrows denote hiding (corresponding to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe local specification).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBy clicking on the nodes, one can inspect their signatures.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn this way, we can see that both \NAMEREF{List\_Order\_Sorted} and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order} have the same signature. Hence, it
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis legal to add a view:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{EXAMPLE}%[\SLIDESMALL]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\VIEW \NAMEDEFN{v2}[\NAMEREF{Total\_Order}] ~:~ \NAMEREF{List\_Order\_Sorted}[\NAMEREF{Total\_Order}] \TO
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order}[\NAMEREF{Total\_Order}]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWe have already added this view to \texttt{Sorting.casl}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe corresponding
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof obligation between \NAMEREF{List\_Order\_Sorted} and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order} is displayed in Fig.~\ref{fig:dg1}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski as a red arrow.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHere is a summary of the types of nodes and links occurring in
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidevelopment graphs:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Named nodes] correspond to a named specification.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Unnamed nodes] correspond to an anonymous specification.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Elliptic nodes] correspond to a specification in the current library.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Rectangular nodes] are external nodes corresponding
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski to a specification downloaded from
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskianother library.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Black links] correspond to reference to other specifications
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(definition links in the sense of \cite[IV:4]{CASL/RefManual}).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Blue links] correspond to hiding (hiding definition links).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Red links] correspond to open proof obligations (theorem links).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Green links] correspond to proved proof obligations (theorem links).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Solid links] correspond to global (definition or theorem)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilinks in the sense of \cite[IV:4]{CASL/RefManual}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Dashed links] correspond to local (definition or theorem) links in the sense of \cite[IV:4]{CASL/RefManual}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiWe now explain the menus of the development graph window.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiMost of the pull-down menus of the window are daVinci-specific
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitheir function can be looked up in the daVinci documentation.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe exception is the Edit menu. Moreover, the nodes and links
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof the graph have attached pop-up menus, which appear when
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiclicking with the right mouse button.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Edit] This menu has two submenus:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Unnamed nodes] With the ``Hide'' submenu, it is possible
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskito reduce the complexity of the graph by hiding all unnamed nodes;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskionly nodes corresponding to named specifications remain displayed.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiPaths between named nodes going through unnamed nodes
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiare displayed as links. With the ``Show'' submenu, the unnamed
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskinodes re-appear.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Proofs] This menu allows to apply some of the deduction
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskirules for development graphs, see Sect. IV:4.4 of the \CASL
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiReference Manual \cite{CASL/RefManual}. However, it is still
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiexperimental and far from being completely implemented.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiMoreover, in the future \Hets will be interfaced with various
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski logic-specific theorem proving, rewriting and consistency checking
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Pop-up menu for nodes]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHere, the number of submenus depends on the type of the node:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show signature] Shows the signature of the node.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show sublogic] Shows the logic and, within that logic, the minimal sublogic
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifor the signature and the axioms of the node.
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\item[Show origin] Shows the kind of \CASL structuring construct that
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskiled to the node.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show just subtree] (Only for named nodes) Reduce the complexity
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof the graph by just showing the subtree below the current node.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Undo show just subtree] (Only for named nodes) Undo the reduction.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show referenced library] (Only for external nodes) Open a new window
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskishowing the development graph for the library the external node refers to.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Pop-up menu for links]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAgain, the number of submenus depends on the type of the node:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show morphism] Shows the signature morphism of the link. It consists
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof two components: a logic translation and a signature morphism in the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitarget logic of the logic translation.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiIn the (most frequent) case
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof an intra-logic signature morphism, the logic translation component is
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskijust the identity.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show origin] Shows the kind of \CASL structuring construct that
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiled to the link.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show proof status] (Only for theorem links) Show the proof status.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\section{Reading, Writing and Formatting}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Hets provides several options controlling the types of files
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithat are read and written.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-i ITYPE}, \texttt{--input-type=ITYPE}] Specify
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\texttt{ITYPE} as the type of the input file. The default is
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\texttt{het} (\HetCASL plain text). \texttt{ast} is for reading
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiin abstract syntax trees in ATerm format, while \texttt{ast.baf}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskireads in the compressed ATerm format.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-O DIR}, \texttt{--output-dir=DIR}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiSpecify \texttt{DIR} as destination directory for output files.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-o OTYPES}, \texttt{--output-types=OTYPES}]
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\texttt{OTYPES} is a comma separated list of output types:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{verbatim}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (ast|[fh]?dg(.nax)?).(het|trm|taf|html|xml)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |(pp.(het|tex|html))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |(graph.(dot|ps|davinci))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{verbatim}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe default is \texttt{dg.taf}, which means that the development
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskigraph of the library is stored in textual ATerm format (\texttt{taf}).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThis format can be read in when a library is downloaded from
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskianother library, avoiding the need to re-analyse the downloaded library.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe \texttt{pp} format is for pretty printing, either as plain text
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(\texttt{het}), \LaTeX input (\texttt{tex}) or HTML (\texttt{html}).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiA formatter with pretty-printed output currently is available only for
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithe \CASL logic. For example, it is possible to generate a pretty
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiprinted \LaTeX\ version of \texttt{Order.casl} by typing:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThis will generate a file \texttt{Order.pp.tex}. It can be included
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinto \LaTeX\ documents, provided that the style \texttt{hets.sty}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicoming with the \Hets distribution is used.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe option \texttt{-r RAW} or \texttt{--raw=RAW} allows one
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskito influence the formatting in more detail.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHere, \texttt{RAW} is \texttt{(ascii|text|(la)?tex)=STRING},
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskiand \texttt{STRING} is passed to the appropriate pretty-printer.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiThe deatils of these options are to be fixed in the future only.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe other output formats are for future usage.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Miscellaneous Options}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-v[Int]}, \texttt{--verbose[=Int]}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiSet the verbosity level according to \texttt{Int}. Default is 1.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-q}, \texttt{--quiet}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiBe quiet -- no diagnostic output at all. Overrides -v.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-V}, \texttt{--version}] Print version number and exit.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-h}, \texttt{--help}, \texttt{--usage}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiPrint usage information and exit.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{+RTS IntM -RTS}] Increase the stack size to
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \texttt{Int} megabytes (needed in case of a stack overflow).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThis must be the first option.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\section{Limits of \Hets}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\Hets is still intensively under development. In particular, the
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskifollowing points are still missing:
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\begin{itemize}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\item There is no static analysis for architectural specifications.
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\item Distributed libraries are always downloaded from the local disk,
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskinot from the Internet.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\item Version numbers of libraries are not considered properly.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\item The proof engine for development graphs has not been completed.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets has been built based on experiences with its
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \index{Cats@\Cats}%
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \index{Maya@\MAYA}%
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe \CASL Tool Set (\Cats)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\cite{Mossakowski:2000:CST,Mossakowski:1998:SSA}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicomes with similar analysis tools as \Hets (only for \CASL).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Cats should be used if a static analysis of architectural
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecifications is needed, because this is not available
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%but neither supports extensions nor does it identify
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%sublanguages of \CASL (and the tools to be used with
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%sublanguages only).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe management of development graphs is not integrated
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskibut is provided with a stand-alone version of the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskitool \MAYA \cite{Autexier:2002:IHD,AutexierEtal02}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%(which only supports part of \CASL's
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%structuring constructs; in particular, hiding is not supported).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Cats and \MAYA
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%are mainly important in the current transition phase,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%since \Hets does not support full \CASL (e.g. architectural
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%specifications) yet.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski can be obtained from the \CoFI tools home page \cite{CoFITools}.
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
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski(hets@tzi.de). We will take account your feedback when deciding which
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogics and proof tools to integrate next into \Hets. Help with
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiintegration of more logics and proof tools into \Hets is also welcome.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets is mainly maintained by
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiChristian Maeder (maeder@tzi.de) and Till Mossakowski
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(till@tzi.de). The mailing list is hets@tzi.de.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\paragraph{Acknowledgement}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets has been programmed by the following people:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiKatja Abu-Dib,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiCarsten Fischer,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiJorina Freya Gerken,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiSonja Gr\"{o}ning,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiWiebke Herding,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMartin K\"{u}hl,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiKlaus L\"{u}ttich,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiChristian Maeder,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMaciek Makowski,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiTill Mossakowski,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiDaniel Pratsch,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiFelix Reckers,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMarkus Roggenbach,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiPascal Schmidt.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\Hets also benefited much from contributions by Serge Autexier, Dieter
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiHutter and Bartek Klin (through work on its precursors \Cats and
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\bibliographystyle{plain}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\bibliography{cofibib,cofi-ann,UM,hets}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{document}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% Local Variables:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% mode: latex
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% TeX-master: "UserGuide"