README.md revision 499b61abb04643053c571ef2a4e10b59d73f9ca7
a9de0a2f34860a24f457c777e740b7e87e6e3827Christian Maeder# Hets (The heterogeneous tool set)
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian MaederHets is a parsing, static analysis and proof management tool incorporating various provers and different specification languages, thus providing a tool for heterogeneous specifications. Logic translations are first-class citizens.
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder### Supported languages
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder* general-purpose logics: [Propositional](http://en.wikipedia.org/wiki/Propositional_calculus), [QBF](http://en.wikipedia.org/wiki/QBF), [TPTP](http://www.tptp.org/)/SoftFOL, [CASL](http://www.cofi.info/CASL) (FOL), [HasCASL](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/HasCASL/) (HOL)
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian Maeder* logical frameworks: [Isabelle](http://www.cl.cam.ac.uk/research/hvg/Isabelle/), [LF](http://en.wikipedia.org/wiki/LF_%28logical_framework%29), DFOL
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski* modeling languages: [Meta-Object Facility (MOF)](https://en.wikipedia.org/wiki/Meta-Object_Facility), [Query/View/Transformation (QVT)](https://en.wikipedia.org/wiki/QVT)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski* ontologies and constraint languages: [OWL](http://www.w3.org/TR/owl2-overview/), [CommonLogic](http://cl.tamu.edu/), [RelScheme](http://en.wikipedia.org/wiki/Database_schema), ConstraintCASL
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder* reactive systems: CspCASL, [CoCASL](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/CoCASL/), ModalCASL, [Maude](http://maude.cs.uiuc.edu/)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder* programming languages: [Haskell](http://www.haskell.org/), [VSE](http://www.dfki.de/vse/systems/vse/)
0095c7efbddd0ffeed6aaf8ec015346be161d819Till Mossakowski* logics of specific tools: Reduce, DMU ([CATIA](http://en.wikipedia.org/wiki/CATIA))
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski### The following provers have been connected to Hets:
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder* [minisat](http://minisat.se/) and [zChaff](http://www.princeton.edu/~chaff/zchaff.html), which are SAT solvers,
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder* [SPASS](http://www.spass-prover.org/), [Vampire](http://en.wikipedia.org/wiki/Vampire_(theorem_prover)), [Darwin](http://combination.cs.uiowa.edu/Darwin/), [Hyper](http://userpages.uni-koblenz.de/~bpelzer/hyper/) and MathServe, which are automatic first-order theorem provers,
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder* [Pellet](http://clarkparsia.com/pellet/) and [Fact++](http://owl.man.ac.uk/factplusplus/), description logic tableau provers,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski* [Leo-II](http://page.mi.fu-berlin.de/cbenzmueller/leo/) and [Satallax](http://www.ps.uni-saarland.de/~cebrown/satallax/), automated higher-order provers,
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder* [Isabelle](http://www.cl.cam.ac.uk/Research/HVG/Isabelle/), an interactive higher-order theorem prover,
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder* [CSPCASL-prover](http://dx.doi.org/10.1016/j.entcs.2009.08.018), an Isabelle-based prover for CspCASL,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski* [VSE](http://www.dfki.de/vse/systems/vse/), an interactive prover for dynamic logic.
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiThe structuring constructs of the heterogeneous specification language are those of the language [CASL](http://www.cofi.info/CASL), plus some constructs to select languages (logics) and language translations. The heterogeneous specification language of Hets is called [HetCASL](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/HetCASL/index_e.htm). However, Hets can also read other structuring constructs, like those of Haskell, Maude or OWL. All these are mapped to so-called development graphs and processed with a proof calculus for heterogeneous development graphs that allows to decompose global proof obligations into local ones (during this, Hets also needs to compute [colimits](http://en.wikipedia.org/wiki/Limit_%28category_theory%29#Colimits_2) of theories over the involved logics).
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiHets is based on a graph of logics and logic translations. The overall architecture is depicted below. Adding new logics and logic translations to Hets can be done with moderate effort by adding some Haskell code to the Hets source. With the [Latin](https://trac.omdoc.org/LATIN/) project, this becomes much easier: logics (and in the near future also logic translations) can be declaratively specified in [LF](http://twelf.plparty.org/wiki/Bibliography_of_LF).
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederYou can try out Hets using the [Web-based interface](http://rest.hets.eu/)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski#### The best way to use hets is under Ubuntu. Possibly run this OS in a virtual box.
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiA compressed (1.2G, uncompressed 4.2G) virtual box image can be [downloaded from here](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/vbox-x86-linux). username/password is ubuntu/reverse.
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski### Installing Hets under Ubuntu
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski#### The basic system
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maedersudo apt-get install software-properties-common
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskisudo apt-add-repository ppa:hets/hets
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maedersudo apt-get update
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maedersudo apt-get install hets-desktop
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder* for the full system including all provers etc., use hets-desktop-all instead of hets-desktop
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder* for using Hets as a server providing a RESTful interface, use hets-server or hets-server-all. This is a smaller version without GUI dependencies. Note that also hets-desktop can be used as as server.
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder#### Hets development
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederFor Hets development additionally type in
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskisudo apt-add-repository -s "deb http://ppa.launchpad.net/hets/hets/ubuntu xenial main"
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskisudo apt-get update
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskisudo apt-get build-dep hets-desktop
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiReplace 'xenial' with the Ubuntu version that you use.
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiThe Hets sources should be obtained from the git repository (see the end of this page).
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski### Installing Hets under Archlinux
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederWe provide the AUR-packages [`hets-desktop-bin`](https://aur.archlinux.org/packages/hets-desktop-bin/) and [`hets-server-bin`](https://aur.archlinux.org/packages/hets-server-bin/) to install 64 bit binaries of Hets/Hets-server.
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederIf you would like to compile Hets yourself, you can install one of the AUR-packages [`hets-desktop`](https://aur.archlinux.org/packages/hets-desktop/) and [`hets-server`](https://aur.archlinux.org/packages/hets-server/).
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder### Installing Hets under OS X/macOS (10.9 (Mavericks) and greater)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski* Install Homebrew: See [https://brew.sh](https://brew.sh)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski* Install Java: `brew cask install java`
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder* Only for Hets-Desktop, install X11: `brew cask install xquartz`
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski* Either install hets-desktop: `brew install spechub/hets/hets-desktop`
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder* Or install hets-server: `brew install spechub/hets/hets-server`
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski### Hets binaries
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski(these are usually not needed but may replace the binaries from above)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski * [Daily snapshot](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/linux/daily/)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski * [Latest release](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/linux/releasedhets.bz2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder * [All versions](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/linux/versions/)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski* Linux x86_64
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski * [Daily snapshot](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/linux64/daily/)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder * [Latest release](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/linux64/releasedhets.bz2)
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder * [All versions](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/linux64/versions/)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski * [Daily snapshot](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/pc-solaris/daily/)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski * [Latest release](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/pc-solaris/releasedhets.bz2)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski * [All versions](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/pc-solaris/versions/)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski#### How to use a hets binary?
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian MaederJust download the binary and put it somewhere in the $PATH.
e7d2b3903c7b44db432538b0d720c21062c24823Christian Maeder* Our current linux binaries also rely on gtk-2 and glade-2 libraries for more and better menus. Thus you may need to install additional libraries. Use ldd (or "otools -L hets" on Macs) to see which libraries are missing.)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski* For displaying development graphs (with the -g option), you need to install [uDraw(Graph)](http://www.informatik.uni-bremen.de/uDrawGraph/en/) (formerly known as daVinci) that relies on [Tcl/Tk (version 8.4 or 8.5)](http://www.tcl.tk/software/tcltk/8.4.html) (which probably has been already installed on your computer anyway). Make sure uDrawGraph and wish are in your $PATH.
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiDownload the [CASL libraries](http://www.cofi.info/Libraries) and set $HETS_LIB to the folder containing these.
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski### Quickstart
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiHets is called with
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskihets -g filename
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiFor entering the command line mode, just call
a98fd29a06e80e447af26d898044c23497adbc73Mihai CodescuFor a short description of the options, call
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski### Restful Interface
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiSee [RESTful Interface](https://github.com/spechub/Hets/wiki/RESTful-Interface)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder### User Documentation
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiA good starting point is the [Hets user guide](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/UserGuide.pdf) and the [Hets user guide for Common Logic users](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/UserGuideCommonLogic.pdf). Furthermore two vidoes showing a heterogeneous proof are available:
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski* [A small video showing a heterogeneous proof](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/hets.m2v)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder* [A new video (H.264-Codec) showing a heterogeneous proof](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/Hets.mov)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiFor a formal introduction to hets see the introductory paper [The Heterogeneous Tool Set](http://www.informatik.uni-bremen.de/~till/papers/hets-paper.pdf) by Till Mossakowski, Christian Maeder, Klaus Lüttich and Stefan Wölfl. For more in-depth information about Hets see the thesis [Heterogeneous specification and the heterogeneous tool set](http://www.informatik.uni-bremen.de/~till/papers/habil.pdf) by Till Mossakowski.
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiFor questions related to hets there is a [mailing list](http://www.informatik.uni-bremen.de/mailman/listinfo/hets-users).
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski### Emacs Mode for CASL specifications
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiTo support writing CASL specifications we have an [emacs mode](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/emacs_mode)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder### Including specifications in LaTeX documents
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederWith the option "-o pp.tex" hets can produce nice LaTeX output from your specifictions that can be embedded in your publications using the [hetcasl.sty](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/hetcasl.sty) style file.
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder## Development
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederA good starting point is the code documentation for [Hets - the Heterogeneous Tool Set](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/src-distribution/versions/Hets/docs/).
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederSince Hets is rather large and complex we recommend following the interactive session in [Debugging and Testing Hets](https://github.com/spechub/Hets/wiki/Debugging-and-Testing-Hets) to get familiar with the central datastructures of Hets.
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederThe formal background and the general structure of Hets is described in chapter 7 of [Heterogeneous specification and the heterogeneous tool set](http://www.informatik.uni-bremen.de/~till/papers/habil.pdf).
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederHets is written in [Haskell](http://www.haskell.org), and is compiled using [GHC](http://www.haskell.org/ghc) using a couple of [language extensions](http://www.haskell.org/ghc/docs/latest/html/users_guide/ghc-language-features.html). Among the Haskell [books and tutorials](http://www.haskell.org/haskellwiki/Books_and_tutorials) we recommend [Real World Haskell](http://book.realworldhaskell.org/).
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederThe [language definition](http://www.haskell.org/onlinereport) covers the Haskell98 standard which we are supposed to stick to in most cases. Make sure that you are familiar with at least the most common [library functions of the Prelude](http://www.haskell.org/onlinereport/prelude-index.html).
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederFor searching or looking up any [library functions](http://www.haskell.org/ghc/docs/latest/html/libraries) you may also try [Hoogle](http://www.haskell.org/hoogle).
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederAlso look into [programming guidelines](http://www.haskell.org/haskellwiki/Programming_guidelines) and [things to avoid in Haskell](http://www.haskell.org/haskellwiki/Things_to_avoid).
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu### Dependencies
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederDependencies can be installed as specified in [Hets Development](#hets-development)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder### Contributing changes
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederBefore committing haskell source files you may check compliance to the programming guidelines:
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder* Use [scan](http://projects.haskell.org/style-scanner/) which can be installed by `cabal install scan`.
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder* The comments in your haskell sources should not cause `haddock` to fail. After `make` (for re-compiling changed sources) `make doc` will call `haddock`.
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder* Also check your source with [hlint](http://community.haskell.org/~ndm/hlint/) which you may install by `cabal install hlint`.
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederAlso have a look at the current [Release Notes](https://github.com/spechub/Hets/releases/latest), [Debugging and Testing Hets](https://github.com/spechub/Hets/wiki/Debugging-and-Testing-Hets),[Code Review](https://github.com/spechub/Hets/wiki/Code-Review) and [Branching](https://github.com/spechub/Hets/wiki/Branching).
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederIf you want to participate in the Hets development feel free to tell us via our [mailing list](http://www.informatik.uni-bremen.de/mailman/listinfo/hets-devel) for Hets developers. This mailing list can also be read via http://news.gmane.org/gmane.comp.lang.hets.devel.
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederIf you wish to make larger changes we generally recommend [forking](https://help.github.com/articles/fork-a-repo) this repository. You can however request access to this repository if you plan on contributing regularly.
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder### Build Hets using Stack
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder* [Install Stack](https://docs.haskellstack.org/en/stable/install_and_upgrade) (use the generic Linux option if you are on Ubuntu).
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder* Install build- and GUI-dependencies
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sudo apt-get install libglib2.0-dev libcairo2-dev libpango1.0-dev libgtk2.0-dev libglade2-dev libncurses-dev
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder brew cask install xquartz
c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder brew install binutils glib libglade cairo gtk fontconfig freetype gettext spechub/hets/udrawgraph
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder* Build Hets with one of the following:
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder make hets_server
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich This uses Stack to build the Hets[-Server] binary.
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder During this process, the specified version of GHC is installed in the user directory, all dependencies are built and finally, the Hets[-Server] binary is compiled.
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder## Troubleshooting & Useful Tools
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder## Hints for contributors switching from svn to git
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder* We recommend the [Git - SVN Crash Course](http://git-scm.com/course/svn.html).
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder* For github specific info on checking out this repository see [Fetching a remote](https://help.github.com/articles/fetching-a-remote).
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederThe Hets source code is licensed under the GPLv2 or higher