\documentclass{article}

\usepackage{alltt}

\usepackage{casl}

\usepackage{xspace}

\usepackage{color}

\input{xy}

\xyoption{v2}

\newcommand{\QUERY}[1]%{}

{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}

\newcommand{\eat}[1]{}

\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}

{\end{ITEMS}\end{EXAMPLEFORMAT}\par}

\newcommand{\IEXT}[1] {\\#1\I}

\newcommand{\IEND} {\I\END}

\newenvironment{EXAMPLEFORMAT} {}{}

%% Added by MB to have some extra vertical space after the ``main'' examples

%% following the points (and some others in the text):

\newenvironment{BIGEXAMPLE} {\begin{EXAMPLE}} {\end{EXAMPLE}\medskip}

\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}

\newenvironment{DETAILSFORMAT} {}{}

\newenvironment{META}[1][] {#1\begin{METAFORMAT}}{\end{METAFORMAT}}

\newenvironment{METAFORMAT} {\medskip\vrule\hspace{1ex}\vrule\hspace{1ex}%

\begin{minipage}{0.9\textwidth}\it}

{\end{minipage}\par\medskip}

\newcommand{\SLIDESMALL} {}

\newcommand{\SLIDESONLY}[1] {}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% SIMULATING SMALL-CAPS FOR BOLD, EMPH

\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}

%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}

\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}

\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}

\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}

\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}

\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}

%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}

\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}

\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}

\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}

\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}

\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}

%\newcommand {\CoFI}{CoFI\xspace}

\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}

\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}

\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}

\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}

\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}

\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}

\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}

\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}

\newcommand{\largeELAN} {\largeTEXTSC{E}{LAN}\xspace}

\newcommand {\HOL}{\normalTEXTSC{H}{OL}\xspace}

\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}

\newcommand {\Isabelle}{\normalTEXTSC{I}{SABELLE}\xspace}

\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}

\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}

%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL

\newcommand{\LCF}{LCF\xspace}

\newcommand{\ASF}{ASF\xspace}

%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}

%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}

\newcommand{\SDF}{SDF\xspace}

%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}

%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}

\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}

\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}

\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}

\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}

%% Do NOT use \ASF+\SDF (it gives a superflous space in the middle)

\newcommand{\CCC}{CCC\xspace}

\newcommand{\CoCASL}{\normalTEXTSC{C}{O}\normalTEXTSC{C}{ASL}\xspace}

\newcommand{\CspCASL}{\normalTEXTSC{C}{SP}-\normalTEXTSC{C}{ASL}\xspace}

\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}

\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}

\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}

\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}

\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}

\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}

\begin{document}

\title{{\bf \protect{\LARGEHets} User Guide}\\

-- Version 0.3 --}

\author{Till Mossakowski\\[1em]

Department of Computer Science\\ and Bremen

Institute for Safe Systems,\\ University of Bremen, Germany.\\[1em]

Comments to: hets@tzi.de

}

\maketitle

\section{Introduction}

The Heterogeneous Tool Set (\protect\Hets) is the main analysis tool

for the specification language heterogeneous \CASL. Heterogeneous

\CASL (\HetCASL) combines the specification langauage \CASL with \CASL extensions

and sublanguages, as well as completely different logics and even

programming languages such as Haskell. \HetCASL

extends the structuring mechanisms of \CASL:

\emph{Basic specifications} are

unstructured specifications or modules written in a specific logic.

The graph of currently supported logics is shown in Fig.~\ref{fig:LogicGraph},

and the degree of support by \Hets in Fig.~\ref{fig:Languages}.

With \emph{heterogeneous structured specifications}, it is possible to

combine and rename specifications, hide parts thereof, and also

translate them to other logics. \emph{Architectural specifications}

prescribe the structure of implementations. \emph{Specification

libraries} are collections of named structured and architectural

specifications.

\Hets consists of logic-specific tools for the parsing and static

analysis of the different involved logics, as well as a

logic-independent parsing and static analysis tool for structured and

architectural specifications and libraries. The latter of course needs

