UserGuide.tex revision 91dd24480df03b2cca7c1645bb2866d7000dfdb1
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\documentclass{article}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{alltt}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{casl}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{color}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\QUERY}[1]%{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\eat}[1]{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\IEXT}[1] {\\#1\I}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\IEND} {\I\END}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{EXAMPLEFORMAT} {}{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%% Added by MB to have some extra vertical space after the ``main'' examples
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%% following the points (and some others in the text):
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{BIGEXAMPLE} {\begin{EXAMPLE}} {\end{EXAMPLE}\medskip}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{DETAILSFORMAT} {}{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{META}[1][] {#1\begin{METAFORMAT}}{\end{METAFORMAT}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{METAFORMAT} {\medskip\vrule\hspace{1ex}\vrule\hspace{1ex}%
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \begin{minipage}{0.9\textwidth}\it}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski {\end{minipage}\par\medskip}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\SLIDESMALL} {}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\SLIDESONLY}[1] {}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% SIMULATING SMALL-CAPS FOR BOLD, EMPH
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%\newcommand {\CoFI}{CoFI\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeELAN} {\largeTEXTSC{E}{LAN}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HOL}{\normalTEXTSC{H}{OL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Isabelle}{\normalTEXTSC{I}{SABELLE}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%%%%% Klaus macros
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%%%%% end of Klaus macros
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LCF}{LCF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\ASF}{ASF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SDF}{SDF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski%% Do NOT use \ASF+\SDF (it gives a superfluous space in the middle)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CCC}{CCC\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CoCASL}{\normalTEXTSC{C}{O}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CspCASL}{\normalTEXTSC{C}{SP}-\normalTEXTSC{C}{ASL}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{document}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\title{{\bf \protect{\LARGEHets} User Guide}\\
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski-- Version 0.44 --}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\author{Till Mossakowski\\[1em]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDepartment of Computer Science\\ and Bremen
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiInstitute for Safe Systems,\\ University of Bremen, Germany.\\[1em]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiComments to: hets@tzi.de
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Introduction}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe Heterogeneous Tool Set (\protect\Hets) is the main analysis tool
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor the specification language heterogeneous \CASL. Heterogeneous
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\CASL (\HetCASL) combines the specification language \CASL with \CASL extensions
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowskiand sublanguages, as well as completely different logics and even
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiprogramming languages such as Haskell. \HetCASL
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowskiextends the structuring mechanisms of \CASL:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{Basic specifications} are
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiunstructured specifications or modules written in a specific logic.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe graph of currently supported logics is shown in Fig.~\ref{fig:LogicGraph},
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiand the degree of support by \Hets in Fig.~\ref{fig:Languages}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWith \emph{heterogeneous structured specifications}, it is possible to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicombine and rename specifications, hide parts thereof, and also
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitranslate them to other logics. \emph{Architectural specifications}
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowskiprescribe the structure of implementations. \emph{Specification
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski libraries} are collections of named structured and architectural
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets consists of logic-specific tools for the parsing and static
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskianalysis of the different involved logics, as well as a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogic-independent parsing and static analysis tool for structured and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiarchitectural specifications and libraries. The latter of course needs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito call the logic-specific tools whenever a basic specification is
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\section{Logics supported by \Hets}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \begin{center}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \includegraphics[scale=0.4]{LogicGraph}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\caption{Graph of logics currently supported by \Hets. The more an
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiellipse is filled, the more stable is the implementation of the logic.}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\label{fig:LogicGraph}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{figure}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{center}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{tabular}{|l|c|c|c|}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiLanguage & Parser & Static Analysis & Prover \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CASL & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CoCASL & x & x & - \\\hline
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski\ModalCASL & x & x & - \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\HasCASL & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiHaskell & x & x & -\\\hline
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\CspCASL & (x) & - & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Structured specifications & x & x & (x) \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Architectural specifications & x & x & -\\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CASLDL & x & - & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiOWL DL basic & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiOWL DL structure & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiSPASS & - & - & x \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiIsabelle & - & - & x \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\caption{Current degree of \Hets support for the different languages.\label{fig:Languages}}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{description}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[CASL] extends many sorted first-order logic with partial
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski functions and subsorting. It also provides induction sentences,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski expressing the (free) generation of datatypes.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%It is mainly designed and used for the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%specification of requirements for software systems. But it is also
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%used for the specification of \Dolce (Descriptive Ontology for
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Linguistic and Cognitive Engineering), an Upper Ontology for knowledge
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%representation. \cite{Gangemi:2002:SOD} Further it is now used to
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%specify calculi for time and space.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiFor more details on \CASL see \cite{CASL-RM,CASL-UM}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiWe have implemented the \CASL logic in such a way that much of the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiimplementation can be re-used for \CASL extensions as well; this
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiis achieved via ``holes'' (realized via polymorphic variables) in the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskitypes for signatures, morphisms, abstract syntax etc. This eases
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiintegration of \CASL extensions and keeps the effort of integrating
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CASL extensions quite moderate.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[CoCASL] \cite{MossakowskiEA04} is a coalgebraic extension of \CASL,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskisuited for the specification of process types and reactive system.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe central proof method is coinduction.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[ModalCASL] is an extension of \CASL with multi-modalities and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiterm modalities. It allows the specification of modal systems with
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiKripke's possible worlds semantics. It is also possible to express
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicertain forms of dynamic logic.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[HasCASL] is a higher order extension of \CASL allowing
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski polymorphic datatypes and functions. It is closely related to the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski programming language Haskell and allows program constructs being
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski embedded in the specification.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithe language is summarized in \cite{HasCASL/Summary}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe latter document is also available on the CD-ROM
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[Haskell] is a modern, pure and strongly typed functional
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski programming language. It simultaneously is the implementation
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski language of \Hets, such that in the future, \Hets might be applied
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe definitive reference for Haskell is \cite{PeytonJones03},
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[CspCASL] \cite{Roggenbach:2003:C-CN} is a combination of \CASL
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski with the process algebra CSP.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[OWL DL] is the Web Ontology Language (OWL) recommended by the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski World Wide Web Consortium (W3C, \texttt{http://www.w3c.org}). It is
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski used for knowledge representation and the Semantic Web
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \cite{berners:2001:SWeb}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiHets calls an external OWL DL parser
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski written in JAVA to obtain the abstract syntax for an OWL file and its
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski imports. The JAVA parser is also doing a first analysis classifying
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski the OWL ontology into the sublanguages OWL Full, OWL DL and OWL
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Hets only supports the last two, more restricted variants.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski structuring of the OWL imports is displayed as Development Graph.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[CASL-DL] is an extension of a restriction of \CASL, realizing
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskia strongly typed variant of OWL DL in \CASL syntax.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \CASL with cardinality restrictions for the description of sorts and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski unary predicates. The restrictions are based on the equivalence
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski between \CASLDL, OWL~DL and \SHOIN. Compared to \CASL only unary
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski and binary predicates, predefined datatypes and concepts (subsorts
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski of the topsort Thing) are allowed. It is used to bring OWL DL and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \CASL closer together.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[SPASS] \cite{WeidenbachEtAl02} is an automatic theorem prover for first-order logic
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiwith equality.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[Isabelle] \cite{NipPauWen02} is an interactive theorem prover for higher-order
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\end{description}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiSPASS and Isabelle are the only logics coming with a prover. Proof
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskisupport for the other logics can be obtained by using logic translations
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskito a prover-supported logic.
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.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Getting started}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe latest \Hets version can be obtained from the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\Hets tools home page
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski Since \Hets is being
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiimproved constantly, it is recommended always to use the latest version.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets currently is available for Linux, Solaris and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiMacIntosh users need to install some libraries, which can be found
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiat the \Hets download page.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiIf you want to compile \Hets from the sources, please follow the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskilink ``Hets: source code and information for developers''
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskion teh \Hets web page, download the sources (as tarball or from
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicvs), and follow the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiinstructions in the \texttt{INSTALL} file.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\subsection*{uDraw(Graph)}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiFor the display of development graphs (with the -g option), \Hets uses
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiuDraw(Graph), formerly known as daVinci.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiYou can get uDraw(Graph) freely from
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiMoreover, you need Tcl/Tk as well, available freely from
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\url{http://www.scriptics.com/software/tcltk/}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiBut Tcl/Tk probably has been already installed
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskion your computer anyway.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiSet the environment variable \texttt{\$UNIWISH} to the wish binary
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski(which is part of Tcl/Tk), and \texttt{\$UNIDAVINCI} to the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiuDraw(Graph) binary. Furthermore, uDraw(Graph) requires that
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\texttt{DAVINCIHOME} is set to the installation directory of
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\subsection*{Isabelle}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiFor theorem proving with Isabelle, you need to install Isabelle,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiwhich is available freely from
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiWe recommend to use the latest version (Isabelle 2005), together
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiwith Proof General, a proof interface that comes with the Isabelle
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidistribution. Proof General uses the Eamcs or Xemacs editor.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiSet the environment variable
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\texttt{\$HETS\_ISABELLE} to the Isabelle (or Emacs, for use with proof general) binary, and set \texttt{\$LC\_CTYPE} to \texttt{C}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\subsection*{SPASS}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiFor theorem proving with SPASS, obtain SPASS freely from
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\subsection*{Libraries of specifications}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiA repository of libraries of specifications for use with \Hets
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiis available under \url{http://www.cofi.info/Libraries}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe environment variable \texttt{HETS\_LIB} should be set to
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskia location where the specification libraries are stored.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski%\QUERY{This should be done by the install script!}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Analysis of Specifications}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiConsider the following \CASL
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecification:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{Strict\_Partial\_Order} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\PRED]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SORT \( Elem \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% \COMMENTENDLINE{\PRED abbreviates predicate}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL x,y,z : Elem \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{COMMENT}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiNote that there may exist \(x, y\) such that\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskineither \(x < y\) nor \(y < x\).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets can be used for parsing and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskichecking static well-formedness of specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{parsing}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{static!analysis}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{analysis, static}%
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiLet us assume that the example is in a file named
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{Order.casl} (actually, this file is provided
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiwith the \Hets distribution).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThen you can check the well-formedness of the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispecification by typing (into some shell):
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets checks both the correctness of this specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski with respect to the \CASL syntax, as
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwell as its correctness with respect to the static semantics (e.g.\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhether all identifiers have been declared before they are used,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhether operators are applied to arguments of the correct sorts,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhether the use of overloaded symbols is unambiguous, and so on).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe following flags are available in this context:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing -- the static analysis
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-s}, \texttt{--just-structured}]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiDo the parsing and the static analysis of (heterogeneous) structured
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecifications, but leave out the analysis of basic specifications.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThis can be used to quickly produce a development graph
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskishowing the dependencies among the specifications (cf. Sect.~\ref{sec:DevGraph}).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiUse \texttt{DIR} as the directory for specification libraries
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(equivalently, you can set the variable \texttt{HETS\_LIB} before
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskicalling \Hets).
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\item[\texttt{--casl-amalg=ANALYSIS}]
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski For the analysis of architectural specification (a quite advanced
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski amalgamability checking
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski algorithm for \CASL logic; it is a comma-separated list of zero or
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski more of the following options:
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \begin{description}
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \item[\texttt{sharing}] perform sharing analysis for sorts,
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski operations and predicates.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \item[\texttt{cell}] perform cell condition check; implies
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \texttt{sharing}. With this option on the subsort embeddings are
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \item[\texttt{colimit-thinness}] perform colimit thinness check;
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski implies \texttt{sharing}. The colimit thinness check is less
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski complete and usually takes longer than the full cell condition
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski check (\texttt{cell} option), but may prove more efficient in case
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski of certain specifications.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \end{description}
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski If \texttt{ANALYSIS} is empty then amalgamability analysis for
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \CASL is skipped.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski The default value for \texttt{--casl-amalg} is
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \texttt{cell}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Heterogeneous Specification} \label{sec:HetSpec}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Hets accepts plain text input files with the following endings:\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{tabular}{|l|c|c|}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiEnding & default logic & structuring language\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.casl} & \CASL & \CASL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.het} & \CASL & \CASL \\\hline
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill Mossakowski\texttt{.hs} & Haskell/HasSLe & Haskell\\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\texttt{.owl} & OWL DL, OWL Lite & OWL\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiAlthough the endings \texttt{.casl} and \texttt{.het} are
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinterchangeable, the former should be used for libraries of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskihomogeneous \CASL specifications and the latter for \HetCASL libraries
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiof heterogeneous specifications (that use the \CASL structuring
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiconstructs). Within a \HetCASL library, the current logic can be changed e.g.\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskito \HasCASL in the following way:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe subsequent specifications are then parsed and analysed as
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\HasCASL specifications. Within such specifications,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiit is possible to use references to named \CASL specifications;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithese are then automatically translated along the default
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiembedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(Heterogeneous constructs
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifor explicit translations between logics will be made available
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiin the future.)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiA \CspCASL specification consists of a \CASL specification
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifor the data part and a \Csp process built over this data part.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiTherefore, \HetCASL provides a heterogeneous language construct
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{data} as follows:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilibrary Buffer
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski free type List[Elem] ::= nil | cons(Elem; List[Elem])
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski channel read, write : Elem
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski let Buf(l:List[Elem]) =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski read?x -> Buf( cons(x,nil) )
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski [] if l=nil then STOP else write!last(l) -> Buf( rest(l) )
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHere, the construct \texttt{data List} refers to the \CASL specification
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{List}, which is implicitly embedded into \CspCASL.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe ending \texttt{.hs} is available for directly reading in
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill MossakowskiHaskell programs and HasSLe specifications,
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill Mossakowskiand hence supports the Haskell module system.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithe logic Haskell has to be chosen explicitly, and the \CASL structuring
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisyntax needs to be used:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilibrary Factorial
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispec Factorial =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifac :: Int -> Int
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifac n = foldl (*) 1 [1..n]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiNote that according to the Haskell syntax, Haskell function
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskideclarations and definitions need to start with the first column of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Development Graphs}\label{sec:DevGraph}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDevelopment graphs are a simple kernel formalism for (heterogeneous)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskistructured theorem proving and proof management. A development graph
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiconsists of a set of nodes (corresponding to whole structured
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecifications or parts thereof), and a set of arrows called
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidefinition links, indicating the dependency of each involved
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskistructured specification on its subparts. Arising proof obligations
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiare attached as so-called theorem links to this graph.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe following options let \Hets show the development graph of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskia specification library:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-G}, \texttt{--only-gui}] Shows the development graph in a GUI window,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiand suppresses the writing of an output file.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiLet us extend the above library \texttt{Order.casl}. One use of the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilibrary might be to express the fact that the natural numbers form a
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskistrict partial order as a view, as follows:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{EXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEDEFN{Natural\_Order\_2} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{Natural}} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\PRED \( \_\_<\_\_ : Nat \* Nat\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL x,y:Nat \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. 0 < suc(x) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. \neg x < 0 \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. suc(x) < suc(y) \IFF x < y
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{EXAMPLE}%[\SLIDESMALL]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{Natural\_Order\_2} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I{} \( Elem \MAPSTO Nat\)
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAgain, these specifications can be checked with \Hets. However, this
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskionly checks syntactic and static semantic well-formedness -- it is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiby a strict partial ordering relation. Checking this requires theorem
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproving, which will be discussed below.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHowever, before coming to theorem proving, let us first inspect the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof obligations arising from a specification. This can be done with:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{hets -g Order.casl}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(assuming that the above two specifications and the view
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskihave been added to the file
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets now displays a so-called development graph
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(which is just an overview graph showing the overall structure
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof the specifications in the library), see Fig.~\ref{fig:dg0}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{center}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\includegraphics[scale=0.7]{dg-order-0}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Sample development graph.\label{fig:dg0}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiNodes in a development graph correspond to \CASL specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiArrows show how specifications are related by the structuring
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe black arrow denotes an ordinary import of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecifications (generated by the extension), while the red arrow
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidenotes a proof obligation (corresponding to the view).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThis proof obligation needs to be discharged in order to
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskishow that the view is well-formed (then its color turns into green).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAs a more complex example, consider the following loose specification
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof a sorting function, taken from the \CASL User Manual
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{List\_Order\_Sorted}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\WITHIN]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\PRED]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\PRED \( \_\_is\_sorted : List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL e,e': Elem; L : List \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. empty~is\_sorted \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. cons(e,empty)~is\_sorted \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. cons(e,cons(e',L))~is\_sorted \IFF
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\OP \( order : List \TOTAL List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following specification of sorting by insertion also is taken from
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithe \CASL User Manual \cite{CASL/UserManual}, Chap.~6:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{List\_Order}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\phantomsection
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\WITHIN]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\OP \( insert : Elem \* List \TOTAL List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL e,e':Elem; L:List \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. insert(e, empty) = cons(e, empty) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. insert(e, cons(e',L)) = \[ cons(e', insert(e,L)) \WHEN e' < e\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ELSE cons(e, cons(e',L)) \] \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\OP \( order : List \TOTAL List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL e:Elem; L:List \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. order(empty) = empty \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. order(cons(e,L)) = insert(e, order(L)) \]\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBoth specifications are related. To see this, we first inspect
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitheir signatures. This is possible with:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{hets -g Sorting.casl}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiassuming that \texttt{Sorting.casl} contains the above specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{center}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\includegraphics[scale=0.7]{dg-order-1}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Development graph for the two sorting specifications.\label{fig:dg1}}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn the above-mentioned development graph, we have two types of nodes.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe named ones correspond to named specifications, but there
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiare also unnamed nodes corresponding to anonymous basic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispecifications like the declaration of the $insert$ operation in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order} above. Basically, there is an
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiunnamed node for each structured specification that is not named.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAgain, the black arrows denote an ordinary import of specifications
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(corresponding to the extensions and unions in the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecifications), while the blue arrows denote hiding (corresponding to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe local specification).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBy clicking on the nodes, one can inspect their signatures.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn this way, we can see that both \NAMEREF{List\_Order\_Sorted} and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order} have the same signature. Hence, it
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis legal to add a view:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{EXAMPLE}%[\SLIDESMALL]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\VIEW \NAMEDEFN{v2}[\NAMEREF{Total\_Order}] ~:~ \NAMEREF{List\_Order\_Sorted}[\NAMEREF{Total\_Order}] \TO
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order}[\NAMEREF{Total\_Order}]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWe have already added this view to \texttt{Sorting.casl}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe corresponding
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof obligation between \NAMEREF{List\_Order\_Sorted} and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order} is displayed in Fig.~\ref{fig:dg1}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski as a red arrow.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHere is a summary of the types of nodes and links occurring in
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidevelopment graphs:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Named nodes] correspond to a named specification.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Unnamed nodes] correspond to an anonymous specification.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Elliptic nodes] correspond to a specification in the current library.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Rectangular nodes] are external nodes corresponding
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski to a specification downloaded from
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskianother library.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Black links] correspond to reference to other specifications
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(definition links in the sense of \cite[IV:4]{CASL/RefManual}).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Blue links] correspond to hiding (hiding definition links).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Red links] correspond to open proof obligations (theorem links).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Green links] correspond to proved proof obligations (theorem links).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Solid links] correspond to global (definition or theorem)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilinks in the sense of \cite[IV:4]{CASL/RefManual}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Dashed links] correspond to local (definition or theorem) links in the sense of \cite[IV:4]{CASL/RefManual}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiWe now explain the menus of the development graph window.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiMost of the pull-down menus of the window are uDraw(Graph)-specific
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskitheir function can be looked up in the uDraw(Graph) documentation.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe exception is the Edit menu. Moreover, the nodes and links
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof the graph have attached pop-up menus, which appear when
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiclicking with the right mouse button.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Edit] This menu has two submenus:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[Unnamed nodes]
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe ``Hide/show names'' menu is a toggle:
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiyou can switcn on or off the display of names for nodes that
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiare initially unnamed. The newly named nodes get names that
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiare derived from named neighbour nodes.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiWith the ``Hide nodes'' submenu, it is possible
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskito reduce the complexity of the graph by hiding all unnamed nodes;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskionly nodes corresponding to named specifications remain displayed.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiPaths between named nodes going through unnamed nodes
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiare displayed as links. With the ``Show nodes'' submenu, the unnamed
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskinodes re-appear.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Proofs] This menu allows to apply some of the deduction
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskirules for development graphs, see Sect. IV:4.4 of the \CASL
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiReference Manual \cite{CASL/RefManual}. While support for
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskilocal and global (definition or theorem) links is stable,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskisupport for hiding links and consistency checking is still
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Pop-up menu for nodes]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHere, the number of submenus depends on the type of the node:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show signature] Shows the signature of the node.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show sublogic] Shows the logic and, within that logic, the minimal sublogic
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifor the signature and the axioms of the node.
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\item[Show origin] Shows the kind of \CASL structuring construct that
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskiled to the node.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show just subtree] (Only for named nodes) Reduce the complexity
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof the graph by just showing the subtree below the current node.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Undo show just subtree] (Only for named nodes) Undo the reduction.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show referenced library] (Only for external nodes) Open a new window
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskishowing the development graph for the library the external node refers to.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Pop-up menu for links]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAgain, the number of submenus depends on the type of the node:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show morphism] Shows the signature morphism of the link. It consists
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof two components: a logic translation and a signature morphism in the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitarget logic of the logic translation.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiIn the (most frequent) case
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof an intra-logic signature morphism, the logic translation component is
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskijust the identity.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show origin] Shows the kind of \CASL structuring construct that
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiled to the link.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show proof status] (Only for theorem links) Show the proof status.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\section{Reading, Writing and Formatting}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Hets provides several options controlling the types of files
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithat are read and written.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-i ITYPE}, \texttt{--input-type=ITYPE}] Specify
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\texttt{ITYPE} as the type of the input file. The default is
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\texttt{het} (\HetCASL plain text). \texttt{ast} is for reading
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiin abstract syntax trees in ATerm format, while \texttt{ast.baf}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskireads in the compressed ATerm format.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-O DIR}, \texttt{--output-dir=DIR}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiSpecify \texttt{DIR} as destination directory for output files.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-o OTYPES}, \texttt{--output-types=OTYPES}]
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\texttt{OTYPES} is a comma separated list of output types:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{verbatim}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (ast|[fh]?dg(.nax)?).(het|trm|taf|html|xml)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |(pp.(het|tex|html))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |(graph.(dot|ps|davinci))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{verbatim}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe default is \texttt{dg.taf}, which means that the development
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskigraph of the library is stored in textual ATerm format (\texttt{taf}).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThis format can be read in when a library is downloaded from
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskianother library, avoiding the need to re-analyse the downloaded library.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe \texttt{pp} format is for pretty printing, either as plain text
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(\texttt{het}), \LaTeX input (\texttt{tex}) or HTML (\texttt{html}).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiA formatter with pretty-printed output currently is available only for
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithe \CASL logic. For example, it is possible to generate a pretty
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiprinted \LaTeX\ version of \texttt{Order.casl} by typing:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThis will generate a file \texttt{Order.pp.tex}. It can be included
e8f5a6ef56e210093ad852ed147d7f5f0a24cce9Till Mossakowskiinto \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
e8f5a6ef56e210093ad852ed147d7f5f0a24cce9Till Mossakowskicoming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty)}) is used.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe option \texttt{-r RAW} or \texttt{--raw=RAW} allows one
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskito influence the formatting in more detail.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHere, \texttt{RAW} is \texttt{(ascii|text|(la)?tex)=STRING},
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskiand \texttt{STRING} is passed to the appropriate pretty-printer.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiThe deatils of these options are to be fixed in the future only.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe other output formats are for future usage.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Miscellaneous Options}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-v[Int]}, \texttt{--verbose[=Int]}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiSet the verbosity level according to \texttt{Int}. Default is 1.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-q}, \texttt{--quiet}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiBe quiet -- no diagnostic output at all. Overrides -v.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-V}, \texttt{--version}] Print version number and exit.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-h}, \texttt{--help}, \texttt{--usage}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiPrint usage information and exit.
a231094086321e19f9a689de4745512c91e00e4bTill Mossakowski\item[\texttt{+RTS -KIntM -RTS}] Increase the stack size to
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \texttt{Int} megabytes (needed in case of a stack overflow).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThis must be the first option.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\section{Limits of \Hets}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\Hets is still intensively under development. In particular, the
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskifollowing points are still missing:
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\begin{itemize}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\item There is no static analysis for architectural specifications.
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\item Distributed libraries are always downloaded from the local disk,
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskinot from the Internet.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\item Version numbers of libraries are not considered properly.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\item The proof engine for development graphs has not been completed.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets has been built based on experiences with its
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \index{Cats@\Cats}%
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \index{Maya@\MAYA}%
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe \CASL Tool Set (\Cats)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\cite{Mossakowski:2000:CST,Mossakowski:1998:SSA}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicomes with similar analysis tools as \Hets (only for \CASL).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Cats should be used if a static analysis of architectural
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecifications is needed, because this is not available
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%but neither supports extensions nor does it identify
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%sublanguages of \CASL (and the tools to be used with
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%sublanguages only).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe management of development graphs is not integrated
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskibut is provided with a stand-alone version of the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskitool \MAYA \cite{Autexier:2002:IHD,AutexierEtal02}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%(which only supports part of \CASL's
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%structuring constructs; in particular, hiding is not supported).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Cats and \MAYA
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%are mainly important in the current transition phase,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%since \Hets does not support full \CASL (e.g. architectural
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%specifications) yet.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski can be obtained from the \CoFI tools home page \cite{CoFITools}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Architecture of \Hets}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets is written in Haskell. Its parser uses combinator
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{parsing}%
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe user-defined (also known as ``mixfix'') syntax of \CASL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicalls for a two-pass approach. In the first pass, the skeleton of a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\CASL abstract syntax tree is derived, in order to extract user-defined
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisyntax rules. In a second pass, which is performed during
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskianalysis, these syntax rules are used to parse
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiany expressions that
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiuse mixfix notation. The output is stored in the so-called
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{ATerms}%
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiATerm format \cite{BJKO00}, which is used as interchange format
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor interfacing with other tools.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets provides an abstract interface for
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{institution!independence}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{independence, institution}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinstitutions, so
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithat new logics can be integrated smoothly.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn order to do so, a parser,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskia static checker and a prover for basic specifications in the logic have
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito be provided.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\includegraphics[scale=0.44]{hets}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Architecture of the heterogeneous tool set.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{fig:hets}}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe architecture of \Hets is shown in Fig.~\ref{fig:hets}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIf your favourite logic is missing in \Hets, please tell us
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski(hets@tzi.de). We will take account your feedback when deciding which
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogics and proof tools to integrate next into \Hets. Help with
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiintegration of more logics and proof tools into \Hets is also welcome.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets is mainly maintained by
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiChristian Maeder (maeder@tzi.de) and Till Mossakowski
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(till@tzi.de). The mailing list is hets@tzi.de.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\paragraph{Acknowledgement}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets has been programmed by the following people:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiKatja Abu-Dib,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiCarsten Fischer,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiJorina Freya Gerken,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiSonja Gr\"{o}ning,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiWiebke Herding,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMartin K\"{u}hl,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiKlaus L\"{u}ttich,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiChristian Maeder,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMaciek Makowski,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiTill Mossakowski,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiDaniel Pratsch,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiFelix Reckers,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMarkus Roggenbach,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiPascal Schmidt.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\Hets also benefited much from contributions by Serge Autexier, Dieter
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiHutter and Bartek Klin (through work on its precursors \Cats and
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\bibliographystyle{plain}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\bibliography{cofibib,cofi-ann,UM,hets,kl}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{document}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% Local Variables:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% mode: latex
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% TeX-master: "UserGuide"