This README belongs to a Hets release (and does not apply to

sources directly obtained via cvs).

Information not contained here can be found in the Hets user guide

(doc/UserGuide.pdf) or on the Hets web page (www.tzi.de/cofi/hets).

The subject of this release is a binary "hets" that is able to analyse

heterogeneous and in particular CASL specifications.

The sources need to be compiled with ghc Glasgow Haskell Compiler

(www.haskell.org/ghc).

The output of hets, if the input is successfully accepted, can be

displayed by "daVinci".

daVinci is maintained by b-novative and b-novative holds all rights.

This release may be accompanied with free binary releases of daVinci

Version 2.1, but daVinci 2.1 is no longer supported or maintained!

However, you are encouraged to obtain the latest version of daVinci

Presenter (currently 3.0.5) from http://www.b-novative.com that is

free for academic purposes.

Linux: the linux binary release of daVinci 2.1 relies on the old

shlibs5 that must be installed on your system (if ./daVinci cannot be

found/executed, then shlibs5 are missing)

Solaris: the solaris binary release of daVinci 2.1 should work without

problems

Macintosh (Darwin): there is no release of daVinci for Macintosh, but

b-novative may have one in the mean time

For best quality, get the latest version of daVinci from b-novative.

For hets to find daVinci, the environment variables DAVINCIHOME and

UNIDAVINCI must be set to the installation directory of daVinci and to

the actual executable, respectively.

export DAVINCIHOME=<path>/daVinci_V2.1

export UNIDAVINCI=<path>/daVinci_V2.1/daVinci

A typical call of hets is then: <path>/hets -g Basic/Numbers.casl

If you need to rebuild the hets binary follow the instructions in INSTALL

(This README belongs a to release created by "make release", in case

that you obtained the HetCATS sources as CVS tree)

The heterogeneous tool set (Hets) is mainly maintained by

Christian Maeder (maeder@tzi.de) and Till Mossakowski

(till@tzi.de). The mailing list is hets@tzi.de.

Overview of source modules, with maintainers:

For more details, see the Haddock documentation in docs/

(after generation with "make doc")

--------------------------------------------------------

LICENCE.txt Licence information (english) (Till Mossakowski)

LIZENZ.txt Licence information (german) (Till Mossakowski)

INSTALL Installation and compilation instructions (???)

Makefile GNU-Makefile to compile sources (Klaus Luettich)

README This file (Till Mossakowski)

hets.hs Top-level Haskell module for hets (Till Mossakowski)

version_nr Current version (Till Mossakowski)

ATC/ Conversion from and to ATerms (Klaus Luettich)

CASL/ Instance of Logic: CASL (Till Mossakowski/Christian Maeder/Martin Kuehl)

CoCASL/ Instance of Logic: CoCASL (Till Mossakowski)

CoL/ Instance of Logic: COL (Till Mossakowski)

Common/ Modules common to all logics

Common/ATerm/ Conversion from and to ATerms (Christian Maeder)

Common/Lib/ Set, Map, Graph, Rel modules (Christian Maeder)

Common/Lib/Parsec/ Parsec combinator parser (Christian Maeder)

Common/PrettyPrint.hs pretty printing (Klaus Luettich)

pretty printing should get an own directory

Comorphisms/ Comorphisms of the logic graph (Till Mossakowski)

CspCASL/ Instance of Logic: CspCASL (Markus Roggenbach)

doc/ Documentation (Till Mossakowski)

docs/ Haddock generated documentation (Klaus Luettich)

ghc/ ghc-specific "coerce" (Christian Maeder)

GUI/ GUI for displaying development graphs (Till Mossakowski/Jorina Gerken)

HasCASL/ Instance of Logic: HasCASL (Christian Maeder)

Haskell/ Instance of Logic: Haskell (Christian Maeder)

Haskell/Hatchet/ parsing, printing, analysis of Haskell

hetcats/ Command line interface (Klaus Luettich)

hugs/ hugs-specific "coerce" (Christian Maeder)

Isabelle/ Instance of Logic: Isabelle

Logic/ Infrastructure for logic independence (Till Mossakowski)

Modal/ Instance of Logic: ModalCASL (Till Mossakowski)

Proofs/ Heterogeneous proof engine (Till Mossakowski/Jorina Gerken)

Static/ Heterogeneous development graphs and static analysis (Till Mossakowski/Maciek Makowski)

Syntax/ Heterogeneous syntax and parsing (Till Mossakowski, Christian Maeder)

ToHaskell/ translation to Haskell (Christian Maeder)

utils/ Utilities

utils/DrIFT-src/ DrIFT (for polytpyic conversion functions) (Klaus Luettich)

utils/GenerateRules/ generate files to be DRIFTed (Klaus Luettich)

utils/inlineAxioms parse inline axioms (Till Mossakowski)