UserGuide.tex revision 38a46398edcd7ad7d1777ae646d4cc484cce49bf
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
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\CASL (\HetCASL) combines the specification langauage \CASL with \CASL extensions
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand sublanguages, as well as comletely different logics and even
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiprogramming languages such as Haskell. \HetCASL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiextends the strucruting 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}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiprecsribe 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} \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\CASL \ar[u] \ar[ur]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Graph of logics currently supported by \Hets.\label{fig:LogicGraph}}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{figure}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{tabular}{|l|l|l|}\\\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
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\CspCASL & x & - & - \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiStructured specifications & x & x & - \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiArchitectural specifications & x & - & 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}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe definitive reference for Haskell is \cite{Haskell98},
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
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
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMac OS-X. After downloading your platform specific distribution,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiyou have to unpack it as follows (note that the filenames will
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskibe slightly different, depending on your platform):
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\QUERY{Install script needed?!?}
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.
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.
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.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\QUERY{This should be done by the install script!}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiexport DAVINCIHOME=<path>/daVinci_V2.1
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiexport UNIDAVINCI=<path>/daVinci_V2.1/daVinci
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe environment variable \texttt{HETS_LIB} should be set to
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskia location where specification libraries are stored.
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
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski(equivalently, you can set the variable \texttt{HETS_LIB} before
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskicalling \Hets).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Heterogeneous Specification} \label{sec:HetSpec}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets accepts plain text input files with the following endings:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{tabular}{lll}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiEnding & default logic & structuring language\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.casl} & \CASL & \CASL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.het} & \CASL & \CASL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill 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
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiembedding of \CASL into \HasCASL. (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{Formatting}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiA formatter with pretty-printed output currently is available only for
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithe \CASL logic. For example, it is possible to generate a pretty
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiprinted \LaTeX\ version of \texttt{Order.casl} by typing:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe option \texttt{-r RAW} or \texttt{--raw=RAW},
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiwhere \texttt{RAW} is \texttt{(ascii|text|(la)?tex)=STRING},
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiand \texttt{STRING} is passed to the appropiate pretty-printer.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Development Graphs}\label{sec:DevGraph}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe following options let \Hets show the development graph of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskia specification library:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-g}, \texttt{--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
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Precursors of \Hets}
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}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskicomes with roughly the same analysis tools as \Hets.
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
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.
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.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{document}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% Local Variables:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% mode: latex
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% TeX-master: "UserGuide"