to call the logic-specific tools whenever a basic specification is

encountered.

\begin{figure}

$$\xymatrix{

\Text{Haskell}

&

\Text{\HasCASL}

&

\Text{\CspCASL} \\

&

\Text{\CASL} \ar[u] \ar[ur]

&

}$$

\caption{Graph of logics currently supported by \Hets.\label{fig:LogicGraph}}

\end{figure}

\begin{figure}

\begin{tabular}{|l|c|c|c|}\hline

Language & Parser & Static Analysis & Prover \\\hline

\CASL & x & x & - \\\hline

\HasCASL & x & (x) & - \\\hline

Haskell & x & x & -\\\hline

\CspCASL & x & - & - \\\hline

Structured specifications & x & x & (x) \\\hline

Architectural specifications & x & - & -\\\hline

\end{tabular}

\caption{Current degree of \Hets support for the different languages.\label{fig:Languages}}

\end{figure}

An introduction to \CASL can be found in the \CASL User Manual

\cite{CASL/UserManual}; the detailed language reference is given in

the \CASL Reference Manual \cite{CASL/RefManual}. These documents

explain both the \CASL logic and language of basic specifications as

well as the logic-independent constructs for structured and

architectural specifications. Corresponding documents explaining the

\HetCASL language constructs for \emph{heterogeneous} structured specifications

are forthcoming, until then, \cite{Mossakowski:2003:FHS} may serve as a short

introduction. Moreover, the main heterogeneous constructs will be illustrated

in Sect.~\ref{sec:HetSpec} below.

An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};

the language is summarized in \cite{HasCASL/Summary}.

The definitive reference for Haskell is \cite{PeytonJones03},

see also \url{www.haskell.org}. An introduction to \CspCASL

is given in \cite{Roggenbach:2003:CCN}.

\section{Getting started}

The latest \Hets version can be obtained from the

\CoFI tools home page \cite{CoFITools}. Since \Hets is being

improved constantly, it is recommended always to use the latest version.

\Hets currently is available for Linux, Solaris and

Mac OS-X. After downloading your platform specific distribution,

you have to unpack it as follows (note that the filenames will

be slightly different, depending on your platform):

\begin{verbatim}

tar zxf hets.tgz # gtar under Solaris

\end{verbatim}

If you have a source distribution then please follow the instructions of the

\texttt{INSTALL} file.

For the display of development graphs, \Hets uses daVinci.

daVinci is maintained by b-novative and b-novative holds all rights.

This release may be accompanied with free binary releases of daVinci

Version 2.1, but daVinci 2.1 is no longer supported or maintained.

However, you are encouraged to obtain the latest version of daVinci

Presenter (currently 3.0.5) from \url{http://www.b-novative.com}.

It needs a license key, but is free for academic purposes.

Linux: the linux binary release of daVinci 2.1 relies on the old

shlibs5 that must be installed on your system (if ./daVinci cannot be

found/executed, then shlibs5 are missing)

Solaris: the solaris binary release of daVinci 2.1 should work without

problems

Macintosh (Darwin): there is no release of daVinci for Macintosh, but

b-novative may have one in the mean time

For best quality, get the latest version of daVinci from b-novative.

For \Hets to find daVinci, the environment variables \texttt{DAVINCIHOME} and

\texttt{UNIDAVINCI} must be set to the installation directory of daVinci and to

the actual executable, respectively.

\QUERY{This should be done by the install script!}

\begin{verbatim}

export DAVINCIHOME=<path>/daVinci_V2.1

export UNIDAVINCI=<path>/daVinci_V2.1/daVinci

\end{verbatim}

The environment variable \texttt{HETS\_LIB} should be set to

a location where specification libraries are stored.

\section{Analysis of Specifications}

Consider the following \CASL

specification:

\medskip

\begin{BIGEXAMPLE}

\I\SPEC \NAMEREF{Strict\_Partial\_Order} =

%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}

\begin{ITEMS}[\PRED]

\I\SORT \( Elem \)

\I\PRED \( \_\_<\_\_ : Elem \* Elem \)

