UserGuide.tex revision 2ef350ad6e8df3c2c1d76bb6a9dca42a267b3eb1
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\documentclass{article}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\usepackage{alltt}
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski\usepackage{casl}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\usepackage{xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{color}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\newcommand{\QUERY}[1]%{}
1d9290e729b7cd9a6f666432934fd890a9766fbdChristoph Lange{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\newcommand{\eat}[1]{}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\newcommand{\IEXT}[1] {\\#1\I}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\IEND} {\I\END}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newenvironment{EXAMPLEFORMAT} {}{}
5277e290ad70afdf97f359019afd8fb5816f4102Till 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] {}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski% SIMULATING SMALL-CAPS FOR BOLD, EMPH
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\newcommand {\CoFI}{CoFI\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%%%% Klaus macros
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%%%% end of Klaus macros
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LCF}{LCF\xspace}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\newcommand{\ASF}{ASF\xspace}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\SDF}{SDF\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% Do NOT use \ASF+\SDF (it gives a 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}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{document}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\title{{\bf \protect{\LARGEHets} User Guide}\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski-- Version 0.5 --}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\author{Till Mossakowski\\[1em]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDepartment of Computer Science\\ and Bremen
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiInstitute for Safe Systems,\\ University of Bremen, Germany.\\[1em]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiComments to: hets-devel@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
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\CASL (\HetCASL) combines the specification language \CASL with \CASL extensions
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederand sublanguages, as well as completely different logics and even
533d6033bec94a46d13b73cafe40953f699757c7Christian Maederprogramming languages such as Haskell. \HetCASL
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederextends the structuring mechanisms of \CASL:
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder\emph{Basic specifications} are
d78a2b8c5a63f3e63393e5cc44a5e9b253ac459bChristian Maederunstructured specifications or modules written in a specific logic.
464c78620a182d2e8fbd125098045eae8788e2bdTill MossakowskiThe graph of currently supported logics and logic translations (the
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowskilatter are also called comorphisms) is shown in
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFig.~\ref{fig:LogicGraph}, and the degree of support by \Hets in
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFig.~\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}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiprescribe the structure of implementations. \emph{Specification
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski libraries} are collections of named structured and architectural
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskispecifications.
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski\Hets consists of logic-specific tools for the parsing and static
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowskianalysis of the different involved logics, as well as a
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowskilogic-independent parsing and static analysis tool for structured and
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowskiarchitectural specifications and libraries. The latter of course needs
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowskito call the logic-specific tools whenever a basic specification is
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\section{Logics supported by \Hets}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{figure}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \begin{center}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \includegraphics[scale=0.4]{LogicGraph}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\caption{Graph of logics currently supported by \Hets. The more an
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiellipse is filled, the more stable is the implementation of the logic.}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\label{fig:LogicGraph}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{figure}
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder\begin{center}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{tabular}{|l|c|c|c|}\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiLanguage & Parser & Static Analysis & Prover \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\CASL & x & x & - \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\CoCASL & x & x & - \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\ModalCASL & x & x & - \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\HasCASL & x & x & - \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiHaskell & x & x & -\\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\CspCASL & (x) & - & - \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski%Structured specifications & x & x & (x) \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski%Architectural specifications & x & x & -\\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\CASLDL & x & - & - \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiOWL DL basic & x & (x) & - \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiOWL DL structure & x & (x) & - \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiSPASS & - & - & x \\\hline
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\Isabelle & - & - & x \\\hline
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\caption{Current degree of \Hets support for the different languages.\label{fig:Languages}}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{description}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[CASL] extends many sorted first-order logic with partial
30256573a343132354b122097b0ee1215dda1364Till Mossakowski functions and subsorting. It also provides induction sentences,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski expressing the (free) generation of datatypes.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski%It is mainly designed and used for the
30256573a343132354b122097b0ee1215dda1364Till Mossakowski%specification of requirements for software systems. But it is also
30256573a343132354b122097b0ee1215dda1364Till Mossakowski%used for the specification of \Dolce (Descriptive Ontology for
30256573a343132354b122097b0ee1215dda1364Till Mossakowski%Linguistic and Cognitive Engineering), an Upper Ontology for knowledge
30256573a343132354b122097b0ee1215dda1364Till Mossakowski%representation. \cite{Gangemi:2002:SOD} Further it is now used to
30256573a343132354b122097b0ee1215dda1364Till Mossakowski%specify calculi for time and space.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiFor more details on \CASL see \cite{CASL-RM,CASL-UM}.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiWe have implemented the \CASL logic in such a way that much of the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiimplementation can be re-used for \CASL extensions as well; this
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiis achieved via ``holes'' (realized via polymorphic variables) in the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitypes for signatures, morphisms, abstract syntax etc. This eases
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiintegration of \CASL extensions and keeps the effort of integrating
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\CASL extensions quite moderate.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[CoCASL] \cite{MossakowskiEA04} is a coalgebraic extension of \CASL,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisuited for the specification of process types and reactive system.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe central proof method is coinduction.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[ModalCASL] is an extension of \CASL with multi-modalities and
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederterm modalities. It allows the specification of modal systems with
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiKripke's possible worlds semantics. It is also possible to express
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicertain forms of dynamic logic.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[HasCASL] is a higher order extension of \CASL allowing
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski polymorphic datatypes and functions. It is closely related to the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski programming language Haskell and allows program constructs being
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski embedded in the specification.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskithe language is summarized in \cite{HasCASL/Summary}.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiThe latter document is also available on the CD-ROM
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[Haskell] is a modern, pure and strongly typed functional
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski programming language. It simultaneously is the implementation
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski language of \Hets, such that in the future, \Hets might be applied
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThe definitive reference for Haskell is \cite{PeytonJones03},
5277e290ad70afdf97f359019afd8fb5816f4102Till 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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder World Wide Web Consortium (W3C, \texttt{http://www.w3c.org}). It is
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski used for knowledge representation and the Semantic Web
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \cite{berners:2001:SWeb}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHets calls an external OWL DL parser
5277e290ad70afdf97f359019afd8fb5816f4102Till 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
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski the OWL ontology into the sublanguages OWL Full, OWL DL and OWL
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Hets only supports the last two, more restricted variants.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski structuring of the OWL imports is displayed as Development Graph.
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski\item[CASL-DL] is an extension of a restriction of \CASL, realizing
881ab7022a03f9a6fa697d3067d05d61844929cbChristian Maedera strongly typed variant of OWL DL in \CASL syntax.
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder \CASL with cardinality restrictions for the description of sorts and
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder unary predicates. The restrictions are based on the equivalence
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder between \CASLDL, OWL~DL and \SHOIN. Compared to \CASL only unary
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder and binary predicates, predefined datatypes and concepts (subsorts
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski of the topsort Thing) are allowed. It is used to bring OWL DL and
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder \CASL closer together.
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder\item[SPASS] \cite{WeidenbachEtAl02} is an automatic theorem prover for first-order logic
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederwith equality.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover for higher-order
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\end{description}
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederSPASS and \Isabelle are the only logics coming with a prover. Proof
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulzsupport for the other logics can be obtained by using logic translations
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowskito a prover-supported logic.
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederAn introduction to \CASL can be found in the \CASL User Manual
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder\cite{CASL-UM}; the detailed language reference is given in
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederthe \CASL Reference Manual \cite{CASL/RefManual}. These documents
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederexplain both the \CASL logic and language of basic specifications as
533d6033bec94a46d13b73cafe40953f699757c7Christian Maederwell as the logic-independent constructs for structured and
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian Maederarchitectural specifications. Corresponding documents explaining the
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maeder\HetCASL language constructs for \emph{heterogeneous} structured specifications
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulzare forthcoming, until then, \cite{Mossakowski:2003:FHS} may serve as a short
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiintroduction. Moreover, the main heterogeneous constructs will be illustrated
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiin Sect.~\ref{sec:HetSpec} below.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Getting started}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe latest \Hets version can be obtained from the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\Hets tools home page
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Since \Hets is being
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiimproved constantly, it is recommended always to use the latest version.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\Hets currently is available for Linux, Solaris and
30256573a343132354b122097b0ee1215dda1364Till 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)}
7a8592051724fa46499bde120f44cdc8db270876Till 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/}.
c57bde4abc9029546fa396c4eccacf969e126b96Mihai CodescuBut Tcl/Tk probably has been already installed
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskion your computer anyway.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiSet the environment variable \texttt{\$UNIWISH} to the wish binary
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder(which is part of Tcl/Tk), and \texttt{\$UNIDAVINCI} to the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiuDraw(Graph) binary. Furthermore, uDraw(Graph) requires that
89118fd658073a87eddf4ead4bb63c6adb30550dTill 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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiWe recommend to use the latest version (\Isabelle 2005), together
533d6033bec94a46d13b73cafe40953f699757c7Christian Maederwith Proof General, a proof interface that comes with the \Isabelle
533d6033bec94a46d13b73cafe40953f699757c7Christian Maederdistribution. Proof General uses the Eamcs or Xemacs editor.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiSet the environment variable
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\texttt{\$HETS\_ISABELLE} to the \Isabelle (or Emacs, for use with proof general) binary, and set \texttt{\$LC\_CTYPE} to \texttt{C}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiSome \Isabelle theories generated by \Hets may need to have libraries
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiavailable, see the paragraph `Libraries` below.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\subsection*{SPASS}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiFor theorem proving with SPASS, obtain SPASS freely from
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\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}.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiThe environment variable \texttt{HETS\_LIB} should be set to
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskia location where the specification libraries are stored.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%\QUERY{This should be done by the install script!}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\section{Analysis of Specifications}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiConsider the following \CASL
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskispecification:
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{BIGEXAMPLE}
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder\I\SPEC \NAMEREF{Strict\_Partial\_Order} =
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder\begin{ITEMS}[\PRED]
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu\I\SORT \( Elem \)
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski% \COMMENTENDLINE{\PRED abbreviates predicate}
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski\(\[ \FORALL x,y,z : Elem \\
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
ab5781bda9fa3062a3a92c4b57fa6bc7b70c745aTill Mossakowski \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski\begin{COMMENT}
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus LuettichNote that there may exist \(x, y\) such that\\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskineither \(x < y\) nor \(y < x\).
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski\end{BIGEXAMPLE}
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski\Hets can be used for parsing and
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederchecking static well-formedness of specifications.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \index{parsing}%
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu \index{static!analysis}%
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder \index{analysis, static}%
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederLet us assume that the example is in a file named
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu\texttt{Order.casl} (actually, this file is provided
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maederwith the \Hets distribution).
c57bde4abc9029546fa396c4eccacf969e126b96Mihai CodescuThen you can check the well-formedness of the
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maederspecification by typing (into some shell):
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz\Hets checks both the correctness of this specification
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder with respect to the \CASL syntax, as
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maederwell as its correctness with respect to the static semantics (e.g.\
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maederwhether all identifiers have been declared before they are used,
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maederwhether operators are applied to arguments of the correct sorts,
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maederwhether the use of overloaded symbols is unambiguous, and so on).
c57bde4abc9029546fa396c4eccacf969e126b96Mihai CodescuThe following flags are available in this context:
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu\begin{description}
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing -- the static analysis
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\item[\texttt{-s}, \texttt{--just-structured}]
de55550f7d117195f127481d18ec2d5e8d2317ffMihai CodescuDo the parsing and the static analysis of (heterogeneous) structured
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescuspecifications, but leave out the analysis of basic specifications.
de55550f7d117195f127481d18ec2d5e8d2317ffMihai CodescuThis can be used to quickly produce a development graph
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maedershowing the dependencies among the specifications (cf. Sect.~\ref{sec:DevGraph}).
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
c57bde4abc9029546fa396c4eccacf969e126b96Mihai CodescuUse \texttt{DIR} as the directory for specification libraries
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu(equivalently, you can set the variable \texttt{HETS\_LIB} before
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maedercalling \Hets).
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian Maeder\item[\texttt{--casl-amalg=ANALYSIS}]
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian Maeder For the analysis of architectural specification (a quite advanced
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian Maeder feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu amalgamability checking
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maeder algorithm for \CASL logic; it is a comma-separated list of zero or
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maeder more of the following options:
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maeder \begin{description}
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz \item[\texttt{sharing}] perform sharing analysis for sorts,
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz operations and predicates.
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz \item[\texttt{cell}] perform cell condition check; implies
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz \texttt{sharing}. With this option on the subsort embeddings are
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz \item[\texttt{colimit-thinness}] perform colimit thinness check;
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz implies \texttt{sharing}. The colimit thinness check is less
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski complete and usually takes longer than the full cell condition
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski check (\texttt{cell} option), but may prove more efficient in case
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski of certain specifications.
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski \end{description}
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski If \texttt{ANALYSIS} is empty then amalgamability analysis for
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \CASL is skipped.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski The default value for \texttt{--casl-amalg} is
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \texttt{cell}.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\end{description}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\section{Heterogeneous Specification} \label{sec:HetSpec}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets accepts plain text input files with the following endings:\\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{tabular}{|l|c|c|}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiEnding & default logic & structuring language\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.casl} & \CASL & \CASL \\\hline
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\texttt{.het} & \CASL & \CASL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.hs} & Haskell/HasSLe & Haskell\\\hline
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\texttt{.owl} & OWL DL, OWL Lite & OWL\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiAlthough the endings \texttt{.casl} and \texttt{.het} are
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiinterchangeable, the former should be used for libraries of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskihomogeneous \CASL specifications and the latter for \HetCASL libraries
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiof heterogeneous specifications (that use the \CASL structuring
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiconstructs). Within a \HetCASL library, the current logic can be changed e.g.\
30256573a343132354b122097b0ee1215dda1364Till Mossakowskito \HasCASL in the following way:
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{verbatim}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\end{verbatim}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe subsequent specifications are then parsed and analysed as
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\HasCASL specifications. Within such specifications,
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiit is possible to use references to named \CASL specifications;
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithese are then automatically translated along the default
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiembedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
30256573a343132354b122097b0ee1215dda1364Till Mossakowski(Heterogeneous constructs
30256573a343132354b122097b0ee1215dda1364Till Mossakowskifor explicit translations between logics will be made available
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiin the future.)
30256573a343132354b122097b0ee1215dda1364Till MossakowskiA \CspCASL specification consists of a \CASL specification
30256573a343132354b122097b0ee1215dda1364Till Mossakowskifor the data part and a \Csp process built over this data part.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiTherefore, \HetCASL provides a heterogeneous language construct
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\texttt{data} as follows:
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\begin{verbatim}
533d6033bec94a46d13b73cafe40953f699757c7Christian Maederlibrary Buffer
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder free type List[Elem] ::= nil | cons(Elem; List[Elem])
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder channel read, write : Elem
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder let Buf(l:List[Elem]) =
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder read?x -> Buf( cons(x,nil) )
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder [] if l=nil then STOP else write!last(l) -> Buf( rest(l) )
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\end{verbatim}
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederHere, the construct \texttt{data List} refers to the \CASL specification
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\texttt{List}, which is implicitly embedded into \CspCASL.
5c9181d2fd65687ced28a27cb8e161dee6d97f51Eugen KuksaThe ending \texttt{.hs} is available for directly reading in
5c9181d2fd65687ced28a27cb8e161dee6d97f51Eugen KuksaHaskell programs and HasSLe specifications,
650631bddf665ec5ef991bf4ce2f569b7709d104Christian Maederand hence supports the Haskell module system.
5c9181d2fd65687ced28a27cb8e161dee6d97f51Eugen KuksaBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
5c9181d2fd65687ced28a27cb8e161dee6d97f51Eugen Kuksathe logic Haskell has to be chosen explicitly, and the \CASL structuring
5c9181d2fd65687ced28a27cb8e161dee6d97f51Eugen Kuksasyntax needs to be used:
5c9181d2fd65687ced28a27cb8e161dee6d97f51Eugen Kuksa\begin{verbatim}
650631bddf665ec5ef991bf4ce2f569b7709d104Christian Maederlibrary Factorial
5c9181d2fd65687ced28a27cb8e161dee6d97f51Eugen Kuksalogic Haskell
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederspec Factorial =
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederfac :: Int -> Int
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederfac n = foldl (*) 1 [1..n]
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\end{verbatim}
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederNote that according to the Haskell syntax, Haskell function
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederdeclarations and definitions need to start with the first column of
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\section{Development Graphs}\label{sec:DevGraph}
17787092f1a5f5d16445e8293fd4bcde69e3fc81Mihai CodescuDevelopment graphs are a simple kernel formalism for (heterogeneous)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskistructured theorem proving and proof management. A development graph
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiconsists of a set of nodes (corresponding to whole structured
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederspecifications or parts thereof), and a set of arrows called
533d6033bec94a46d13b73cafe40953f699757c7Christian Maederdefinition links, indicating the dependency of each involved
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederstructured specification on its subparts. Arising proof obligations
533d6033bec94a46d13b73cafe40953f699757c7Christian Maederare attached as so-called theorem links to this graph.
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThe following options let \Hets show the development graph of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskia specification library:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-G}, \texttt{--only-gui}] Shows the development graph in a GUI window,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiand suppresses the writing of an output file.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\end{description}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiLet us extend the above library \texttt{Order.casl}. One use of the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilibrary might be to express the fact that the natural numbers form a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskistrict partial order as a view, as follows:
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{BIGEXAMPLE}
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\end{BIGEXAMPLE}
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\begin{EXAMPLE}
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\I\SPEC \NAMEDEFN{Natural\_Order\_2} =
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\IEXT{\NAMEREF{Natural}} \THEN
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\I\PRED \( \_\_<\_\_ : Nat \* Nat\)
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\(\[ \FORALL x,y:Nat \\
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder \. 0 < suc(x) \\
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder \. \neg x < 0 \\
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder \. suc(x) < suc(y) \IFF x < y
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\begin{EXAMPLE}%[\SLIDESMALL]
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\NAMEREF{Natural\_Order\_2} =
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\I{} \( Elem \MAPSTO Nat\)
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian MaederAgain, these specifications can be checked with \Hets. However, this
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maederonly checks syntactic and static semantic well-formedness -- it is
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskiby a strict partial ordering relation. Checking this requires theorem
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiproving, which will be discussed below.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiHowever, before coming to theorem proving, let us first inspect the
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiproof obligations arising from a specification. This can be done with:
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\texttt{hets -g Order.casl}
c488ac18796ad6383b1edf7fa2820edc8296c89eChristian Maeder(assuming that the above two specifications and the view
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichhave been added to the file
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\Hets now displays a so-called development graph
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski(which is just an overview graph showing the overall structure
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiof the specifications in the library), see Fig.~\ref{fig:dg0}.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\begin{figure}
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\begin{center}
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\includegraphics[scale=0.7]{dg-order-0}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\caption{Sample development graph.\label{fig:dg0}}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiNodes in a development graph correspond to \CASL specifications.
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiArrows show how specifications are related by the structuring
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe black arrow denotes an ordinary import of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskispecifications (generated by the extension), while the red arrow
30256573a343132354b122097b0ee1215dda1364Till Mossakowskidenotes a proof obligation (corresponding to the view).
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederThis proof obligation needs to be discharged in order to
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskishow that the view is well-formed (then its color turns into green).
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederAs a more complex example, consider the following loose specification
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederof a sorting function, taken from the \CASL User Manual
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\cite{CASL-UM}, Chap.~6:
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\begin{BIGEXAMPLE}
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\I\SPEC \NAMEREF{List\_Order\_Sorted}
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\begin{ITEMS}[\WITHIN]
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\begin{ITEMS}[\PRED]
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\I\PRED \( \_\_is\_sorted : List \)
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\(\[ \FORALL e,e': Elem; L : List \\
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder \. empty~is\_sorted \\
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder \. cons(e,empty)~is\_sorted \\
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder \. cons(e,cons(e',L))~is\_sorted \IFF
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\I\OP \( order : List \TOTAL List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following specification of sorting by insertion also is taken from
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederthe \CASL User Manual \cite{CASL-UM}, 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}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{figure}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{center}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\includegraphics[scale=0.7]{dg-order-1}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\caption{Development graph for the two sorting specifications.\label{fig:dg1}}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiIn the above-mentioned development graph, we have two types of nodes.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe named ones correspond to named specifications, but there
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiare also unnamed nodes corresponding to anonymous basic
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecifications like the declaration of the $insert$ operation in
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\NAMEREF{List\_Order} above. Basically, there is an
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiunnamed node for each structured specification that is not named.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiAgain, the black arrows denote an ordinary import of specifications
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski(corresponding to the extensions and unions in the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederspecifications), while the blue arrows denote hiding (corresponding to
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskithe local specification).
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiBy clicking on the nodes, one can inspect their signatures.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiIn this way, we can see that both \NAMEREF{List\_Order\_Sorted} and
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\NAMEREF{List\_Order} have the same signature. Hence, it
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskiis legal to add a view:
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{EXAMPLE}%[\SLIDESMALL]
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\I\VIEW \NAMEDEFN{v2}[\NAMEREF{Total\_Order}] ~:~ \NAMEREF{List\_Order\_Sorted}[\NAMEREF{Total\_Order}] \TO
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\NAMEREF{List\_Order}[\NAMEREF{Total\_Order}]
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiWe have already added this view to \texttt{Sorting.casl}.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiThe corresponding
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederproof obligation between \NAMEREF{List\_Order\_Sorted} and
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\NAMEREF{List\_Order} is displayed in Fig.~\ref{fig:dg1}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder as a red arrow.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiHere is a summary of the types of nodes and links occurring in
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederdevelopment graphs:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Named nodes] correspond to a named specification.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Unnamed nodes] correspond to an anonymous specification.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Elliptic nodes] correspond to a specification in the current library.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Rectangular nodes] are external nodes corresponding
38914aa544a92aa72e537446cfff297dc6109e04Christian Maeder to a specification downloaded from
38914aa544a92aa72e537446cfff297dc6109e04Christian Maederanother library.
38914aa544a92aa72e537446cfff297dc6109e04Christian Maeder\item[Black links] correspond to reference to other specifications
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder(definition links in the sense of \cite[IV:4]{CASL/RefManual}).
a748e6c1e72afbfa4f76e06632c05cb535bb54a0Christian Maeder\item[Blue links] correspond to hiding (hiding definition links).
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Red links] correspond to open proof obligations (theorem links).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Green links] correspond to proved proof obligations (theorem links).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Solid links] correspond to global (definition or theorem)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilinks in the sense of \cite[IV:4]{CASL/RefManual}.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Dashed links] correspond to local (definition or theorem) links in the sense of \cite[IV:4]{CASL/RefManual}.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\end{description}
a748e6c1e72afbfa4f76e06632c05cb535bb54a0Christian MaederWe now explain the menus of the development graph window.
a748e6c1e72afbfa4f76e06632c05cb535bb54a0Christian MaederMost of the pull-down menus of the window are uDraw(Graph)-specific
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskitheir function can be looked up in the uDraw(Graph) documentation.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe exception is the Edit menu. Moreover, the nodes and links
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiof the graph have attached pop-up menus, which appear when
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiclicking with the right mouse button.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Edit] This menu has two submenus:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Unnamed nodes]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe ``Hide/show names'' menu is a toggle:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiyou can switcn on or off the display of names for nodes that
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiare initially unnamed. The newly named nodes get names that
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiare derived from named neighbour nodes.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiWith the ``Hide nodes'' submenu, it is possible
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederto reduce the complexity of the graph by hiding all unnamed nodes;
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskionly nodes corresponding to named specifications remain displayed.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiPaths between named nodes going through unnamed nodes
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiare displayed as links. With the ``Show nodes'' submenu, the unnamed
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskinodes re-appear.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Proofs] This menu allows to apply some of the deduction rules
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski for development graphs, see Sect. IV:4.4 of the \CASL Reference
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Manual \cite{CASL/RefManual}. While support for local and global
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (definition or theorem) links is stable, support for hiding links
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski and checking conservativity is still experimental. In most cases, it is
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski advisable to use ``Automatic'', which automatically applies the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski rules in the correct order. As a result, the the open theorem links
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (marked in red) will be reduced to local proof goals, that is, they
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski become green, and instead, some of the node will get red, indicating
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski open local proof goals.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{description}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Pop-up menu for nodes]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederHere, the number of submenus depends on the type of the node:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Show signature] Shows the signature of the node.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Show local axioms] Shows the local axioms of the node.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Show theory] Shows the theory of the node (including axioms
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiimported from other nodes). Warning: axioms imported via hiding links
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiare not part of the theory; they can be made visible only by re-adding
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithe hidden symbols, using the proof rule \emph{Theorem-Hide-Shift}.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Translate theory] Translates the theory of a node to another logic.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederA menu with the possible translation paths will be displayed.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Show taxonomy graphs] (Only available for some logics) Shows the subsort graph of the signature of the node.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Show sublogic] Shows the logic and, within that logic, the minimal sublogic
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederfor the signature and the axioms of the node.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Show origin] Shows the kind of \CASL structuring construct that
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiled to the node.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Prove] Try to prove the local proof goals. See Section~\ref{sec:Proofs}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Show proof status] Show open and proven local proof goals.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Check consistency] Check the consistency of the theory of the node.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\item[Show just subtree] (Only for named nodes) Reduce the complexity
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiof the graph by just showing the subtree below the current node.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Undo show just subtree] (Only for named nodes) Undo the reduction.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Show referenced library] (Only for external nodes) Open a new window
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill Mossakowskishowing the development graph for the library the external node refers to.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Pop-up menu for links]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiAgain, the number of submenus depends on the type of the node:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Show morphism] Shows the signature morphism of the link. It consists
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiof two components: a logic translation and a signature morphism in the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskitarget logic of the logic translation.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiIn the (most frequent) case
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof an intra-logic signature morphism, the logic translation component is
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskijust the identity.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Show origin] Shows the kind of \CASL structuring construct that
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiled to the link.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Show proof status] (Only for theorem links) Show the proof status.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Check conservativity] (Experimental) Check whether the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskitheory of the target node of the link
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiis a conservative extension of the theory of the source node.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Reading, Writing and Formatting}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets provides several options controlling the types of files
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithat are read and written.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-i ITYPE}, \texttt{--input-type=ITYPE}] Specify
5277e290ad70afdf97f359019afd8fb5816f4102Till 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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederin abstract syntax trees in ATerm format, while \texttt{ast.baf}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskireads in the compressed ATerm format.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiThe possible input types are:
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{verbatim}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski (casl|het|owl|hs|ast[.baf]|[tree.]gen_trm[.baf])
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\end{verbatim}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[\texttt{-O DIR}, \texttt{--output-dir=DIR}]
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiSpecify \texttt{DIR} as destination directory for output files.
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[\texttt{-o OTYPES}, \texttt{--output-types=OTYPES}]
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\texttt{OTYPES} is a comma separated list of output types:
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{verbatim}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski | pp.(het|tex|html)
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski | graph.(dot|ps|davinci)
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski | ast.(het|trm|taf|html|xml)
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski | (fdg|hdg|dg)[.nax].(het|trm|taf|html|xml)
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\end{verbatim}
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiThe default is \texttt{dg.taf}, which means that the development
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedergraph of the library is stored in textual ATerm format (\texttt{taf}).
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiThis format can be read in when a library is downloaded from
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskianother library, avoiding the need to re-analyse the downloaded library.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiThe \texttt{pp} format is for pretty printing, either as plain text
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski(\texttt{het}), \LaTeX input (\texttt{tex}) or HTML (\texttt{html}).
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiA formatter with pretty-printed output currently is available only for
38914aa544a92aa72e537446cfff297dc6109e04Christian Maederthe \CASL logic. For example, it is possible to generate a pretty
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiprinted \LaTeX\ version of \texttt{Order.casl} by typing:
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiThis will generate a file \texttt{Order.pp.tex}. It can be included
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiinto \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskicoming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty)}) is used.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiWhen the \texttt{thy} format is selected, \Hets will try to translate
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskieach specification in the library to \Isabelle, and write one \Isabelle
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\texttt{.thy} file per specification.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiWhen the \texttt{comptable.xml} format is selected, \Hets will extract
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithe composition and inverse table of a Tarskian relation algebra from
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskispecification(s) (selected with the \texttt{-n} or \texttt{--spec}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskioption). It is assumed that the relation algebra is
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskigenerated by basic relations, and that the specification is written
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederin the \CASL logic. A sample specification of a relation
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskialgebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiavailable from \texttt{www.cofi.info/Libraries}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe output format is XML, the URL of the DTD is included in the
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[\texttt{-t TRANS}, \texttt{--translation=TRANS}]
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederchooses a translation option. \texttt{TRANS} is a colon-separated list
d3e4f883d74b0cd6b1708141fddc20e895e82eb1Eugen Kuksawithout blanks of one or more from:
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederCASL2HasCASL,\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiCASL2SubCFOL,\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiCFOL2IsabelleHOL,
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCoCASL2CoPCFOL,\\
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCoCFOL2IsabelleHOL,
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCoPCFOL2CoCFOL,
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCspCASL2IsabelleHOL,\\
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCspCASL2Modal,
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHasCASL2HasCASL,
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHasCASL2Haskell,\\
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHasCASL2IsabelleHOL,
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHaskell2IsabelleHOLCF,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-r RAW} or \texttt{--raw=RAW}] This option allows one
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederto influence the formatting in more detail.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHere, \texttt{RAW} is \texttt{(ascii|text|(la)?tex)=STRING},
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand \texttt{STRING} is passed to the appropriate pretty-printer.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe deatils of these options are to be fixed in the future only.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe other output formats are for future usage.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Miscellaneous Options}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-v[Int]}, \texttt{--verbose[=Int]}]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiSet the verbosity level according to \texttt{Int}. Default is 1.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-q}, \texttt{--quiet}]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBe quiet -- no diagnostic output at all. Overrides -v.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-V}, \texttt{--version}] Print version number and exit.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-h}, \texttt{--help}, \texttt{--usage}]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiPrint usage information and exit.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[\texttt{+RTS -KIntM -RTS}] Increase the stack size to
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \texttt{Int} megabytes (needed in case of a stack overflow).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThis must be the first option.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-l LOGIC}, \texttt{--logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidecelation. The default is \CASL.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-n SPECS}, \texttt{--spec=SPECS}]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskichooses a list of named specifications for processing
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Proofs with \Hets}\label{sec:Proofs}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe graphical user interface (GUI) for calling a prover
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis shown in Fig. \ref{fig:proof_window}. The list on the right
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskishows all goal names prefixed with the proof status in square
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskibrackets. A proved goal is indicated by a '+', a '-' indicates a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidisproved goal and a space denotes an open goal.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\includegraphics[width=\textwidth]{proofmanagement1}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Hets Goal and Prover Interface\label{fig:proof_window}}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIf you open this GUI processing the goals of one node for the first
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitime, it will show all goals as open. Within this list you can select
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithose goals that should be inspected or proved. The button 'Display'
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowskishows the selected goals in the ASCII syntax of this theory's logic in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskia separate window. With the 'Prove' button the actual prover is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilaunched. This is described in more detail in the following
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiparagraphs. By pressing the 'Show Proof Details' button a window is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiopened where for each proved goal the used axioms are shown. The
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski'Status:' shows either 'No prover running' or 'Waiting for prover' in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiblack or blue. If you press the 'Close' button the window is closed
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand the status of the goals' list is integrated into the
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDevelopmentGraph. If all goals have been proved, the selected node
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiturns from red into green.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe list 'Pick Theorem Prover:' lets you choose one of the connected
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiprovers (currently, these are SPASS and \Isabelle, described below). By
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskipressing 'Prove' the selected prover is launched and the theory along
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwith the selected goals is translated via the shortest possible path
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof comorphims into the provers logic. The button 'More fine grained
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiselection...' lets you pick a (composed) comorphism in a separate
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwindow from where the prover is launched then.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection*{SPASS}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\includegraphics[width=\textwidth]{spassGUI1}
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski\caption{Interface of the SPASS prover\label{fig:SPASS_GUI}}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe automatic theorem prover SPASS
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{WeidenbachEtAl02} is a resultion-based prover for first-order logic
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederwith equality.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIf you have choosen SPASS, initially, all selected goals are tried in a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirow. After this so called batch mode the results are displayed in a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwindow which is shown in Fig. \ref{fig:SPASS_GUI}. This GUI for the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitheorem prover SPASS is very similiar to the 'Select Goal(s) and
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiProve' GUI which lets you choose a prover for some goals. But with the
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiSPASS GUI, the actual SPASS prover is launched with the selected
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskigoal. Further it is possible to set a time-limt and some options for
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiSPASS. The available options are shown in separate window by pressing
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe 'Help' button. The status of the selected goal is shown in the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski'Status:' line with either 'Proved', 'Disproved', 'Open' or 'Open Time
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(Time is up!)'. If a goal has been proved the labels of the used
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiaxioms are shown in the list on the right. The button 'Show Details'
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskishows the whole output of SPASS. 'Save Prover Configuration allows you
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito save the configuation and status of each proof for
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidocumentation. By pressing the button 'Exit Prover' the status of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithese proofs and goals is transferred back to the main 'Select Goal(s)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand Prove' window.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection*{Isabelle}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Isabelle \cite{NipPauWen02} is an interactive theorem prover, which is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimore powerful than SPASS, but also requires more user interaction.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskihas a very small core guaranteeing correctness, and its provers,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilike the simplifier or the tableaux prover, are built on top of this
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicore. Furthermore, there is over fifteen years of experience with it,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand several mathematical textbooks have been partially
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{formal!verification}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Isabelle is a tactic based theorem prover implemented in standard ML.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe main \Isabelle logic (called Pure) is some weak intuitionistic type
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitheory with polymorphism. The logic Pure is used to represent a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskivariety of logics within \Isabelle; one of them being \HOL (higher-order
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogic). For example, logical implication in Pure (written
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{==>}, also called meta-implication), is different from logical
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiimplication in \HOL (written \texttt{-->}, also called object
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIt is essential to be aware of the fact that the \Isabelle/\HOL logic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis different from the logics that are encoded into it via comorphisms.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederTherefore, the formulas appearing in subgoals of proofs with \Isabelle
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwill not conform to the syntax of the original input logic. They may
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskieven use features of \Isabelle/\HOL such as higher-order functions
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithat are not present in an input logic like \CASL.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Isabelle is started with ProofGeneral
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\cite{DBLP:conf/tacas/Aspinall00,url:ProofGeneral} in a separate Emacs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{url:Emacs,url:XEmacs}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe \Isabelle theory file conforms to the Isabelle/Isar syntax
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{NipPauWen02}. It starts with the theory (encoded along the selected
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski comorphism), followed by a list of theorems. Initially, all the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski theorems have trivial proofs, using the `oops` command. However, if
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski you have saved earlier proof attempts, \Hets will patch these into
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski the generated \Isabelle theory file, ensuring that your previous work
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski is not lost. (But note that this patching can only be successful
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder if you do not rename specifications, or change their structure.) You
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski now can replace the 'oops' commands with real \Isabelle proofs, and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski use Proof General to step through the proofs. You finish your session
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski by saving your file (using the Emacs file menu, or the Ctrl-x Ctrl-s
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski key sequence), and pressing a button in a small pop-up window
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski generated by \Hets.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\section{Limits of \Hets}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Hets is still intensively under development. In particular, the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifollowing points are still missing:
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{itemize}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item There is no proof support for architectural specifications.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item Distributed libraries are always downloaded from the local disk,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskinot from the Internet.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item Version numbers of libraries are not considered properly.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item The proof engine for development graphs provides only experimental
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maedersupport for hiding links and for conservativity.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\section{Architecture of \Hets}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\Hets is written in Haskell. Its parser uses combinator
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \index{parsing}%
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederThe user-defined (also known as ``mixfix'') syntax of \CASL
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maedercalls for a two-pass approach. In the first pass, the skeleton of a
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\CASL abstract syntax tree is derived, in order to extract user-defined
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maedersyntax rules. In a second pass, which is performed during
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederanalysis, these syntax rules are used to parse
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiany expressions that
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederuse mixfix notation. The output is stored in the so-called
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder \index{ATerms}%
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederATerm format \cite{BJKO00}, which is used as interchange format
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederfor interfacing with other tools.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\Hets provides an abstract interface for
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder \index{institution!independence}%
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \index{independence, institution}%
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinstitutions, so
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithat new logics can be integrated smoothly.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiIn order to do so, a parser,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskia static checker and a prover for basic specifications in the logic have
30256573a343132354b122097b0ee1215dda1364Till Mossakowskito be provided.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{figure}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder%\includegraphics[scale=0.5]{hets}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\caption{Architecture of the heterogeneous tool set.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\label{fig:hets}}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuThe architecture of \Hets is shown in Fig.~\ref{fig:hets}.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederIf your favourite logic is missing in \Hets, please tell us
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu(hets@tzi.de). We will take account your feedback when deciding which
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codesculogics and proof tools to integrate next into \Hets. Help with
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuintegration of more logics and proof tools into \Hets is also welcome.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\Hets is mainly maintained by
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian MaederChristian Maeder (maeder@tzi.de) and Till Mossakowski
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu(till@tzi.de). The mailing list is \url{hets@tzi.de},
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuthe homepage is
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\url{http://www.informatik.uni-bremen.de/mailman/listinfo/hets-devel}.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\paragraph{Acknowledgement}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuThe heterogeneous tool set \Hets, which shows that the theory outlined
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuin this work can also be brought to practice, would not have possible
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuwithout cooperation with Christian Maeder and Klaus L\"uttich.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederBesides the author, the following people have been involved
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuin the implementation of \Hets:
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuKatja Abu-Dib,
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuCarsten Fischer,
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuJorina Freya Gerken,
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuSonja Gr\"{o}ning,
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian MaederWiebke Herding,
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuAnton Kirilov,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederTina Krausser,
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuMartin K\"{u}hl,
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuKlaus L\"{u}ttich,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederChristian Maeder,
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuMaciek Makowski,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederRazvan Pascanu,
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuDaniel Pratsch,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederFelix Reckers,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederMarkus Roggenbach,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederPascal Schmidt and
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuPaolo Torrini.
6135dff41a8cf187b8821aab7def02f624f8e856Christian Maeder\Hets has been built based on experiences with its
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu \index{Cats@\Cats}%
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \index{Maya@\MAYA}%
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe \CASL Tool Set (\Cats)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\cite{Mossakowski:2000:CST,Mossakowski:1998:SSA}
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiprovides parsing and static analysis for \CASL.
af35cfab2b45879b385a8ec31558f7ebb1b3dc5fChristian MaederIt has been developed by the present author with help
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiof Mark van den Brand, Kolyang, Bartek Klin, Pascal Schmidt and
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian MaederFrederic Voisin.
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\MAYA \cite{Autexier:2002:IHD,AutexierEtal02} is a proof management
e683cd5ffcfa43e18a9b3eb7c7aeec32dab50c06Mihai Codescutool based on development graphs. \MAYA only supports development
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedergraphs without hiding and without logic translations. \MAYA has been
e683cd5ffcfa43e18a9b3eb7c7aeec32dab50c06Mihai Codescudeveloped by Serge Autexier and Dieter Hutter.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuI also want to thank Agn\`es Arnould, Thibaud Brunet, Pascale LeGall,
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuKathrin Hoffmann, Katiane Lopes, Klaus L\"uttich, Christian Maeder,
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian MaederStefan Merz, Maria Martins Moreira, Christophe
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian MaederRingeissen, Markus Roggenbach, Dmitri Schamschurko, Lutz Schr\"oder,
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian MaederKonstantin Tchekine and Stefan W\"olfl
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescufor giving feedback about \Cats, HOL-CASL and \Hets. Finally,
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuspecial thanks to Christoph L\"uth and George Russell
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederfor help with connecting \Hets to their UniForM workbench.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\bibliographystyle{plain}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\bibliography{cofibib,cofi-ann,UM,hets,kl}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\end{document}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu%%% Local Variables:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%%% mode: latex
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder%%% TeX-master: "UserGuide"