UserGuide.tex revision 3e0309de8bbb1588c0f976d6ce3f1e615d17da84
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\documentclass{article}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage[show]{ed} % set to hide for producing a released version
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{alltt}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{casl}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{color}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{url}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{threeparttable,hhline}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage[pdfborder=0 0 0,bookmarks,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskipdfauthor={Till Mossakowski, Christian Maeder, Mihai Codescu},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskipdftitle={Hets User Guide}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{hyperref} %% do not load more packages after this line!!
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}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newenvironment{DETAILSFORMAT} {}{}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newenvironment{META}[1][] {#1\begin{METAFORMAT}}{\end{METAFORMAT}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newenvironment{METAFORMAT} {\medskip\vrule\hspace{1ex}\vrule\hspace{1ex}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \begin{minipage}{0.9\textwidth}\it}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski {\end{minipage}\par\medskip}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SLIDESMALL} {}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SLIDESONLY}[1] {}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\newcommand {\CoFI}{CoFI\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\largeELAN} {\largeTEXTSC{E}{LAN}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand {\HOL}{\normalTEXTSC{H}{OL}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till 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 {\SPASS}{\normalTEXTSC{S}{PASS}\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\newcommand{\SROIQ}{$\mathcal{SROIQ}$(\textbf{D})\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\DL}{DL\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till 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}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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}
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill 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)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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}
881ab7022a03f9a6fa697d3067d05d61844929cbChristian Maeder\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}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\title{{\bf \protect{\LARGEHets} User Guide}\\
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski-- Version 0.95 --}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\author{Till Mossakowski, Christian Maeder,
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski Mihai Codescu, Dominik L\"{u}cke\\[1em]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDFKI Lab Bremen, Bremen, Germany.\\[1em]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiComments to: hets-users@informatik.uni-bremen.de \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski(the latter needs subscription to the mailing list)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Introduction}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe central idea of the Heterogeneous Tool Set (\protect\Hets) is to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiprovide a general framework for formal methods integration and proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimanagement. One can think of \Hets acting like a motherboard where
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidifferent expansion cards can be plugged in, the expansion cards here
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskibeing individual logics (with their analysis and proof tools) as well
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskias logic translations. Individual logics and their analysis and proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitools can be plugged into the \Hets motherboard using an
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiobject-oriented interface based on institutions
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\cite{GoguenBurstall92}. The \Hets motherboard already has plugged in
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskia number of expansion cards (e.g., the theorem provers Isabelle, SPASS
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand more, as well as model finders). Hence, a variety of tools is
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiavailable, without the need to hard-wire each tool to the logic at
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{figure}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{center}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \includegraphics[width=0.45\textwidth]{hets-motherboard}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{The \Hets motherboard and some expansion cards}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets supports a number of input languages directly, such as \CASL,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiCommon Logic, OWL-DL, Haskell, and Maude. For heterogeneous
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecification, \Hets offers language heterogeneous \CASL.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHeterogeneous \CASL (\HetCASL) generalises the structuring
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CASL \cite{CASL-UM,CASL/RefManual} to arbitrary logics
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski(if they are formalised as institutions and plugged into
881ab7022a03f9a6fa697d3067d05d61844929cbChristian Maederthe \Hets motherboard), as well as to heterogeneous
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicombination of specification written in different logics.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiFig.~\ref{fig:lang} for a simple subset of the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\HetCASL syntax, where \emph{basic specifications} are unstructured
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskispecifications or modules written in a specific logic. The graph of
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicurrently supported logics and logic translations (the latter are also
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicalled comorphisms) is shown in Fig.~\ref{fig:LogicGraph}, and the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidegree of support by \Hets in Fig.~\ref{fig:Languages}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{figure}[ht]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiSPEC ::= BASIC-SPEC
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski | SPEC then SPEC
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski | SPEC then %implies SPEC
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski | SPEC with SYMBOL-MAP
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski | SPEC with logic ID
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiDEFINITION ::= logic ID
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski | spec ID = SPEC end
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski | view ID : SPEC to SPEC = SYMBOL-MAP end
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski | view ID : SPEC to SPEC = with logic ID end
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiLIBRARY = DEFINITION*
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\end{verbatim}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\caption{Syntax of a simple subset of the heterogeneous
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskispecification language.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\texttt{BASIC-SPEC} and \texttt{SYMBOL-MAP} have a logic
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskispecific syntax, while \texttt{ID} stands for some form of
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiidentifiers.\label{fig:lang}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiWith \emph{heterogeneous structured specifications}, it is possible to
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicombine and rename specifications, hide parts thereof, and also
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskitranslate them to other logics. \emph{Architectural specifications}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiprescribe the structure of implementations. \emph{Specification
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski libraries} are collections of named structured and architectural
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskispecifications.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\Hets consists of logic-specific tools for the parsing and static
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskianalysis of the different involved logics, as well as a
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskilogic-independent parsing and static analysis tool for structured and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiarchitectural specifications and libraries. The latter of course needs
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskito call the logic-specific tools whenever a basic specification is
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\Hets is based on the theory of institutions \cite{GoguenBurstall92},
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiwhich formalize the notion of a logic. The theory behind \Hets is laid
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiout in \cite{Habil}. A short overview of \Hets is given in
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\cite{MossakowskiEA06,MossakowskiEtAl07b}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\section{Logics supported by Hets}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe following list of logics (formalized as so-called institutions
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\cite{GoguenBurstall92}) is currently supported by \Hets:
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till 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 with green, the more stable is the implementation of the logic. Blue indicates a prover-supported logic.}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\label{fig:LogicGraph}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{figure}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{center}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{tabular}{|l|c|c|c|}\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiLanguage & Parser & Static Analysis & Prover \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CASL & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CoCASL & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\ModalCASL & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\HasCASL & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiHaskell & (x) & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CspCASL & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CspCASL\_Trace & - & - & x \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CspCASL\_Failure & - & - & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiConstraint\CASL & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiTemporal & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiRelScheme & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiDFOL & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiExtModal & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiLF & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Structured specifications & x & x & (x) \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Architectural specifications & x & x & -\\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CASLDL & x & - & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiDMU & x & - & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiOWL DL & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiPropositional & x & x & x \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiSoftFOL & x & - & x \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiMaude & x & x & - \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiVSE & x & x & x \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Isabelle & (x) & - & x \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\caption{Current degree of \Hets support for the different languages.\label{fig:Languages}}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[CASL] extends many sorted first-order logic with partial
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski functions and subsorting. It also provides induction sentences,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski expressing the (free) generation of datatypes.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%It is mainly designed and used for the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%specification of requirements for software systems. But it is also
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%used for the specification of \Dolce (Descriptive Ontology for
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Linguistic and Cognitive Engineering), an Upper Ontology for knowledge
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski%representation. \cite{Gangemi:2002:SOD} Further it is now used to
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%specify calculi for time and space.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiFor more details on \CASL see \cite{CASL/RefManual,CASL-UM}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWe have implemented the \CASL logic in such a way that much of the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiimplementation can be re-used for \CASL extensions as well; this
5277e290ad70afdf97f359019afd8fb5816f4102Till 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 systems.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe central proof method is coinduction.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[ModalCASL] \cite{ModalCASL}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski 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
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski polymorphic datatypes and functions. It is closely related to the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski programming language Haskell and allows program constructs being
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski embedded in the specification.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
7e7c1b5990145d02f8abb7c74d3c0d609735b54cTill Mossakowskithe language is summarized in \cite{HasCASL/Summary}, the semantics
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiin \cite{Schroder05b,Schroder-habil}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[Haskell] is a modern, pure and strongly typed functional
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski programming language. It simultaneously is the implementation
a8ce558d09f304be325dc89458c9504d3ff7fe80Till 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{Roggenbach06} is a combination of \CASL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski with the process algebra CSP.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[ConstraintCASL] is an experimental logic for the specification
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiof qualitative constraint calculi.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[OWL DL] is the Web Ontology Language (OWL) recommended by the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski World Wide Web Consortium (W3C, \url{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
5277e290ad70afdf97f359019afd8fb5816f4102Till 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
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Hets only supports the last two, more restricted variants.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski structuring of the OWL imports is displayed as Development Graph.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[CASL-DL] \cite{OWL-CASL-WADT2004}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiis 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
a8ce558d09f304be325dc89458c9504d3ff7fe80Till 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
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski of the topsort Thing) are allowed. It is used to bring OWL DL and
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \CASL closer together.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\item[Propositional] is classical propositional logic, with
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskithe zChaff SAT solver \cite{Herbstritt03} connected to it.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[SoftFOL] \cite{LuettichEA06a} offers three automated theorem
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski proving (ATP) systems for first-order logic with equality: (1) \SPASS
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \cite{WeidenbachEtAl02}; (2) Vampire \cite{RiazanovV02}; and (3)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski MathServe Broker\footnote{which chooses an appropriate ATP upon a
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski classification of the FOL problem} \cite{ZimmerAutexier06}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski These together comprise some of the most advanced theorem provers
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski for first-order logic.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski for higher-order logic.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\ednote{TODO Till: update list}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiVarious logics are supported with proof tools. Proof support for the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiother logics can be obtained by using logic translations to a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiprover-supported logic.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAn introduction to \CASL can be found in the \CASL User Manual
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{CASL-UM}; the detailed language reference is given in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe \CASL Reference Manual \cite{CASL/RefManual}. These documents
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiexplain both the \CASL logic and language of basic specifications as
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwell as the logic-independent constructs for structured and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiarchitectural specifications. The corresponding document explaining the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\HetCASL language constructs for \emph{heterogeneous} structured specifications
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis the \HetCASL language summary \cite{Mossakowski04}; a formal
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisemantics as well as a user manual with more examples are in preparation.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiSome of \HetCASL's heterogeneous constructs will be illustrated
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiin Sect.~\ref{sec:HetSpec} below.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Logic translations supported
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{comorphisms}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiLogic translations (formalized as institution comorphisms
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\cite{GoguenRosu02}) translate from a given source logic to a given
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskitarget logic. More precisely, one and the same logic translation
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimay have several source and target \emph{sub}logics: for
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskieach source sublogic, the corresponding sublogic of the target
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogic is indicated.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiA graph of the most important logics and sublogics, together with their
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicomorphisms, is shown in Fig.~\ref{fig:SublogicGraph}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \begin{center}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \includegraphics[scale=0.4]{SublogicGraph}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Graph of most important sublogics currently supported by \Hets,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitogether with their comorphisms.}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\label{fig:SublogicGraph}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiIn more detail, the following list of logic translations is currently
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisupported by \Hets:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\ednote{TODO Mihai,Till: check VSE, Maude, DFOL descr. or ref.}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{tabular}{|l|p{8cm}|}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiCASL2CoCASL & inclusion \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiCASL2CspCASL & inclusion \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiCASL2HasCASL & inclusion \\\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiCASL2Isabelle & inclusion on sublogic CFOL=
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski(translation $(7)$ of \cite{Mossakowski02}) \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiCASL2Modal & inclusion \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiCASL2PCFOL & coding of subsorting (SubPCFOL=) by injections, see Chap.\ III:3.1 of the CASL Reference Manual \cite{CASL/RefManual} \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiCASL2PCFOLTopSort & coding of subsorting (SulPeCFOL=) by a top sort and unary
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskipredicates for the subsorts \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiCASL2Propositional & translation of propositional FOL \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiCASL2SoftFOL & coding of CASL.SuleCFOL=E to SoftFOL \cite{LuettichEA06a},
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskimapping types to soft types \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiCASL2SoftFOLInduction & same as CASL2SoftFOL but with instances of induction
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskiaxioms for all proof goals \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiCASL2SubCFOL & coding of partial functions by error elements
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski(translation $(4a')$ of \cite{Mossakowski02}, but extended to subsorting, i.e. sublogic SubPCFOL=) \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiCASL2VSE & inclusion on sublogic CFOL= \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiCASL2VSEImport & inclusion on sublogic CFOL= \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiCASL2VSERefine & refining translation of CASL.CFOL= to VSE \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiCASL\_DL2CASL & inclusion \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiCoCASL2CoPCFOL & coding of subsorting by injections, similar to CASL2PCFOL \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiCoCASL2CoSubCFOL & coding of partial functions by error supersorts, similar to CASL2SubCFOL \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiCoCASL2Isabelle & extended translation similar to CASL2Isabelle \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiCspCASL2CspCASL\_Failure & inclusion \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiCspCASL2CspCASL\_Trace & inclusion \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiCspCASL2Modal & translating the CASL data part to ModalCASL \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiDFOL2CASL & translating dependent types \\\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDMU2OWL & interpreting Catia output as OWL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{tabular}{|l|p{7cm}|}\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHasCASL2HasCASLNoSubtypes & coding out subtypes \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHasCASL2HasCASLPrograms & coding of \HasCASL axiomatic recursive definitions
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskias \HasCASL recursive program definitions \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHasCASL2Haskell & translation of \HasCASL recursive program definitions to Haskell \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHasCASL2IsabelleOption & coding of HasCASL to Isabelle/HOL \cite{Groening05} \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHaskell2Isabelle & coding of Haskell to Isabelle/HOL \cite{TorriniEtAl07} \\\hline
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill MossakowskiHaskell2IsabelleHOLCF & coding of Haskell to Isabelle/HOLCF \cite{TorriniEtAl07} \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiMaude2CASL & inclusion \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiModal2CASL & the standard translation of modal logic
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskito first-order logic \cite{blackburn_p-etal:2001a} \\\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiOWL2CASL & inclusion \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiPropositional2CASL & inclusion \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiRelScheme2CASL & inclusion \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Getting started}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe latest \Hets version can be obtained from the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets tools home page
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Since \Hets is being
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiimproved constantly, it is recommended always to use the latest version.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets currently is available (on Intel architectures only) for Linux, Solaris
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThere are three possibilities to install \Hets:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{enumerate}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiThe Java-based \Hets installer. Download a \texttt{.jar} file and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskijava -jar \texttt{file.jar}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiNote that you need Sun Java 1.4.2 or later. On a Mac, you can just
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidouble-click on the \texttt{.jar} file.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe installer will lead you through the installation with
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskia graphical interface. It will download and install further
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisoftware (if not already installed on your computer):
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{tabular}{|l|l|p{5cm}|}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHets-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiuDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiTcl/Tk & graphics widget system & (version 8.4 or 8.5 must be installed before)\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\SPASS & theorem prover & \url{http://spass.mpi-sb.mpg.de/}\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiDarwin & theorem prover & should be installed manually from \url{http://combination.cs.uiowa.edu/Darwin/}\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski(X)Emacs & editor (for Isabelle) & (must be installed manually)\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiIf you do not have Sun Java, you can just download the hets binary.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiYou have to unpack it with \texttt{bunzip2} and then put it at
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisome place coverd by your \texttt{PATH}. You also have to
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskiinstall the above mentioned software and set
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiseveral environment variables, as explained on the installation page.
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill MossakowskiYou may compile \Hets from the sources, please follow the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilink ``Hets: source code and information for developers''
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskion the \Hets web page, download the sources (as tarball or from
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisvn), and follow the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinstructions in the \texttt{INSTALL} file, but be prepared to take some time.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{enumerate}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiDepending on your application further tools are supported and may be
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinstalled in addition:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{tabular}{|l|l|p{5cm}|}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskizChaff & SAT solver & \url{http://www.princeton.edu/~chaff/zchaff.html} \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiminisat & SAT solver & \url{http://minisat.se/} \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiPellet & OWL reasoner & \url{http://clarkparsia.com/pellet/} \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiE-KRHyper & theorem prover
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & \url{http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/} \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiReduce & computer algebra system
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & \url{http://www.reduce-algebra.com/} \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMaude & rewrite system & \url{http://maude.cs.uiuc.edu/} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiVSE & theorem prover & (non-public) \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTwelf & & \url{http://twelf.plparty.org/} \\\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\ednote{TODO Mihai, Till, Luecke: check prover list}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\section{Analysis of Specifications}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiConsider the following \CASL
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecification:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{BIGEXAMPLE}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\I\SPEC \NAME{Strict\_Partial\_Order} =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{ITEMS}[\PRED]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\I\SORT \( Elem \)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski% \COMMENTENDLINE{\PRED abbreviates predicate}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL x,y,z : Elem \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{COMMENT}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiNote that there may exist \(x, y\) such that\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskineither \(x < y\) nor \(y < x\).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets can be used for parsing and
5277e290ad70afdf97f359019afd8fb5816f4102Till 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
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{Order.casl} (actually, this file is provided
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwith the \Hets distribution as \texttt{Hets-lib/UserManual/Chapter3.casl}).
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).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following flags are available in this context:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski -- the static analysis is skipped and no development is created.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-s}, \texttt{--just-structured}] Do the parsing and the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski static analysis of (heterogeneous) structured specifications, but
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski leave out the analysis of basic specifications. This can be used
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski for prototyping issues, namely to quickly produce a development graph
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski showing the dependencies among the specifications (cf.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Sect.~\ref{sec:DevGraph}) even if the individual specifications are
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski not correct yet.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiUse \texttt{DIR} as a colon separated list of directories for specification libraries (equivalently, you can set the variable \texttt{HETS\_LIB} before
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicalling \Hets).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-a ANALYSIS}, \texttt{--casl-amalg=ANALYSIS}]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski For the analysis of architectural specification (a quite advanced
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski amalgamability checking
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski algorithm for \CASL logic; it is a comma-separated list of zero or
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski more of the following options:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \item[\texttt{sharing}] perform sharing analysis for sorts,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski operations and predicates.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \item[\texttt{cell}] perform cell condition check; implies
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \texttt{sharing}. With this option on, the subsort embeddings are
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \item[\texttt{colimit-thinness}] perform colimit thinness check;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski implies \texttt{sharing}. The colimit thinness check is less
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski complete and usually takes longer than the full cell condition
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski check (\texttt{cell} option), but may prove more efficient in case
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski of certain specifications.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski If \texttt{ANALYSIS} is empty then amalgamability analysis for
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \CASL is skipped.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski The default value for \texttt{--casl-amalg} is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \texttt{cell}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\section{Heterogeneous Specification} \label{sec:HetSpec}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets accepts plain text input files with the following endings:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{tabular}{|l|c|c|}\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiEnding & default logic & structuring language\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.casl} & \CASL & \CASL \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.het} & \CASL & \CASL \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.hs} & Haskell & Haskell\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.owl} & OWL DL, OWL Lite & OWL\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.elf} & LF & Twelf \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.maude} & Maude & Maude \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFurthermore, \texttt{.xml} files are accepted as Catia output if the default
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogic is set to DMU before a library import or by the ``\texttt{-l DMU}''
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicommand line option of \Hets.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAlthough the endings \texttt{.casl} and \texttt{.het} are
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinterchangeable, the former should be used for libraries of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskihomogeneous \CASL specifications and the latter for \HetCASL libraries
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof heterogeneous specifications (that use the \CASL structuring
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiconstructs). Within a \HetCASL library, the current logic can be changed e.g.\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskito \HasCASL in the following way:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe subsequent specifications are then parsed and analysed as
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\HasCASL specifications. Within such specifications,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiit is possible to use references to named \CASL specifications;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithese are then automatically translated along the default
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiembedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(There are also heterogeneous constructs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor explicit translations between logics, see \cite{Mossakowski04}.)
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiA \CspCASL specification consists of a \CASL specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor the data part and a \Csp process built over this data part.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTherefore, \HetCASL provides a heterogeneous language construct
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{data} as follows:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilibrary Buffer
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski free type List[Elem] ::= nil | cons(Elem; List[Elem])
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ops last: List -> ? Elem;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski rest: List -> ? List
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski channel read, write : Elem
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski process Buf(List): read, write, List;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski EmptyBuffer : read,write, List;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Buf(l)= read? x :: Elem -> Buf(cons(x,nil)) []
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (if l=nil then STOP else
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski write!last(l) -> Buf(rest(l)))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski EmptyBuffer = Buf(nil)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHere, the construct \texttt{data List} refers to the \CASL specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{List}, which is implicitly embedded into \CspCASL.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe ending \texttt{.hs} is available for directly reading in
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHaskell programs % and HasSLe specifications,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiand hence supports the Haskell module system.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithe logic Haskell has to be chosen explicitly, and the \CASL structuring
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisyntax needs to be used:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilibrary Factorial
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispec Factorial =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifac :: Int -> Int
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifac n = foldl (*) 1 [1..n]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiNote that according to the Haskell syntax, Haskell function
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskideclarations and definitions need to start with the first column of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\section{Development Graphs}\label{sec:DevGraph}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDevelopment graphs are a simple kernel formalism for (heterogeneous)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskistructured theorem proving and proof management.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiA development graph consists of a set of nodes (corresponding to whole
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskistructured specifications or parts thereof), and a set of arrows
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicalled \emph{definition links}, indicating the dependency of each
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinvolved structured specification on its subparts. Each node is
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiassociated with a signature and some set of local axioms. The axioms
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof other nodes are inherited via definition links. Definition links
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiare usually drawn as black solid arrows, denoting an import of another
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecification.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiComplementary to definition links, which \emph{define} the theories of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskirelated nodes, \emph{theorem links} serve for \emph{postulating}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskirelations between different theories. Theorem links are the central
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidata structure to represent proof obligations arising in formal
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiTheorem links can be \emph{global} (drawn as solid arrows) or
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\emph{local} (drawn as dashed arrows): a global theorem link
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskipostulates that all axioms of the source node (including the inherited
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiones) hold in the target node, while a local theorem link only postulates
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithat the local axioms of the source node hold in the target node.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiBoth definition and theorem links can be \emph{homogeneous},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskii.e. stay within the same logic, or \emph{heterogeneous}, i.e.\ %% such that
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithe logic changes along the arrow. Technically, this is the case
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifor Grothendieck signature morphisms $(\rho,\sigma)$ where
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski$\rho\not=id$. This case is indicated with double arrows.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiTheorem links are initially displayed in red.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe \emph{proof
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski calculus} for development graphs
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\cite{MossakowskiEtAl05,Habil} is given by rules
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithat allow for proving global theorem links by decomposing them
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiinto simpler (local and global) ones. Theorem links that have been
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiproved with this calculus are drawn in green. Local theorem links can
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskibe proved by turning them into \emph{local proof goals}. The latter
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskican be discharged using a logic-specific calculus as given by an
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskientailment system for a specific institution. Open local
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiproof goals are indicated by marking the corresponding node in the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidevelopment graph as red; if all local implications are proved, the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskinode is turned into green. This implementation ultimately is based
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskion a theorem \cite{Habil} stating soundness and relative completeness
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiof the proof calculus for heterogeneous development graphs.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiand in \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe following options let \Hets show the development graph of
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskia specification library:
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{description}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-u}, \texttt{--uncolored}] no colors in shown graphs
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe following additional options also apply typical rules from the development
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskigraph calculus to the final graph and save applying these rule via the GUI.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-A}, \texttt{--apply-automatic-rule}] apply the automatic
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski strategy to the development graph. This is what you usual want in order to
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski get goals within nodes for proving.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-N}, \texttt{--normal-form}] compute all normal forms for nodes
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski with incoming hiding links. (This may take long and may not be implemented
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski for all logics.)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiLet us extend the above library \texttt{Order.casl}. One use of the
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskilibrary might be to express the fact that the natural numbers form a
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskistrict partial order as a view, as follows:
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{BIGEXAMPLE}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{BIGEXAMPLE}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{EXAMPLE}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\I\SPEC \NAMEDEFN{Natural\_Order\_2} =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\IEXT{\NAMEREF{Natural}} \THEN
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\I\PRED \( \_\_<\_\_ : Nat \* Nat\)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\(\[ \FORALL x,y:Nat \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. 0 < suc(x) \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. \neg x < 0 \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. suc(x) < suc(y) \IFF x < y
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{EXAMPLE}%[\SLIDESMALL]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\NAMEREF{Natural\_Order\_2} =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\I{} \( Elem \MAPSTO Nat\)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAgain, these specifications can be checked with \Hets. However, this
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskionly checks syntactic and static semantic well-formedness -- it is
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiby a strict partial ordering relation. Checking this requires theorem
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiproving, which will be discussed below.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHowever, before coming to theorem proving, let us first inspect the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiproof obligations arising from a specification. This can be done with:
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\texttt{hets -g Order.casl}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski(assuming that the above two specifications and the view
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskihave been added to the file
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Hets now displays a so-called development graph
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(which is just an overview graph showing the overall structure
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof the specifications in the library), see Fig.~\ref{fig:dg0}.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{figure}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{center}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\includegraphics[scale=0.7]{dg-order-0}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\caption{Sample development graph.\label{fig:dg0}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiNodes in a development graph correspond to \CASL specifications.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidenotes a proof obligation (corresponding to the view).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThis proof obligation needs to be discharged in order to
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskishow that the view is well-formed (then its color turns into green).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAs a more complex example, consider the following loose specification
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof a sorting function, taken from the \CASL User Manual
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\cite{CASL-UM}, Chap.~6:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{BIGEXAMPLE}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\I\SPEC \NAMEREF{List\_Order\_Sorted}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
e8f5a6ef56e210093ad852ed147d7f5f0a24cce9Till Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
e8f5a6ef56e210093ad852ed147d7f5f0a24cce9Till Mossakowski\begin{ITEMS}[\WITHIN]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{ITEMS}[\PRED]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\I\PRED \( \_\_is\_sorted : List \)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\(\[ \FORALL e,e': Elem; L : List \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \. empty~is\_sorted \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \. cons(e,empty)~is\_sorted \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \. cons(e,cons(e',L))~is\_sorted \IFF
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{ITEMS}[\OP]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\I\OP \( order : List \TOTAL List \)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{BIGEXAMPLE}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe following specification of sorting by insertion also is taken from
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskithe \CASL User Manual \cite{CASL-UM}, Chap.~6:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{BIGEXAMPLE}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\I\SPEC \NAMEREF{List\_Order}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\phantomsection
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{ITEMS}[\WITHIN]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{ITEMS}[\OP]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\I\OP \( insert : Elem \* List \TOTAL List \)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\(\[ \FORALL e,e':Elem; L:List \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. insert(e, empty) = cons(e, empty) \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. insert(e, cons(e',L)) = \[ cons(e', insert(e,L)) \WHEN e' < e\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \ELSE cons(e, cons(e',L)) \] \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{ITEMS}[\OP]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\I\OP \( order : List \TOTAL List \)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\(\[ \FORALL e:Elem; L:List \\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \. order(empty) = empty \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. order(cons(e,L)) = insert(e, order(L)) \]\)
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\end{BIGEXAMPLE}
47af295501ed5f407848f61b9943d58ccb43be29Till MossakowskiBoth specifications are related. To see this, we first inspect
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskitheir signatures. This is possible with:
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\texttt{hets -g Sorting.casl}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskiassuming that \texttt{Sorting.casl} contains the above specifications.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\begin{figure}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{center}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill 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
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiunnamed node for each structured specification that is not named.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAgain, the black arrows denote an ordinary import of specifications
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(corresponding to the extensions and unions in the
5277e290ad70afdf97f359019afd8fb5816f4102Till 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}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski as a red arrow.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHere is a summary of the types of nodes and links occurring in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidevelopment graphs:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Named nodes] correspond to a named specification.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Unnamed nodes] correspond to an anonymous specification.
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski\item[Elliptic nodes] correspond to a specification in the current library.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Rectangular nodes] are external nodes corresponding to a specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski downloaded from another library.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Red nodes] have open proof obligations.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Yellow nodes] have an open conservativity proof obligations.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Green nodes] have all proof obligations resolved.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Black links] correspond to reference to other specifications (definition
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski links in the sense of \cite[IV:4]{CASL/RefManual}).
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Red links] correspond to open proof obligations (theorem links).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Green links] correspond to proven theorem links.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Yellow links] correspond to proven theorem links with open
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski conservativity or to open hiding theorem links.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Blue links] correspond to hiding, free, or cofree definition links.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Violett links] correspond to a mixture of links becoming visible after
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski ``expand'' or ``Show unnamed nodes with open proofs''.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Solid links] correspond to global (definition or theorem)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilinks in the sense of \cite[IV:4]{CASL/RefManual}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Dashed links] correspond to local (theorem) links in the sense of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \cite[IV:4]{CASL/RefManual}. These are usually created after
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ``Global-Decomposition'' or only be visible after ``Show newly added proven
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Single line links] have homogeneous signature morphisms (staying within
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski one and the same logic).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Double line links] have heterogeneous signature morphisms (moving
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski between logics).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiWe now explain the menus of the development graph window.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMost of the pull-down menus of the window are uDraw(Graph)-specific
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskitheir function can be looked up in the uDraw(Graph) documentation\footnote{see
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\url{http://www.informatik.uni-bremen.de/uDrawGraph/en/service/uDG31\_doc/}.}.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe exception is the Edit menu. Moreover, the nodes and links
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiof the graph have attached pop-up menus, which appear when
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiclicking with the right mouse button.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\ednote{TODO Mihai: update}\\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{description}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Edit] This menu has the following submenus:
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{description}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Undo] Undo the last development graph proof step (see under Proofs)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Redo] Restore the last undone development graph proof step (see
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski under Proofs)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe ``Hide/show names/nodes/edges'' menu is a toggle:
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiyou can switch on or off the display of node names, unnamed nodes or
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiproven theorem links.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiWith the ``Hide/show internal node names'' option, the nodes that
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiare initially unnamed get names that
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiare derived from named neighbour nodes.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiWith the ``Hide/show unnamed nodes'' option, it is possible
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskito reveal the unnamed nodes which do not have open proof goals.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiInitially, the complexity of the graph is reduced by hiding all these nodes;
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskionly nodes corresponding to named specifications are displayed.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiPaths between named nodes going through unnamed nodes
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiare displayed as edges; these paths are then expanded when showing the
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiunnamed nodes.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWhen applying the development graph calculus rules, theorem links that have
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskibeen proven are removed from the graph. With the ``Hide/Show newly added
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiproven edges'' option, it is possible to re-display these links; they are marked
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskias proven in the link info (see \emph{Pop-up menu for links}, below).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Focus node]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThis menu is particularly useful when navigating a large development graph,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhich does not fit on a single screen. The list of all nodes is displayed:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe nodes are identified by the internal node number and the internal node name.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiOnce a node is selected, the view centers on it.
theorem links. It is possible to select/deselect all links or to invert the
i.e. have a model. The model finders currently interfaced are
Manual \cite{CASL/RefManual} or one of
i.e. axioms declared locally.
\emph{Proofs/Compute Normal Form}. For such nodes, a warning is displayed.
between them, i.e. translation (blue links) and inclusion (black links).
| graph.(exp.dot|dot)
The \texttt{owl} option \cite{books/sp/Kohlhase06} will produce OWL files in
The \texttt{omdoc} format \cite{books/sp/Kohlhase06} is an XML-based
When the \texttt{comptable.xml} format is selected, \Hets will extract
algebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
available from \texttt{www.cofi.info/Libraries}.
printed \LaTeX\ version of \texttt{Order.casl} by typing:
This will generate a file \texttt{Order.pp.tex}. It can be included
into \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
coming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty}) is used.
The format \texttt{pp.xml} represents a library in XML for our change
The \texttt{tptp} format (\url{http://www.tptp.org}) is a standard
\item[\texttt{-l LOGIC}, \texttt{--logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
\item[\texttt{-m FILE}, \texttt{--modelSparQ=FILE}] model check a qualitative calculus given in SparQ lisp notation \cite{SparQ06} against a \CASL specification
prover, i.e. by using the ``Prove'' menu of a red node.
% http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0
\url{http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0}
\cite{DBLP:conf/tacas/Aspinall00,url:ProofGeneral} in a separate Emacs
The \Isabelle theory file conforms to the Isabelle/Isar syntax
E-KRHyper\footnote{\url{http://www.uni-koblenz.de/~bpelzer/ekrhyper/}}
KRHyper\footnote{\url{http://www.uni-koblenz.de/~wernhard/krhyper/}} by
version, where e.g.\ error handling is ignored. For technical reasons
the static analysis of basic specifications) and/or translates (along
of the \Hets home page at \url{http://www.dfki.de/sks/hets}.
%\input{hets.tex}