% \COMMENTENDLINE{\PRED abbreviates predicate}

\end{ITEMS}

\(\[ \FORALL x,y,z : Elem \\

\. \NOT(x < x) \RIGHT{\LABEL{strict}} \\

\. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\

\. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\

\]\)

\begin{COMMENT}

Note that there may exist \(x, y\) such that\\

neither \(x < y\) nor \(y < x\).

\end{COMMENT}

\I\END

\end{BIGEXAMPLE}

\Hets can be used for parsing and

checking static well-formedness of specifications.

\index{parsing}%

\index{static!analysis}%

\index{analysis, static}%

Let us assume that the example is in a file named

\texttt{Order.casl} (actually, this file is provided

with the \Hets distribution).

Then you can check the well-formedness of the

specification by typing (into some shell):

\begin{quote}

\texttt{hets Order.casl}

\end{quote}

\Hets checks both the correctness of this specification

with respect to the \CASL syntax, as

well as its correctness with respect to the static semantics (e.g.\

whether all identifiers have been declared before they are used,

whether operators are applied to arguments of the correct sorts,

whether the use of overloaded symbols is unambiguous, and so on).

The following flags are available in this context:

\begin{description}

\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing -- the static analysis

is skipped.

\item[\texttt{-s}, \texttt{--just-structured}]

Do the parsing and the static analysis of (heterogeneous) structured

specifications, but leave out the analysis of basic specifications.

This can be used to quickly produce a development graph

showing the dependencies among the specifications (cf. Sect.~\ref{sec:DevGraph}).

\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]

Use \texttt{DIR} as the directory for specification libraries

(equivalently, you can set the variable \texttt{HETS\_LIB} before

calling \Hets).

\end{description}

\section{Heterogeneous Specification} \label{sec:HetSpec}

\Hets accepts plain text input files with the following endings:\\

\begin{tabular}{|l|c|c|}\hline

Ending & default logic & structuring language\\\hline

\texttt{.casl} & \CASL & \CASL \\\hline

\texttt{.het} & \CASL & \CASL \\\hline

\texttt{.hs} & Haskell & Haskell\\\hline

\end{tabular}

\medskip

Although the endings \texttt{.casl} and \texttt{.het} are

interchangeable, the former should be used for libraries of

homogeneous \CASL specifications and the latter for \HetCASL libraries

of heterogeneous specifications (that use the \CASL structuring

constructs). Within a \HetCASL library, the current logic can be changed e.g.\

to \HasCASL in the following way:

\begin{verbatim}

logic HasCASL

\end{verbatim}

The subsequent specifications are then parsed and analysed as

\HasCASL specifications. Within such specifications,

it is possible to use references to named \CASL specifications;

these are then automatically translated along the default

embedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).

(Heterogeneous constructs

for explicit translations between logics will be made available

in the future.)

A \CspCASL specification consists of a \CASL specification

for the data part and a \Csp process built over this data part.

Therefore, \HetCASL provides a heterogeneous language construct

\texttt{data} as follows:

\begin{verbatim}

library Buffer

logic CASL

spec List =

free type List[Elem] ::= nil | cons(Elem; List[Elem])

end

logic CspCASL

spec Buffer =

data List

channel read, write : Elem

process read

let Buf(l:List[Elem]) =

read?x -> Buf( cons(x,nil) )

[] if l=nil then STOP else write!last(l) -> Buf( rest(l) )

in Buf(nil)

end

\end{verbatim}

Here, the construct \texttt{data List} refers to the \CASL specification

\texttt{List}, which is implicitly embedded into \CspCASL.

The ending \texttt{.hs} is available for directly reading in

Haskell programs, and hence supports the Haskell module system.

By contrast, in \HetCASL libraries (ending with \texttt{.het}),

the logic Haskell has to be chosen explicitly, and the \CASL structuring

syntax needs to be used:

\begin{verbatim}

library Factorial

logic Haskell

spec Factorial =

fac :: Int -> Int

fac n = foldl (*) 1 [1..n]

end

\end{verbatim}

Note that according to the Haskell syntax, Haskell function

