UserGuide.tex revision 89118fd658073a87eddf4ead4bb63c6adb30550d
\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}}
%%%%% Klaus macros
\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
%%%%% end of Klaus macros
%% 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 superfluous 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}
\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
\begin{document}
\title{{\bf \protect{\LARGEHets} User Guide}\\
-- Version 0.7 --}
\author{Till Mossakowski\\[1em]
DFKI Lab Bremen, Bremen, Germany.\\[1em]
Comments to: hets-devel@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 language \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 and logic translations (the
latter are also called comorphisms) 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.
\section{Logics supported by \Hets}
\begin{figure}
\begin{center}
\includegraphics[scale=0.4]{LogicGraph}
\end{center}
\caption{Graph of logics currently supported by \Hets. The more an
ellipse is filled, the more stable is the implementation of the logic.}
\label{fig:LogicGraph}
\end{figure}
\begin{figure}
\begin{center}
\begin{tabular}{|l|c|c|c|}\hline
Language & Parser & Static Analysis & Prover \\\hline
\CASL & x & x & - \\\hline
\CoCASL & x & x & - \\\hline
\ModalCASL & x & x & - \\\hline
\HasCASL & x & x & - \\\hline
Haskell & x & x & -\\\hline
\CspCASL & (x) & - & - \\\hline
%Structured specifications & x & x & (x) \\\hline
%Architectural specifications & x & x & -\\\hline
\CASLDL & x & - & - \\\hline
OWL DL basic & x & (x) & - \\\hline
OWL DL structure & x & (x) & - \\\hline
SoftFOL & - & - & x \\\hline
\Isabelle & - & - & x \\\hline
\end{tabular}
\end{center}
\caption{Current degree of \Hets support for the different languages.\label{fig:Languages}}
\end{figure}
\begin{description}
\item[CASL] extends many sorted first-order logic with partial
functions and subsorting. It also provides induction sentences,
expressing the (free) generation of datatypes.
%It is mainly designed and used for the
%specification of requirements for software systems. But it is also
%used for the specification of \Dolce (Descriptive Ontology for
%Linguistic and Cognitive Engineering), an Upper Ontology for knowledge
%representation. \cite{Gangemi:2002:SOD} Further it is now used to
%specify calculi for time and space.
For more details on \CASL see \cite{CASL-RM,CASL-UM}.
%
We have implemented the \CASL logic in such a way that much of the
implementation can be re-used for \CASL extensions as well; this
is achieved via ``holes'' (realized via polymorphic variables) in the
types for signatures, morphisms, abstract syntax etc. This eases
integration of \CASL extensions and keeps the effort of integrating
\CASL extensions quite moderate.
\item[CoCASL] \cite{MossakowskiEA04} is a coalgebraic extension of \CASL,
suited for the specification of process types and reactive system.
The central proof method is coinduction.
\item[ModalCASL] \cite{ModalCASL}
is an extension of \CASL with multi-modalities and
term modalities. It allows the specification of modal systems with
Kripke's possible worlds semantics. It is also possible to express
certain forms of dynamic logic.
\item[HasCASL] is a higher order extension of \CASL allowing
polymorphic datatypes and functions. It is closely related to the
programming language Haskell and allows program constructs being
embedded in the specification.
An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
the language is summarized in \cite{HasCASL/Summary}, the semantics
in \cite{Schroder05b,Schroder-habil}.
\item[Haskell] is a modern, pure and strongly typed functional
programming language. It simultaneously is the implementation
language of \Hets, such that in the future, \Hets might be applied
to itself.
The definitive reference for Haskell is \cite{PeytonJones03},
see also \url{www.haskell.org}.
\item[CspCASL] \cite{Roggenbach:2003:C-CN} is a combination of \CASL
with the process algebra CSP.
\item[OWL DL] is the Web Ontology Language (OWL) recommended by the
World Wide Web Consortium (W3C, \texttt{http://www.w3c.org}). It is
used for knowledge representation and the Semantic Web
\cite{berners:2001:SWeb}.
Hets calls an external OWL DL parser
written in JAVA to obtain the abstract syntax for an OWL file and its
imports. The JAVA parser is also doing a first analysis classifying
the OWL ontology into the sublanguages OWL Full, OWL DL and OWL
Lite.
Hets only supports the last two, more restricted variants.
The
structuring of the OWL imports is displayed as Development Graph.
\item[CASL-DL] \cite{OWL-CASL-WADT2004}
is an extension of a restriction of \CASL, realizing
a strongly typed variant of OWL DL in \CASL syntax.
It extends
\CASL with cardinality restrictions for the description of sorts and
unary predicates. The restrictions are based on the equivalence
between \CASLDL, OWL~DL and \SHOIN. Compared to \CASL only unary
and binary predicates, predefined datatypes and concepts (subsorts
of the topsort Thing) are allowed. It is used to bring OWL DL and
\CASL closer together.
\item[SoftFOL] \cite{LuettichEA06a} offers three automated theorem
proving systems (ATP) for first-order logic with equality: (1) SPASS
\cite{WeidenbachEtAl02}; (2) Vampire \cite{RiazanovV02}; and (3)
MathServ Broker\footnote{which chooses an appropiate ATP upon a
classification of the FOL problem} \cite{ZimmerAutexier06}.
These together comprise some of the most advanced theorem provers
for first-order logic.
\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover for higher-order
logic.
\end{description}
SoftFOL and \Isabelle are currently the only logics coming with a
prover. Proof support for the other logics can be obtained by using
logic translations to a prover-supported logic.
An introduction to \CASL can be found in the \CASL User Manual
\cite{CASL-UM}; 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.
\section{Getting started}
The latest \Hets version can be obtained from the
\Hets tools home page
\begin{quote}
\texttt{http://www.dfki.de/sks/hets}
\end{quote}
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.
The \Hets installer will automatically download and install further
software (if not already installed on your computer):
\medskip
{\small
\begin{tabular}{|l|l|l|}\hline
CASL-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
uDraw(Graph) & graph drawing & \url{http://www.tzi.de/uDrawGraph/en/}\\\hline
Tcl/Tk & graphics widget system & \url{http://www.scriptics.com/software/tcltk/} \\\hline
SPASS & theorem prover & \texttt{http://spass.mpi-sb.mpg.de/}\\\hline
\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
(X)Emacs & editor (for Isabelle) & (must be installed manually)\\\hline
\end{tabular}
}
\medskip
If you want to compile \Hets from the sources, please follow the
link ``Hets: source code and information for developers''
on teh \Hets web page, download the sources (as tarball or from
cvs), and follow the
instructions in the \texttt{INSTALL} file.
\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).
\item[\texttt{--casl-amalg=ANALYSIS}]
For the analysis of architectural specification (a quite advanced
feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
amalgamability checking
algorithm for \CASL logic; it is a comma-separated list of zero or
more of the following options:
\begin{description}
\item[\texttt{sharing}] perform sharing analysis for sorts,
operations and predicates.
\item[\texttt{cell}] perform cell condition check; implies
\texttt{sharing}. With this option on the subsort embeddings are
analyzed.
\item[\texttt{colimit-thinness}] perform colimit thinness check;
implies \texttt{sharing}. The colimit thinness check is less
complete and usually takes longer than the full cell condition
check (\texttt{cell} option), but may prove more efficient in case
of certain specifications.
\end{description}
If \texttt{ANALYSIS} is empty then amalgamability analysis for
\CASL is skipped.
The default value for \texttt{--casl-amalg} is
\texttt{cell}.
\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/HasSLe & Haskell\\\hline
\texttt{.owl} & OWL DL, OWL Lite & OWL\\\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}).
(There are also heterogeneous constructs
for explicit translations between logics.)
\eat{
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 HasSLe specifications,
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-UM}, 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-UM}, 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[Red nodes] have open proof obligations.
\item[Green nodes] have all proof obligations resolved.
\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[Yellow links] correspond to open proof obligations involving hiding (hiding 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}.
\item[Single links] have homogeneous signature morphisms (staying within
one and the same logic).
\item[Double links] have heterogeneous signature morphisms (moving between
logics).
\end{description}
We now explain the menus of the development graph window.
Most of the pull-down menus of the window are uDraw(Graph)-specific
layout menus;
their function can be looked up in the uDraw(Graph) 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 the following submenus:
\begin{description}
\item[Unnamed nodes]
The ``Hide/show names'' menu is a toggle:
you can switcn on or off the display of names for nodes that
are initially unnamed. The newly named nodes get names that
are derived from named neighbour nodes.
With the ``Hide nodes'' 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 nodes'' 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}. While support for local and global
(definition or theorem) links is stable, support for hiding links
and checking conservativity is still experimental. In most cases, it is
advisable to use ``Automatic'', which automatically applies the
rules in the correct order. As a result, the the open theorem links
(marked in red) will be reduced to local proof goals, that is, they
become green, and instead, some of the node will get red, indicating
open local proof goals.
\item[Translate Graph] translates the whole development graph
along a logic comorphism.
\item[Show Logic Graph] shows the graph of logics and logic comorphisms
currently supported by \Hets.
\item[Show Library Graph] shows the graph of libraries that have
been loaded into \Hets, and their dependencies. For library,
the corresponding development graphs can be shown using its node menu.
Also, a list of specifications and views can be shown.
\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 local axioms] Shows the local axioms of the node.
\item[Show theory] Shows the theory of the node (including axioms
imported from other nodes). Warning: axioms imported via hiding links
are not part of the theory; they can be made visible only by re-adding
the hidden symbols, using the proof rule \emph{Theorem-Hide-Shift}.
\item[Translate theory] Translates the theory of a node to another logic.
A menu with the possible translation paths will be displayed.
\item[Taxonomy graphs] (Only available for some logics) Shows the subsort graph of 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 proof status] Show open and proven local proof goals.
\item[Prove] Try to prove the local proof goals. See Section~\ref{sec:Proofs}
for details.
\item[Check consistency] Check the consistency of the theory of 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.
%\item[Show spec] Show the structured specification of the node.
% (not fully implemented yet)
\item[Show number of node] Show the internal number of the node.
\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.
\item[Check conservativity] (Experimental) Check whether the
theory of the target node of the link
is a conservative extension of the theory of the source node.
\item[Show ID of this edge] Shows the internal number of the edge.
These numbers are also used in the proof status information for
edges.
\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.
The possible input types are:
\begin{verbatim}
(casl|het|owl|hs|ast[.baf]|[tree.]gen_trm[.baf])
\end{verbatim}
\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 separated list of output types:
\begin{verbatim}
env
| thy
| pp.(het|tex|html)
| graph.(dot|ps|davinci)
| ast.(het|trm|taf|html|xml)
| (fdg|hdg|dg)[.nax].(het|trm|taf|html|xml)
\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{hetcasl.sty}
coming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty)}) is used.
When the \texttt{thy} format is selected, \Hets will try to translate
each specification in the library to \Isabelle, and write one \Isabelle
\texttt{.thy} file per specification.
When the \texttt{comptable.xml} format is selected, \Hets will extract
the composition and inverse table of a Tarskian relation algebra from
specification(s) (selected with the \texttt{-n} or \texttt{--spec}
option). It is assumed that the relation algebra is
generated by basic relations, and that the specification is written
in the \CASL logic. A sample specification of a relation
algebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
available from \texttt{www.cofi.info/Libraries}.
The output format is XML, the URL of the DTD is included in the
XML file.
\item[\texttt{-t TRANS}, \texttt{--translation=TRANS}]
chooses a translation option. \texttt{TRANS} is a colon-separated list
without blanks of one or more from:
\begin{tabular}{|l|l|}\hline
CASL2CoCASL & inclusion \\\hline
CASL2CspCASL & inclusion \\\hline
CASL2HasCASL & inclusion \\\hline
CASL2Modal & inclusion \\\hline
CASL2PCFOL & coding of subsorting by injections\\\hline
CASL2SPASS & \\\hline
CASL2SubCFOL & coding of partial functions by error supersorts \\\hline
CASL2TopSort & coding of subsorting by a top sort \\\hline
CFOL2IsabelleHOL & coding of \CASL to Isabelle\\\hline
CoCASL2CoPCFOL & coding of subsorting by injections \\\hline
CoCASL2CoSubCFOL & coding of partial functions by error supersorts \\\hline
CoCFOL2IsabelleHOL & coding of \CoCASL to Isabelle \\\hline
CoPCFOL2CoCFOL & coding of partial functions by ??? \\\hline
%%CspCASL2IsabelleHOL & \\\hline
%%CspCASL2Modal & \\\hline
HasCASL2HasCASL & \\\hline
HasCASL2Haskell & translation of executable subset to Haskell \\\hline
HasCASL2IsabelleHOL & coding to Isabelle/HOL \\\hline
Haskell2IsabelleHOLCF & coding to Isabelle/HOLCF \\\hline
Modal2CASL & standard translation \\\hline
PCFOL2CFOL & ? \\\hline
PCFOL2FOL & ? \\\hline
SuleCFOL2SoftFOL & \\\hline
PCoClTyConsHOL2IsabelleHOL & \\\hline
Prop2CASL & \\\hline
PropIE2PropE & \\\hline
PropIE2PropI & \\\hline
PropIE2Prop & \\\hline
\end{tabular}
\item[\texttt{-r RAW} or \texttt{--raw=RAW}] This option allows one
to influence the formatting in more detail.
Here, \texttt{RAW} is \texttt{(ascii|text|(la)?tex)=STRING},
and \texttt{STRING} is passed to the appropriate pretty-printer.
The deatils of these options are to be fixed in the future only.
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 -KIntM -RTS}] Increase the stack size to
\texttt{Int} megabytes (needed in case of a stack overflow).
This must be the first option.
\item[\texttt{-l LOGIC}, \texttt{--logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
decelation. The default is \CASL.
\item[\texttt{-n SPECS}, \texttt{--spec=SPECS}]
chooses a list of named specifications for processing
\end{description}
\section{Proofs with \Hets}\label{sec:Proofs}
The graphical user interface (GUI) for calling a prover
is shown in Fig. \ref{fig:proof_window}. The list on the right
shows all goal names prefixed with the proof status in square
brackets. A proved goal is indicated by a '+', a '-' indicates a
disproved goal and a space denotes an open goal.
\begin{figure}
\centering
\includegraphics[width=\textwidth]{proofmanagement1}
\caption{Hets Goal and Prover Interface\label{fig:proof_window}}
\end{figure}
If you open this GUI processing the goals of one node for the first
time, it will show all goals as open. Within this list you can select
those goals that should be inspected or proved. The button 'Display'
shows the selected goals in the ASCII syntax of this theory's logic in
a separate window. With the 'Prove' button the actual prover is
launched. This is described in more detail in the following
paragraphs. By pressing the 'Show Proof Details' button a window is
opened where for each proved goal the used axioms are shown. The
'Status:' shows either 'No prover running' or 'Waiting for prover' in
black or blue. If you press the 'Close' button the window is closed
and the status of the goals' list is integrated into the
DevelopmentGraph. If all goals have been proved, the selected node
turns from red into green.
The list 'Pick Theorem Prover:' lets you choose one of the connected
provers (currently, these are SPASS and \Isabelle, described below). By
pressing 'Prove' the selected prover is launched and the theory along
with the selected goals is translated via the shortest possible path
of comorphims into the provers logic. The button 'More fine grained
selection...' lets you pick a (composed) comorphism in a separate
window from where the prover is launched then.
\subsection*{SPASS}
\begin{figure}
\centering
\includegraphics[width=\textwidth]{spassGUI1}
\caption{Interface of the SPASS prover\label{fig:SPASS_GUI}}
\end{figure}
The automatic theorem prover SPASS
\cite{WeidenbachEtAl02} is a resultion-based prover for first-order logic
with equality.
If you have choosen SPASS, initially, all selected goals are tried in a
row. After this so called batch mode the results are displayed in a
window which is shown in Fig. \ref{fig:SPASS_GUI}. This GUI for the
theorem prover SPASS is very similiar to the 'Select Goal(s) and
Prove' GUI which lets you choose a prover for some goals. But with the
SPASS GUI, the actual SPASS prover is launched with the selected
goal. Further it is possible to set a time-limt and some options for
SPASS. The available options are shown in separate window by pressing
the 'Help' button. The status of the selected goal is shown in the
'Status:' line with either 'Proved', 'Disproved', 'Open' or 'Open Time
(Time is up!)'. If a goal has been proved the labels of the used
axioms are shown in the list on the right. The button 'Show Details'
shows the whole output of SPASS. 'Save Prover Configuration allows you
to save the configuation and status of each proof for
documentation. By pressing the button 'Exit Prover' the status of
these proofs and goals is transferred back to the main 'Select Goal(s)
and Prove' window.
\subsection*{Isabelle}
\Isabelle \cite{NipPauWen02} is an interactive theorem prover, which is
more powerful than SPASS, but also requires more user interaction.
\Isabelle
has a very small core guaranteeing correctness, and its provers,
like the simplifier or the tableaux prover, are built on top of this
core. Furthermore, there is over fifteen years of experience with it,
and several mathematical textbooks have been partially
\index{formal!verification}%
verified with
\Isabelle.
\Isabelle is a tactic based theorem prover implemented in standard ML.
The main \Isabelle logic (called Pure) is some weak intuitionistic type
theory with polymorphism. The logic Pure is used to represent a
variety of logics within \Isabelle; one of them being \HOL (higher-order
logic). For example, logical implication in Pure (written
\texttt{==>}, also called meta-implication), is different from logical
implication in \HOL (written \texttt{-->}, also called object
implication).
It is essential to be aware of the fact that the \Isabelle/\HOL logic
is different from the logics that are encoded into it via comorphisms.
Therefore, the formulas appearing in subgoals of proofs with \Isabelle
will not conform to the syntax of the original input logic. They may
even use features of \Isabelle/\HOL such as higher-order functions
that are not present in an input logic like \CASL.
\Isabelle is started with ProofGeneral
\cite{DBLP:conf/tacas/Aspinall00,url:ProofGeneral} in a separate Emacs
\cite{url:Emacs,url:XEmacs}.
The \Isabelle theory file conforms to the Isabelle/Isar syntax
\cite{NipPauWen02}. It starts with the theory (encoded along the selected
comorphism), followed by a list of theorems. Initially, all the
theorems have trivial proofs, using the `oops` command. However, if
you have saved earlier proof attempts, \Hets will patch these into
the generated \Isabelle theory file, ensuring that your previous work
is not lost. (But note that this patching can only be successful
if you do not rename specifications, or change their structure.) You
now can replace the 'oops' commands with real \Isabelle proofs, and
use Proof General to step through the proofs. You finish your session
by saving your file (using the Emacs file menu, or the Ctrl-x Ctrl-s
key sequence), and pressing a button in a small pop-up window
generated by \Hets.
\section{Limits of \Hets}
\Hets is still intensively under development. In particular, the
following points are still missing:
\begin{itemize}
\item There is no proof support for architectural specifications.
\item Distributed libraries are always downloaded from the local disk,
not from the Internet.
\item Version numbers of libraries are not considered properly.
\item The proof engine for development graphs provides only experimental
support for hiding links and for conservativity.
\end{itemize}
\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.5]{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-devel@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 (Christian.Maeder@dfki.de) and Till Mossakowski
(Till.Mossakowski@dfki.de). The mailing list is \url{hets-devel@tzi.de},
the homepage is
\paragraph{Acknowledgement}
The heterogeneous tool set \Hets, which shows that the theory outlined
in this work can also be brought to practice, would not have possible
without cooperation with Christian Maeder and Klaus L\"uttich.
Besides the author, the following people have been involved
in the implementation of \Hets:
Katja Abu-Dib,
Carsten Fischer,
Jorina Freya Gerken,
Sonja Gr\"{o}ning,
Wiebke Herding,
Heng Jiang,
Anton Kirilov,
Tina Krausser,
Martin K\"{u}hl,
Mingyi Liu,
Klaus L\"{u}ttich,
Christian Maeder,
Maciek Makowski,
Razvan Pascanu,
Daniel Pratsch,
Felix Reckers,
Markus Roggenbach,
Pascal Schmidt and
Paolo Torrini.
\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}
provides parsing and static analysis for \CASL.
It has been developed by the present author with help
of Mark van den Brand, Kolyang, Bartek Klin, Pascal Schmidt and
Frederic Voisin.
\MAYA \cite{Autexier:2002:IHD,AutexierEtal02} is a proof management
tool based on development graphs. \MAYA only supports development
graphs without hiding and without logic translations. \MAYA has been
developed by Serge Autexier and Dieter Hutter.
I also want to thank Agn\`es Arnould, Thibaud Brunet, Pascale LeGall,
Kathrin Hoffmann, Katiane Lopes, Klaus L\"uttich, Christian Maeder,
Stefan Merz, Maria Martins Moreira, Christophe
Ringeissen, Markus Roggenbach, Dmitri Schamschurko, Lutz Schr\"oder,
Konstantin Tchekine and Stefan W\"olfl
for giving feedback about \Cats, HOL-CASL and \Hets. Finally,
special thanks to Christoph L\"uth and George Russell
for help with connecting \Hets to their UniForM workbench.
\bibliographystyle{plain}
\bibliography{cofibib,cofi-ann,UM,hets,kl}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "UserGuide"
%%% End: