UserGuide.tex revision 460a5052a96ce648bbecc9a0bd41c1b82a1c4e59
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\documentclass{article}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\usepackage{alltt}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\usepackage{casl}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\usepackage{xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\usepackage{color}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\QUERY}[1]%{}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\eat}[1]{}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\IEXT}[1] {\\#1\I}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\IEND} {\I\END}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newenvironment{EXAMPLEFORMAT} {}{}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder%% Added by MB to have some extra vertical space after the ``main'' examples
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder%% following the points (and some others in the text):
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newenvironment{BIGEXAMPLE} {\begin{EXAMPLE}} {\end{EXAMPLE}\medskip}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newenvironment{DETAILSFORMAT} {}{}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newenvironment{META}[1][] {#1\begin{METAFORMAT}}{\end{METAFORMAT}}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newenvironment{METAFORMAT} {\medskip\vrule\hspace{1ex}\vrule\hspace{1ex}%
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder \begin{minipage}{0.9\textwidth}\it}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder {\end{minipage}\par\medskip}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\SLIDESMALL} {}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\SLIDESONLY}[1] {}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder% SIMULATING SMALL-CAPS FOR BOLD, EMPH
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder%\newcommand {\CoFI}{CoFI\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\largeELAN} {\largeTEXTSC{E}{LAN}\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand {\HOL}{\normalTEXTSC{H}{OL}\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand {\Isabelle}{\normalTEXTSC{I}{SABELLE}\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder%%%%% Klaus macros
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder%%%%% end of Klaus macros
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand{\LCF}{LCF\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\ASF}{ASF\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\SDF}{SDF\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder%% Do NOT use \ASF+\SDF (it gives a superfluous space in the middle)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand{\CCC}{CCC\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\CoCASL}{\normalTEXTSC{C}{O}\normalTEXTSC{C}{ASL}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand{\CspCASL}{\normalTEXTSC{C}{SP}-\normalTEXTSC{C}{ASL}\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\begin{document}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\title{{\bf \protect{\LARGEHets} User Guide}\\
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder-- Version 0.5 --}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\author{Till Mossakowski\\[1em]
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von SchroederDepartment of Computer Science\\ and Bremen
045eb445945abe778eba4f86c806e6b20e957957Jonathan von SchroederInstitute for Safe Systems,\\ University of Bremen, Germany.\\[1em]
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von SchroederComments to: hets-devel@tzi.de
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\section{Introduction}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von SchroederThe Heterogeneous Tool Set (\protect\Hets) is the main analysis tool
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederfor the specification language heterogeneous \CASL. Heterogeneous
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\CASL (\HetCASL) combines the specification language \CASL with \CASL extensions
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederand sublanguages, as well as completely different logics and even
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederprogramming languages such as Haskell. \HetCASL
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederextends the structuring mechanisms of \CASL:
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\emph{Basic specifications} are
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederunstructured specifications or modules written in a specific logic.
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von SchroederThe graph of currently supported logics and logic translations (the
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroederlatter are also called comorphisms) is shown in
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von SchroederFig.~\ref{fig:LogicGraph}, and the degree of support by \Hets in
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von SchroederFig.~\ref{fig:Languages}.
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von SchroederWith \emph{heterogeneous structured specifications}, it is possible to
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroedercombine and rename specifications, hide parts thereof, and also
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroedertranslate them to other logics. \emph{Architectural specifications}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederprescribe the structure of implementations. \emph{Specification
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder libraries} are collections of named structured and architectural
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\Hets consists of logic-specific tools for the parsing and static
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederanalysis of the different involved logics, as well as a
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederlogic-independent parsing and static analysis tool for structured and
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederarchitectural specifications and libraries. The latter of course needs
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederto call the logic-specific tools whenever a basic specification is
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\section{Logics supported by \Hets}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder \includegraphics[scale=0.4]{LogicGraph}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\caption{Graph of logics currently supported by \Hets. The more an
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroederellipse is filled, the more stable is the implementation of the logic.}
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder\label{fig:LogicGraph}
e2f6183cac38aa0c12ebb42f526d92749fba6b43Jonathan von Schroeder\begin{tabular}{|l|c|c|c|}\hline
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von SchroederLanguage & Parser & Static Analysis & Prover \\\hline
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\CASL & x & x & - \\\hline
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\CoCASL & x & x & - \\\hline
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\ModalCASL & x & x & - \\\hline
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\HasCASL & x & x & - \\\hline
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von SchroederHaskell & x & x & -\\\hline
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder\CspCASL & (x) & - & - \\\hline
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder%Structured specifications & x & x & (x) \\\hline
e2f6183cac38aa0c12ebb42f526d92749fba6b43Jonathan von Schroeder%Architectural specifications & x & x & -\\\hline
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\CASLDL & x & - & - \\\hline
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von SchroederOWL DL basic & x & (x) & - \\\hline
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von SchroederOWL DL structure & x & (x) & - \\\hline
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von SchroederSPASS & - & - & x \\\hline
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder\Isabelle & - & - & x \\\hline
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\caption{Current degree of \Hets support for the different languages.\label{fig:Languages}}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\begin{description}
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder\item[CASL] extends many sorted first-order logic with partial
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder functions and subsorting. It also provides induction sentences,
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder expressing the (free) generation of datatypes.
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder%It is mainly designed and used for the
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder%specification of requirements for software systems. But it is also
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder%used for the specification of \Dolce (Descriptive Ontology for
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder%Linguistic and Cognitive Engineering), an Upper Ontology for knowledge
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder%representation. \cite{Gangemi:2002:SOD} Further it is now used to
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder%specify calculi for time and space.
11215d71075e01a34e70e0499503aac1ce4b8954Jonathan von SchroederFor more details on \CASL see \cite{CASL-RM,CASL-UM}.
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von SchroederWe have implemented the \CASL logic in such a way that much of the
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroederimplementation can be re-used for \CASL extensions as well; this
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederis achieved via ``holes'' (realized via polymorphic variables) in the
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroedertypes for signatures, morphisms, abstract syntax etc. This eases
26a00c47de4332eaf1ed218f7bb4df92cc44c53fJonathan von Schroederintegration of \CASL extensions and keeps the effort of integrating
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\CASL extensions quite moderate.
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\item[CoCASL] \cite{MossakowskiEA04} is a coalgebraic extension of \CASL,
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroedersuited for the specification of process types and reactive system.
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von SchroederThe central proof method is coinduction.
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\item[ModalCASL] is an extension of \CASL with multi-modalities and
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroederterm modalities. It allows the specification of modal systems with
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von SchroederKripke's possible worlds semantics. It is also possible to express
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroedercertain forms of dynamic logic.
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\item[HasCASL] is a higher order extension of \CASL allowing
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder polymorphic datatypes and functions. It is closely related to the
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder programming language Haskell and allows program constructs being
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder embedded in the specification.
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroederthe language is summarized in \cite{HasCASL/Summary}.
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von SchroederThe latter document is also available on the CD-ROM
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder\item[Haskell] is a modern, pure and strongly typed functional
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder programming language. It simultaneously is the implementation
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder language of \Hets, such that in the future, \Hets might be applied
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von SchroederThe definitive reference for Haskell is \cite{PeytonJones03},
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\item[CspCASL] \cite{Roggenbach:2003:C-CN} is a combination of \CASL
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder with the process algebra CSP.
26a00c47de4332eaf1ed218f7bb4df92cc44c53fJonathan von Schroeder\item[OWL DL] is the Web Ontology Language (OWL) recommended by the
26a00c47de4332eaf1ed218f7bb4df92cc44c53fJonathan von Schroeder World Wide Web Consortium (W3C, \texttt{http://www.w3c.org}). It is
26a00c47de4332eaf1ed218f7bb4df92cc44c53fJonathan von Schroeder used for knowledge representation and the Semantic Web
26a00c47de4332eaf1ed218f7bb4df92cc44c53fJonathan von Schroeder \cite{berners:2001:SWeb}.
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von SchroederHets calls an external OWL DL parser
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder written in JAVA to obtain the abstract syntax for an OWL file and its
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder imports. The JAVA parser is also doing a first analysis classifying
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder the OWL ontology into the sublanguages OWL Full, OWL DL and OWL
11215d71075e01a34e70e0499503aac1ce4b8954Jonathan von Schroeder Hets only supports the last two, more restricted variants.
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder structuring of the OWL imports is displayed as Development Graph.
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder\item[CASL-DL] is an extension of a restriction of \CASL, realizing
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroedera strongly typed variant of OWL DL in \CASL syntax.
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder \CASL with cardinality restrictions for the description of sorts and
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder unary predicates. The restrictions are based on the equivalence
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder between \CASLDL, OWL~DL and \SHOIN. Compared to \CASL only unary
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder and binary predicates, predefined datatypes and concepts (subsorts
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder of the topsort Thing) are allowed. It is used to bring OWL DL and
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder \CASL closer together.
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\item[SPASS] \cite{WeidenbachEtAl02} is an automatic theorem prover for first-order logic
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover for higher-order
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\end{description}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von SchroederSPASS and \Isabelle are the only logics coming with a prover. Proof
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroedersupport for the other logics can be obtained by using logic translations
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederto a prover-supported logic.
045eb445945abe778eba4f86c806e6b20e957957Jonathan von SchroederAn introduction to \CASL can be found in the \CASL User Manual
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\cite{CASL-UM}; the detailed language reference is given in
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederthe \CASL Reference Manual \cite{CASL/RefManual}. These documents
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederexplain both the \CASL logic and language of basic specifications as
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederwell as the logic-independent constructs for structured and
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederarchitectural specifications. Corresponding documents explaining the
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\HetCASL language constructs for \emph{heterogeneous} structured specifications
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederare forthcoming, until then, \cite{Mossakowski:2003:FHS} may serve as a short
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederintroduction. Moreover, the main heterogeneous constructs will be illustrated
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederin Sect.~\ref{sec:HetSpec} below.
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\section{Getting started}
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von SchroederThe latest \Hets version can be obtained from the
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\Hets tools home page
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder Since \Hets is being
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederimproved constantly, it is recommended always to use the latest version.
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder\Hets currently is available for Linux, Solaris and
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von SchroederMacIntosh users need to install some libraries, which can be found
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederat the \Hets download page.
045eb445945abe778eba4f86c806e6b20e957957Jonathan von SchroederIf you want to compile \Hets from the sources, please follow the
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederlink ``Hets: source code and information for developers''
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederon teh \Hets web page, download the sources (as tarball or from
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroedercvs), and follow the
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederinstructions in the \texttt{INSTALL} file.
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\subsection*{uDraw(Graph)}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von SchroederFor the display of development graphs (with the -g option), \Hets uses
045eb445945abe778eba4f86c806e6b20e957957Jonathan von SchroederuDraw(Graph), formerly known as daVinci.
045eb445945abe778eba4f86c806e6b20e957957Jonathan von SchroederYou can get uDraw(Graph) freely from
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\url{http://www.tzi.de/uDrawGraph/en/}.
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von SchroederMoreover, you need Tcl/Tk as well, available freely from
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\url{http://www.scriptics.com/software/tcltk/}.
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von SchroederBut Tcl/Tk probably has been already installed
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroederon your computer anyway.
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von SchroederSet the environment variable \texttt{\$UNIWISH} to the wish binary
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder(which is part of Tcl/Tk), and \texttt{\$UNIDAVINCI} to the
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von SchroederuDraw(Graph) binary. Furthermore, uDraw(Graph) requires that
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder\texttt{DAVINCIHOME} is set to the installation directory of
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder\subsection*{Isabelle}
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von SchroederFor theorem proving with \Isabelle, you need to install \Isabelle,
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroederwhich is available freely from
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}.
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von SchroederWe recommend to use the latest version (\Isabelle 2005), together
b48dcb6f74075d06b770ac905ff25f0c592e2258Jonathan von Schroederwith Proof General, a proof interface that comes with the \Isabelle
b48dcb6f74075d06b770ac905ff25f0c592e2258Jonathan von Schroederdistribution. Proof General uses the Eamcs or Xemacs editor.
b48dcb6f74075d06b770ac905ff25f0c592e2258Jonathan von SchroederSet the environment variable
b48dcb6f74075d06b770ac905ff25f0c592e2258Jonathan von Schroeder\texttt{\$HETS\_ISABELLE} to the \Isabelle (or Emacs, for use with proof general) binary, and set \texttt{\$LC\_CTYPE} to \texttt{C}.
b48dcb6f74075d06b770ac905ff25f0c592e2258Jonathan von SchroederSome \Isabelle theories generated by \Hets may need to have libraries
b48dcb6f74075d06b770ac905ff25f0c592e2258Jonathan von Schroederavailable, see the paragraph `Libraries` below.
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\subsection*{SPASS}
e2f6183cac38aa0c12ebb42f526d92749fba6b43Jonathan von SchroederFor theorem proving with SPASS, obtain SPASS freely from
e2f6183cac38aa0c12ebb42f526d92749fba6b43Jonathan von Schroeder\subsection*{Libraries of specifications}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von SchroederA repository of libraries of specifications for use with \Hets
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroederis available under \url{http://www.cofi.info/Libraries}.
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von SchroederThe environment variable \texttt{HETS\_LIB} should be set to
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroedera location where the specification libraries are stored.
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder%\QUERY{This should be done by the install script!}
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder\section{Analysis of Specifications}
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von SchroederConsider the following \CASL
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder\begin{BIGEXAMPLE}
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder\I\SPEC \NAMEREF{Strict\_Partial\_Order} =
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder\begin{ITEMS}[\PRED]
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\I\SORT \( Elem \)
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder% \COMMENTENDLINE{\PRED abbreviates predicate}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\(\[ \FORALL x,y,z : Elem \\
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von SchroederNote that there may exist \(x, y\) such that\\
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroederneither \(x < y\) nor \(y < x\).
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder\end{BIGEXAMPLE}
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder\Hets can be used for parsing and
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroederchecking static well-formedness of specifications.
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder \index{parsing}%
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder \index{static!analysis}%
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder \index{analysis, static}%
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von SchroederLet us assume that the example is in a file named
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder\texttt{Order.casl} (actually, this file is provided
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroederwith the \Hets distribution).
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von SchroederThen you can check the well-formedness of the
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroederspecification by typing (into some shell):
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder\Hets checks both the correctness of this specification
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder with respect to the \CASL syntax, as
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroederwell as its correctness with respect to the static semantics (e.g.\
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroederwhether all identifiers have been declared before they are used,
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroederwhether operators are applied to arguments of the correct sorts,
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroederwhether the use of overloaded symbols is unambiguous, and so on).
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von SchroederThe following flags are available in this context:
26a00c47de4332eaf1ed218f7bb4df92cc44c53fJonathan von Schroeder\begin{description}
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing -- the static analysis
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder\item[\texttt{-s}, \texttt{--just-structured}]
26a00c47de4332eaf1ed218f7bb4df92cc44c53fJonathan von SchroederDo the parsing and the static analysis of (heterogeneous) structured
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederspecifications, but leave out the analysis of basic specifications.
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von SchroederThis can be used to quickly produce a development graph
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroedershowing the dependencies among the specifications (cf. Sect.~\ref{sec:DevGraph}).
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von SchroederUse \texttt{DIR} as the directory for specification libraries
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder(equivalently, you can set the variable \texttt{HETS\_LIB} before
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[\texttt{--casl-amalg=ANALYSIS}]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder For the analysis of architectural specification (a quite advanced
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder amalgamability checking
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder algorithm for \CASL logic; it is a comma-separated list of zero or
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder more of the following options:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder \begin{description}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder \item[\texttt{sharing}] perform sharing analysis for sorts,
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder operations and predicates.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder \item[\texttt{cell}] perform cell condition check; implies
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder \texttt{sharing}. With this option on the subsort embeddings are
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder \item[\texttt{colimit-thinness}] perform colimit thinness check;
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder implies \texttt{sharing}. The colimit thinness check is less
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder complete and usually takes longer than the full cell condition
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder check (\texttt{cell} option), but may prove more efficient in case
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder of certain specifications.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder \end{description}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder If \texttt{ANALYSIS} is empty then amalgamability analysis for
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder \CASL is skipped.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder The default value for \texttt{--casl-amalg} is
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\end{description}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\section{Heterogeneous Specification} \label{sec:HetSpec}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\Hets accepts plain text input files with the following endings:\\
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{tabular}{|l|c|c|}\hline
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederEnding & default logic & structuring language\\\hline
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\texttt{.casl} & \CASL & \CASL \\\hline
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\texttt{.het} & \CASL & \CASL \\\hline
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\texttt{.hs} & Haskell/HasSLe & Haskell\\\hline
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\texttt{.owl} & OWL DL, OWL Lite & OWL\\\hline
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederAlthough the endings \texttt{.casl} and \texttt{.het} are
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederinterchangeable, the former should be used for libraries of
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederhomogeneous \CASL specifications and the latter for \HetCASL libraries
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederof heterogeneous specifications (that use the \CASL structuring
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederconstructs). Within a \HetCASL library, the current logic can be changed e.g.\
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederto \HasCASL in the following way:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{verbatim}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederThe subsequent specifications are then parsed and analysed as
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\HasCASL specifications. Within such specifications,
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederit is possible to use references to named \CASL specifications;
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederthese are then automatically translated along the default
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederembedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(Heterogeneous constructs
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfor explicit translations between logics will be made available
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederA \CspCASL specification consists of a \CASL specification
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfor the data part and a \Csp process built over this data part.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederTherefore, \HetCASL provides a heterogeneous language construct
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\texttt{data} as follows:
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder\begin{verbatim}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder free type List[Elem] ::= nil | cons(Elem; List[Elem])
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder channel read, write : Elem
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let Buf(l:List[Elem]) =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder read?x -> Buf( cons(x,nil) )
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [] if l=nil then STOP else write!last(l) -> Buf( rest(l) )
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederHere, the construct \texttt{data List} refers to the \CASL specification
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\texttt{List}, which is implicitly embedded into \CspCASL.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederThe ending \texttt{.hs} is available for directly reading in
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederHaskell programs and HasSLe specifications,
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederand hence supports the Haskell module system.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederthe logic Haskell has to be chosen explicitly, and the \CASL structuring
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroedersyntax needs to be used:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{verbatim}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederlibrary Factorial
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederspec Factorial =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfac :: Int -> Int
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfac n = foldl (*) 1 [1..n]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederNote that according to the Haskell syntax, Haskell function
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederdeclarations and definitions need to start with the first column of
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\section{Development Graphs}\label{sec:DevGraph}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederDevelopment graphs are a simple kernel formalism for (heterogeneous)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederstructured theorem proving and proof management. A development graph
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederconsists of a set of nodes (corresponding to whole structured
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederspecifications or parts thereof), and a set of arrows called
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederdefinition links, indicating the dependency of each involved
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederstructured specification on its subparts. Arising proof obligations
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederare attached as so-called theorem links to this graph.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederThe following options let \Hets show the development graph of
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroedera specification library:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{description}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[\texttt{-G}, \texttt{--only-gui}] Shows the development graph in a GUI window,
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederand suppresses the writing of an output file.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\end{description}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederLet us extend the above library \texttt{Order.casl}. One use of the
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederlibrary might be to express the fact that the natural numbers form a
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederstrict partial order as a view, as follows:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{BIGEXAMPLE}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\end{BIGEXAMPLE}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\I\SPEC \NAMEDEFN{Natural\_Order\_2} =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\IEXT{\NAMEREF{Natural}} \THEN
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\I\PRED \( \_\_<\_\_ : Nat \* Nat\)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\(\[ \FORALL x,y:Nat \\
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder \. 0 < suc(x) \\
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder \. \neg x < 0 \\
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder \. suc(x) < suc(y) \IFF x < y
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{EXAMPLE}%[\SLIDESMALL]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\NAMEREF{Natural\_Order\_2} =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\I{} \( Elem \MAPSTO Nat\)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederAgain, these specifications can be checked with \Hets. However, this
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederonly checks syntactic and static semantic well-formedness -- it is
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederby a strict partial ordering relation. Checking this requires theorem
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederproving, which will be discussed below.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederHowever, before coming to theorem proving, let us first inspect the
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederproof obligations arising from a specification. This can be done with:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(assuming that the above two specifications and the view
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederhave been added to the file
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\Hets now displays a so-called development graph
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(which is just an overview graph showing the overall structure
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederof the specifications in the library), see Fig.~\ref{fig:dg0}.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\includegraphics[scale=0.7]{dg-order-0}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\caption{Sample development graph.\label{fig:dg0}}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederNodes in a development graph correspond to \CASL specifications.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederArrows show how specifications are related by the structuring
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederThe black arrow denotes an ordinary import of
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederspecifications (generated by the extension), while the red arrow
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederdenotes a proof obligation (corresponding to the view).
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederThis proof obligation needs to be discharged in order to
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroedershow that the view is well-formed (then its color turns into green).
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederAs a more complex example, consider the following loose specification
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederof a sorting function, taken from the \CASL User Manual
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\cite{CASL-UM}, Chap.~6:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{BIGEXAMPLE}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\I\SPEC \NAMEREF{List\_Order\_Sorted}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{ITEMS}[\WITHIN]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{ITEMS}[\PRED]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\I\PRED \( \_\_is\_sorted : List \)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\(\[ \FORALL e,e': Elem; L : List \\
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder \. empty~is\_sorted \\
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder \. cons(e,empty)~is\_sorted \\
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder \. cons(e,cons(e',L))~is\_sorted \IFF
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{ITEMS}[\OP]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\I\OP \( order : List \TOTAL List \)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\end{BIGEXAMPLE}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederThe following specification of sorting by insertion also is taken from
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederthe \CASL User Manual \cite{CASL-UM}, Chap.~6:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{BIGEXAMPLE}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\I\SPEC \NAMEREF{List\_Order}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{ITEMS}[\WITHIN]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{ITEMS}[\OP]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\I\OP \( insert : Elem \* List \TOTAL List \)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\(\[ \FORALL e,e':Elem; L:List \\
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder \. insert(e, empty) = cons(e, empty) \\
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder \. insert(e, cons(e',L)) = \[ cons(e', insert(e,L)) \WHEN e' < e\\
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder \ELSE cons(e, cons(e',L)) \] \\
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{ITEMS}[\OP]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\I\OP \( order : List \TOTAL List \)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\(\[ \FORALL e:Elem; L:List \\
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder \. order(empty) = empty \\
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder \. order(cons(e,L)) = insert(e, order(L)) \]\)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\end{BIGEXAMPLE}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederBoth specifications are related. To see this, we first inspect
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroedertheir signatures. This is possible with:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederassuming that \texttt{Sorting.casl} contains the above specifications.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\includegraphics[scale=0.7]{dg-order-1}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\caption{Development graph for the two sorting specifications.\label{fig:dg1}}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederIn the above-mentioned development graph, we have two types of nodes.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederThe named ones correspond to named specifications, but there
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederare also unnamed nodes corresponding to anonymous basic
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederspecifications like the declaration of the $insert$ operation in
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\NAMEREF{List\_Order} above. Basically, there is an
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederunnamed node for each structured specification that is not named.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederAgain, the black arrows denote an ordinary import of specifications
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(corresponding to the extensions and unions in the
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederspecifications), while the blue arrows denote hiding (corresponding to
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederthe local specification).
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederBy clicking on the nodes, one can inspect their signatures.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederIn this way, we can see that both \NAMEREF{List\_Order\_Sorted} and
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\NAMEREF{List\_Order} have the same signature. Hence, it
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederis legal to add a view:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{EXAMPLE}%[\SLIDESMALL]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\I\VIEW \NAMEDEFN{v2}[\NAMEREF{Total\_Order}] ~:~ \NAMEREF{List\_Order\_Sorted}[\NAMEREF{Total\_Order}] \TO
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\NAMEREF{List\_Order}[\NAMEREF{Total\_Order}]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederWe have already added this view to \texttt{Sorting.casl}.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederThe corresponding
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederproof obligation between \NAMEREF{List\_Order\_Sorted} and
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\NAMEREF{List\_Order} is displayed in Fig.~\ref{fig:dg1}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder as a red arrow.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederHere is a summary of the types of nodes and links occurring in
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederdevelopment graphs:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{description}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Named nodes] correspond to a named specification.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Unnamed nodes] correspond to an anonymous specification.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Elliptic nodes] correspond to a specification in the current library.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Rectangular nodes] are external nodes corresponding
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder to a specification downloaded from
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederanother library.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Black links] correspond to reference to other specifications
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(definition links in the sense of \cite[IV:4]{CASL/RefManual}).
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Blue links] correspond to hiding (hiding definition links).
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Red links] correspond to open proof obligations (theorem links).
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Green links] correspond to proved proof obligations (theorem links).
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Solid links] correspond to global (definition or theorem)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederlinks in the sense of \cite[IV:4]{CASL/RefManual}.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Dashed links] correspond to local (definition or theorem) links in the sense of \cite[IV:4]{CASL/RefManual}.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\end{description}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederWe now explain the menus of the development graph window.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederMost of the pull-down menus of the window are uDraw(Graph)-specific
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroedertheir function can be looked up in the uDraw(Graph) documentation.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederThe exception is the Edit menu. Moreover, the nodes and links
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederof the graph have attached pop-up menus, which appear when
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederclicking with the right mouse button.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{description}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Edit] This menu has two submenus:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{description}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Unnamed nodes]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederThe ``Hide/show names'' menu is a toggle:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederyou can switcn on or off the display of names for nodes that
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederare initially unnamed. The newly named nodes get names that
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederare derived from named neighbour nodes.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederWith the ``Hide nodes'' submenu, it is possible
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederto reduce the complexity of the graph by hiding all unnamed nodes;
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederonly nodes corresponding to named specifications remain displayed.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederPaths between named nodes going through unnamed nodes
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederare displayed as links. With the ``Show nodes'' submenu, the unnamed
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroedernodes re-appear.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Proofs] This menu allows to apply some of the deduction rules
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder for development graphs, see Sect. IV:4.4 of the \CASL Reference
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Manual \cite{CASL/RefManual}. While support for local and global
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (definition or theorem) links is stable, support for hiding links
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder and checking conservativity is still experimental. In most cases, it is
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder advisable to use ``Automatic'', which automatically applies the
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder rules in the correct order. As a result, the the open theorem links
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (marked in red) will be reduced to local proof goals, that is, they
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder become green, and instead, some of the node will get red, indicating
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder open local proof goals.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\end{description}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Pop-up menu for nodes]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederHere, the number of submenus depends on the type of the node:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{description}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Show signature] Shows the signature of the node.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Show local axioms] Shows the local axioms of the node.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Show theory] Shows the theory of the node (including axioms
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederimported from other nodes). Warning: axioms imported via hiding links
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederare not part of the theory; they can be made visible only by re-adding
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederthe hidden symbols, using the proof rule \emph{Theorem-Hide-Shift}.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Translate theory] Translates the theory of a node to another logic.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederA menu with the possible translation paths will be displayed.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Show taxonomy graphs] (Only available for some logics) Shows the subsort graph of the signature of the node.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Show sublogic] Shows the logic and, within that logic, the minimal sublogic
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfor the signature and the axioms of the node.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Show origin] Shows the kind of \CASL structuring construct that
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederled to the node.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Prove] Try to prove the local proof goals. See Section~\ref{sec:Proofs}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Show proof status] Show open and proven local proof goals.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Check consistency] Check the consistency of the theory of the node.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Show just subtree] (Only for named nodes) Reduce the complexity
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederof the graph by just showing the subtree below the current node.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Undo show just subtree] (Only for named nodes) Undo the reduction.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Show referenced library] (Only for external nodes) Open a new window
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroedershowing the development graph for the library the external node refers to.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\end{description}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Pop-up menu for links]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederAgain, the number of submenus depends on the type of the node:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{description}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Show morphism] Shows the signature morphism of the link. It consists
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederof two components: a logic translation and a signature morphism in the
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroedertarget logic of the logic translation.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederIn the (most frequent) case
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederof an intra-logic signature morphism, the logic translation component is
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederjust the identity.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Show origin] Shows the kind of \CASL structuring construct that
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederled to the link.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Show proof status] (Only for theorem links) Show the proof status.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[Check conservativity] (Experimental) Check whether the
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroedertheory of the target node of the link
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederis a conservative extension of the theory of the source node.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\end{description}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\end{description}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\section{Reading, Writing and Formatting}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\Hets provides several options controlling the types of files
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederthat are read and written.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{description}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[\texttt{-i ITYPE}, \texttt{--input-type=ITYPE}] Specify
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\texttt{ITYPE} as the type of the input file. The default is
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\texttt{het} (\HetCASL plain text). \texttt{ast} is for reading
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederin abstract syntax trees in ATerm format, while \texttt{ast.baf}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederreads in the compressed ATerm format.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederThe possible input types are:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{verbatim}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (casl|het|owl|hs|ast[.baf]|[tree.]gen_trm[.baf])
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[\texttt{-O DIR}, \texttt{--output-dir=DIR}]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederSpecify \texttt{DIR} as destination directory for output files.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[\texttt{-o OTYPES}, \texttt{--output-types=OTYPES}]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\texttt{OTYPES} is a comma separated list of output types:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\begin{verbatim}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | pp.(het|tex|html)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | graph.(dot|ps|davinci)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | ast.(het|trm|taf|html|xml)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | (fdg|hdg|dg)[.nax].(het|trm|taf|html|xml)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederThe default is \texttt{dg.taf}, which means that the development
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroedergraph of the library is stored in textual ATerm format (\texttt{taf}).
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederThis format can be read in when a library is downloaded from
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederanother library, avoiding the need to re-analyse the downloaded library.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederThe \texttt{pp} format is for pretty printing, either as plain text
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(\texttt{het}), \LaTeX input (\texttt{tex}) or HTML (\texttt{html}).
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederA formatter with pretty-printed output currently is available only for
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederthe \CASL logic. For example, it is possible to generate a pretty
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederprinted \LaTeX\ version of \texttt{Order.casl} by typing:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederThis will generate a file \texttt{Order.pp.tex}. It can be included
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederinto \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroedercoming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty)}) is used.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederWhen the \texttt{thy} format is selected, \Hets will try to translate
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroedereach specification in the library to \Isabelle, and write one \Isabelle
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\texttt{.thy} file per specification.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederWhen the \texttt{comptable.xml} format is selected, \Hets will extract
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederthe composition and inverse table of a Tarskian relation algebra from
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederspecification(s) (selected with the \texttt{-n} or \texttt{--spec}
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederoption). It is assumed that the relation algebra is
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroedergenerated by basic relations, and that the specification is written
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederin the \CASL logic. A sample specification of a relation
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederalgebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederavailable from \texttt{www.cofi.info/Libraries}.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederThe output format is XML, the URL of the DTD is included in the
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[\texttt{-t TRANS}, \texttt{--translation=TRANS}]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederchooses a translation option. \texttt{TRANS} is a colon-separated list
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederwithout blanks of one or more from:
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederCFOL2IsabelleHOL,
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederCoCASL2CoPCFOL,\\
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederCoCFOL2IsabelleHOL,
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederCspCASL2IsabelleHOL,\\
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederHasCASL2HasCASL,
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederHasCASL2Haskell,\\
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederHasCASL2IsabelleHOL,
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederHaskell2IsabelleHOLCF,
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder\item[\texttt{-r RAW} or \texttt{--raw=RAW}] This option allows one
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederto influence the formatting in more detail.
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederHere, \texttt{RAW} is \texttt{(ascii|text|(la)?tex)=STRING},
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederand \texttt{STRING} is passed to the appropriate pretty-printer.
\item[\texttt{-l LOGIC}, \texttt{--logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
\cite{DBLP:conf/tacas/Aspinall00,url:ProofGeneral} in a separate Emacs
The \Isabelle theory file conforms to the Isabelle/Isar syntax
\input{hets.tex}