declarations and definitions need to start with the first column of

the text.

\section{Development Graphs}\label{sec:DevGraph}

Development graphs are a simple kernel formalism for (heterogeneous)

structured theorem proving and proof management. A development graph

consists of a set of nodes (corresponding to whole structured

specifications or parts thereof), and a set of arrows called

definition links, indicating the dependency of each involved

structured specification on its subparts. Arising proof obligations

are attached as so-called theorem links to this graph.

Details can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}.

The following options let \Hets show the development graph of

a specification library:

\begin{description}

\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window.

\item[\texttt{-G}, \texttt{--only-gui}] Shows the development graph in a GUI window,

and suppresses the writing of an output file.

\end{description}

\eat{

Let us extend the above library \texttt{Order.casl}. One use of the

library might be to express the fact that the natural numbers form a

strict partial order as a view, as follows:

\medskip

\begin{BIGEXAMPLE}

\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END

\end{BIGEXAMPLE}

\begin{EXAMPLE}

\I\SPEC \NAMEDEFN{Natural\_Order\_2} =

\IEXT{\NAMEREF{Natural}} \THEN

\begin{ITEMS}

\I\PRED \( \_\_<\_\_ : Nat \* Nat\)

\end{ITEMS}

\(\[ \FORALL x,y:Nat \\

\. 0 < suc(x) \\

\. \neg x < 0 \\

\. suc(x) < suc(y) \IFF x < y

\]\)

\I\END

\end{EXAMPLE}

\begin{EXAMPLE}%[\SLIDESMALL]

\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO

\NAMEREF{Natural\_Order\_2} =

\I{} \( Elem \MAPSTO Nat\)

\I\END

\end{EXAMPLE}

Again, these specifications can be checked with \Hets. However, this

only checks syntactic and static semantic well-formedness -- it is

\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in

\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted

by a strict partial ordering relation. Checking this requires theorem

proving, which will be discussed below.

However, before coming to theorem proving, let us first inspect the

proof obligations arising from a specification. This can be done with:

\begin{quote}

\texttt{hets -g Order.casl}

\end{quote}

(assuming that the above two specifications and the view

have been added to the file

\texttt{Order.casl}).

\Hets now displays a so-called development graph

(which is just an overview graph showing the overall structure

of the specifications in the library), see Fig.~\ref{fig:dg0}.

\begin{figure}

\begin{center}

\includegraphics[scale=0.7]{dg-order-0}

\end{center}

\caption{Sample development graph.\label{fig:dg0}}

\end{figure}

Nodes in a development graph correspond to \CASL specifications.

Arrows show how specifications are related by the structuring

constructs.

The black arrow denotes an ordinary import of

specifications (generated by the extension), while the red arrow

denotes a proof obligation (corresponding to the view).

This proof obligation needs to be discharged in order to

show that the view is well-formed (then its color turns into green).

As a more complex example, consider the following loose specification

of a sorting function, taken from the \CASL User Manual

\cite{CASL/UserManual}, Chap.~6:

\begin{BIGEXAMPLE}

\I\SPEC \NAMEREF{List\_Order\_Sorted}

\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =

\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN

\begin{ITEMS}[\WITHIN]

\I\LOCAL

\begin{ITEMS}[\PRED]

\I\PRED \( \_\_is\_sorted : List \)

\end{ITEMS}

\(\[ \FORALL e,e': Elem; L : List \\

\. empty~is\_sorted \\

\. cons(e,empty)~is\_sorted \\

\. cons(e,cons(e',L))~is\_sorted \IFF

\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)

\I\WITHIN

\begin{ITEMS}[\OP]

\I\OP \( order : List \TOTAL List \)

\end{ITEMS}

\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)

\end{ITEMS}

\I\END

\end{BIGEXAMPLE}

The following specification of sorting by insertion also is taken from

the \CASL User Manual \cite{CASL/UserManual}, Chap.~6:

\begin{BIGEXAMPLE}

\I\SPEC \NAMEREF{List\_Order}

[\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =

\phantomsection

\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN

\begin{ITEMS}[\WITHIN]

\I\LOCAL

\begin{ITEMS}[\OP]

\I\OP \( insert : Elem \* List \TOTAL List \)

\end{ITEMS}

\(\[ \FORALL e,e':Elem; L:List \\

\. insert(e, empty) = cons(e, empty) \\

\. insert(e, cons(e',L)) = \[ cons(e', insert(e,L)) \WHEN e' < e\\

\ELSE cons(e, cons(e',L)) \] \\

\]\)

\I\WITHIN

\begin{ITEMS}[\OP]

\I\OP \( order : List \TOTAL List \)

\end{ITEMS}

\(\[ \FORALL e:Elem; L:List \\

\. order(empty) = empty \\

\. order(cons(e,L)) = insert(e, order(L)) \]\)

\end{ITEMS}

\I\END

\end{BIGEXAMPLE}

Both specifications are related. To see this, we first inspect

their signatures. This is possible with:

\begin{quote}

\texttt{hets -g Sorting.casl}

\end{quote}

assuming that \texttt{Sorting.casl} contains the above specifications.

\Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.

\begin{figure}

\begin{center}

\includegraphics[scale=0.7]{dg-order-1}

\end{center}

\caption{Development graph for the two sorting specifications.\label{fig:dg1}}

\end{figure}

In the above-mentioned development graph, we have two types of nodes.

The named ones correspond to named specifications, but there

are also unnamed nodes corresponding to anonymous basic

specifications like the declaration of the $insert$ operation in

\NAMEREF{List\_Order} above. Basically, there is an

unnamed node for each structured specification that is not named.

Again, the black arrows denote an ordinary import of specifications

(corresponding to the extensions and unions in the

specifications), while the blue arrows denote hiding (corresponding to

the local specification).

By clicking on the nodes, one can inspect their signatures.

In this way, we can see that both \NAMEREF{List\_Order\_Sorted} and

\NAMEREF{List\_Order} have the same signature. Hence, it

is legal to add a view:

\begin{EXAMPLE}%[\SLIDESMALL]

\I\VIEW \NAMEDEFN{v2}[\NAMEREF{Total\_Order}] ~:~ \NAMEREF{List\_Order\_Sorted}[\NAMEREF{Total\_Order}] \TO

\NAMEREF{List\_Order}[\NAMEREF{Total\_Order}]

\I\END

\end{EXAMPLE}

We have already added this view to \texttt{Sorting.casl}.

The corresponding

proof obligation between \NAMEREF{List\_Order\_Sorted} and

\NAMEREF{List\_Order} is displayed in Fig.~\ref{fig:dg1}

as a red arrow.

}

Here is a summary of the types of nodes and links occurring in

development graphs:

\begin{description}

\item[Named nodes] correspond to a named specification.

\item[Unnamed nodes] correspond to an anonymous specification.

\item[Elliptic nodes] correspond to a specification in the current library.

\item[Rectangular nodes] are external nodes corresponding

to a specification downloaded from

another library.

\item[Black links] correspond to reference to other specifications

(definition links in the sense of \cite[IV:4]{CASL/RefManual}).

\item[Blue links] correspond to hiding (hiding definition links).

\item[Red links] correspond to open proof obligations (theorem links).

\item[Green links] correspond to proved proof obligations (theorem links).

\item[Solid links] correspond to global (definition or theorem)

links in the sense of \cite[IV:4]{CASL/RefManual}.

\item[Dashed links] correspond to local (definition or theorem) links in the sense of \cite[IV:4]{CASL/RefManual}.

\end{description}

We now explain the menus of the development graph window.

Most of the pull-down menus of the window are daVinci-specific

layout menus;

their function can be looked up in the daVinci documentation.

The exception is the Edit menu. Moreover, the nodes and links

of the graph have attached pop-up menus, which appear when

clicking with the right mouse button.

\begin{description}

\item[Edit] This menu has two submenus:

\begin{description}

\item[Unnamed nodes] With the ``Hide'' submenu, it is possible

to reduce the complexity of the graph by hiding all unnamed nodes;

only nodes corresponding to named specifications remain displayed.

Paths between named nodes going through unnamed nodes

are displayed as links. With the ``Show'' submenu, the unnamed

nodes re-appear.

\item[Proofs] This menu allows to apply some of the deduction

rules for development graphs, see Sect. IV:4.4 of the \CASL

Reference Manual \cite{CASL/RefManual}. However, it is still

experimental and far from being completely implemented.

Moreover, in the future \Hets will be interfaced with various

logic-specific theorem proving, rewriting and consistency checking

tools.

\end{description}

\item[Pop-up menu for nodes]

Here, the number of submenus depends on the type of the node:

\begin{description}

\item[Show signature] Shows the signature of the node.

\item[Show sublogic] Shows the logic and, within that logic, the minimal sublogic

for the signature and the axioms of the node.

\item[Show origin] Shows the kind of \CASL structuring construct that

led to the node.

\item[Show just subtree] (Only for named nodes) Reduce the complexity

of the graph by just showing the subtree below the current node.

\item[Undo show just subtree] (Only for named nodes) Undo the reduction.

\item[Show referenced library] (Only for external nodes) Open a new window

showing the development graph for the library the external node refers to.

\end{description}

\item[Pop-up menu for links]

Again, the number of submenus depends on the type of the node:

\begin{description}

\item[Show morphism] Shows the signature morphism of the link. It consists

of two components: a logic translation and a signature morphism in the

target logic of the logic translation.

In the (most frequent) case

of an intra-logic signature morphism, the logic translation component is

just the identity.

\item[Show origin] Shows the kind of \CASL structuring construct that

led to the link.

\item[Show proof status] (Only for theorem links) Show the proof status.

\end{description}

\end{description}

\section{Reading, Writing and Formatting}

\Hets provides several options controlling the types of files

that are read and written.

\begin{description}

\item[\texttt{-i ITYPE}, \texttt{--input-type=ITYPE}] Specify

\texttt{ITYPE} as the type of the input file. The default is

\texttt{het} (\HetCASL plain text). \texttt{ast} is for reading

in abstract syntax trees in ATerm format, while \texttt{ast.baf}

reads in the compressed ATerm format.

\item[\texttt{-O DIR}, \texttt{--output-dir=DIR}]

Specify \texttt{DIR} as destination directory for output files.

\item[\texttt{-o OTYPES}, \texttt{--output-types=OTYPES}]

\texttt{OTYPES} is a comma seperated list of output types:

\begin{verbatim}

(ast|[fh]?dg(.nax)?).(het|trm|taf|html|xml)

|(pp.(het|tex|html))

|(graph.(dot|ps|davinci))

\end{verbatim}

The default is \texttt{dg.taf}, which means that the development

graph of the library is stored in textual ATerm format (\texttt{taf}).

This format can be read in when a library is downloaded from

another library, avoiding the need to re-analyse the downloaded library.

The \texttt{pp} format is for pretty printing, either as plain text

(\texttt{het}), \LaTeX input (\texttt{tex}) or HTML (\texttt{html}).

A formatter with pretty-printed output currently is available only for

the \CASL logic. For example, it is possible to generate a pretty

printed \LaTeX\ version of \texttt{Order.casl} by typing:

\begin{quote}

\texttt{hets -o pp.tex Order.casl}

\end{quote}

This will generate a file \texttt{Order.pp.tex}. It can be included

into \LaTeX\ documents, provided that the style \texttt{hets.sty}

coming with the \Hets distribution is used.

The option \texttt{-r RAW} or \texttt{--raw=RAW} allows one

to influence the formatting in more detail.

\QUERY{Is the pretty printer documentation OK, Klaus?}

Here, \texttt{RAW} is \texttt{(ascii|text|(la)?tex)=STRING},

and \texttt{STRING} is passed to the appropiate pretty-printer.

The other output formats are for future usage.

\end{description}

\section{Miscellaneous Options}

\begin{description}

\item[\texttt{-v[Int]}, \texttt{--verbose[=Int]}]

Set the verbosity level according to \texttt{Int}. Default is 1.

\item[\texttt{-q}, \texttt{--quiet}]

Be quiet -- no diagnostic output at all. Overrides -v.

\item[\texttt{-V}, \texttt{--version}] Print version number and exit.

\item[\texttt{-h}, \texttt{--help}, \texttt{--usage}]

Print usage information and exit.

\item[\texttt{+RTS IntM -RTS}] Increase the stack size to

\texttt{Int} megabytes (needed in case of a stack overflow).

This must be the first option.

\end{description}

\section{Limits of \Hets}

\Hets is still intensively under development. In particular, the

following points are still missing:

\begin{itemize}

\item Distributed libraries are always downloaded from the local disk,

not from the Internet.

\item Version numbers of libraries are not considered.

\end{itemize}

\Hets has been built based on experiences with its

precursors,

\index{Cats@\Cats}%

\Cats and

\index{Maya@\MAYA}%

\MAYA.

The \CASL Tool Set (\Cats)

\cite{Mossakowski:2000:CST,Mossakowski:1998:SSA}

comes with similar analysis tools as \Hets (only for \CASL).

\Cats should be used if a static analysis of architectural

specifications is needed, because this is not available

in \Hets yet.

%,

%but neither supports extensions nor does it identify

%sublanguages of \CASL (and the tools to be used with

%sublanguages only).

The management of development graphs is not integrated

in \Cats,

but is provided with a stand-alone version of the

tool \MAYA \cite{Autexier:2002:IHD,AutexierEtal02}.

%(which only supports part of \CASL's

%structuring constructs; in particular, hiding is not supported).

%

\Cats and \MAYA

%are mainly important in the current transition phase,

%since \Hets does not support full \CASL (e.g. architectural

%specifications) yet.

%They

can be obtained from the \CoFI tools home page \cite{CoFITools}.

\section{Architecture of \Hets}

\Hets is written in Haskell. Its parser uses combinator

\index{parsing}%

parsing.

The user-defined (also known as ``mixfix'') syntax of \CASL

calls for a two-pass approach. In the first pass, the skeleton of a

\CASL abstract syntax tree is derived, in order to extract user-defined

syntax rules. In a second pass, which is performed during

static

analysis, these syntax rules are used to parse

any expressions that

use mixfix notation. The output is stored in the so-called

\index{ATerms}%

ATerm format \cite{BJKO00}, which is used as interchange format

for interfacing with other tools.

\Hets provides an abstract interface for

\index{institution!independence}%

\index{independence, institution}%

institutions, so

that new logics can be integrated smoothly.

In order to do so, a parser,

a static checker and a prover for basic specifications in the logic have

to be provided.

\begin{figure}

%\includegraphics[scale=0.44]{hets}

\vspace{1em}

\input{hets.tex}

\caption{Architecture of the heterogeneous tool set.

\label{fig:hets}}

\end{figure}

The architecture of \Hets is shown in Fig.~\ref{fig:hets}.

If your favourite logic is missing in \Hets, please tell us

(hets@tzi.de). We will take account your feedback when deciding which

logics and proof tools to integrate next into \Hets. Help with

integration of more logics and proof tools into \Hets is also welcome.

\Hets is mainly maintained by

Christian Maeder (maeder@tzi.de) and Till Mossakowski

(till@tzi.de). The mailing list is hets@tzi.de.

\paragraph{Acknowledgement}

\Hets has been programmed by the following people:

Katja Abu-Dib,

Carsten Fischer,

Jorina Freya Gerken,

Sonja Gr\"{o}ning,

Wiebke Herding,

Martin K\"{u}hl,

Klaus L\"{u}ttich,

Christian Maeder,

Maciek Makowski,

Till Mossakowski,

Daniel Pratsch,

Felix Reckers,

Markus Roggenbach,

and

Pascal Schmidt.

\bibliographystyle{plain}

\bibliography{cofibib,cofi-ann,UM,hets}

\end{document}

%%% Local Variables:

%%% mode: latex

%%% TeX-master: "UserGuide"

%%% End: